diff --git a/.github/workflows/nix-action-9.0-master.yml b/.github/workflows/nix-action-9.0-master.yml index aba868db3f..6caa1aa79b 100644 --- a/.github/workflows/nix-action-9.0-master.yml +++ b/.github/workflows/nix-action-9.0-master.yml @@ -130,6 +130,7 @@ jobs: - rocq-core - mathcomp-reals - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -194,6 +195,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -204,6 +209,7 @@ jobs: - mathcomp-finmap - mathcomp-bigenough - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -276,6 +282,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -688,6 +698,74 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-master" --argstr job "mathcomp-infotheo" + mathcomp-real-closed: + needs: + - rocq-core + - mathcomp-bigenough + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-real-closed) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.0-master\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run 2> err + > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "mathcomp-real-closed" mathcomp-reals: needs: - rocq-core diff --git a/.github/workflows/nix-action-9.1-master.yml b/.github/workflows/nix-action-9.1-master.yml index 185797a8ee..3e3aaf9bfb 100644 --- a/.github/workflows/nix-action-9.1-master.yml +++ b/.github/workflows/nix-action-9.1-master.yml @@ -130,6 +130,7 @@ jobs: - rocq-core - mathcomp-reals - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -194,6 +195,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -204,6 +209,7 @@ jobs: - mathcomp-finmap - mathcomp-bigenough - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -276,6 +282,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -688,6 +698,74 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1-master" --argstr job "mathcomp-infotheo" + mathcomp-real-closed: + needs: + - rocq-core + - mathcomp-bigenough + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-real-closed) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.1-master\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run 2> err + > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-real-closed" mathcomp-reals: needs: - rocq-core diff --git a/.github/workflows/nix-action-master.yml b/.github/workflows/nix-action-master.yml index adb5918eec..0b948625f4 100644 --- a/.github/workflows/nix-action-master.yml +++ b/.github/workflows/nix-action-master.yml @@ -254,6 +254,7 @@ jobs: - rocq-core - mathcomp-reals - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -318,6 +319,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -328,6 +333,7 @@ jobs: - mathcomp-finmap - mathcomp-bigenough - mathcomp-bigenough + - mathcomp-real-closed - stdlib runs-on: ubuntu-latest steps: @@ -401,6 +407,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -746,6 +756,74 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp-finmap" + mathcomp-real-closed: + needs: + - rocq-core + - mathcomp-bigenough + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-real-closed) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"master\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run 2> err > + out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "master" --argstr job "mathcomp-real-closed" mathcomp-reals: needs: - rocq-core diff --git a/.nix/config.nix b/.nix/config.nix index 7c48a67da2..aa747f8ba6 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -8,8 +8,6 @@ let mathcomp-analysis-stdlib.job = true; ssprove.override.version = "main"; mathcomp-infotheo.override.version = "master"; - interval.override.version = "master"; - coquelicot.override.version = "master"; }; in { ## DO NOT CHANGE THIS @@ -57,6 +55,7 @@ in { mathcomp.override.version = "master"; mathcomp-bigenough.override.version = "master"; mathcomp-finmap.override.version = "master"; + mathcomp-real-closed.override.version = "master"; micromega-plugin.override.version = "master"; }; coqPackages = common-bundle // { @@ -64,6 +63,7 @@ in { mathcomp.override.version = "master"; mathcomp-bigenough.override.version = "master"; mathcomp-finmap.override.version = "master"; + mathcomp-real-closed.override.version = "master"; ssprove.job = false; # not yet available for 9.1 }; }; @@ -85,6 +85,7 @@ in { mathcomp.override.version = "master"; mathcomp-bigenough.override.version = "master"; mathcomp-finmap.override.version = "master"; + mathcomp-real-closed.override.version = "master"; micromega-plugin.override.version = "master"; }; coqPackages = common-bundle // { @@ -92,6 +93,7 @@ in { mathcomp.override.version = "master"; mathcomp-bigenough.override.version = "master"; mathcomp-finmap.override.version = "master"; + mathcomp-real-closed.override.version = "master"; ssprove.job = false; # not yet available for 9.1 }; }; @@ -106,6 +108,7 @@ in { mathcomp.override.version = "master"; mathcomp-bigenough.override.version = "master"; mathcomp-finmap.override.version = "master"; + mathcomp-real-closed.override.version = "master"; micromega-plugin.override.version = "master"; }; coqPackages = common-bundle // { @@ -116,6 +119,7 @@ in { mathcomp.override.version = "master"; mathcomp-bigenough.override.version = "master"; mathcomp-finmap.override.version = "master"; + mathcomp-real-closed.override.version = "master"; ssprove.job = false; mathcomp-infotheo.job = false; }; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index e70ee2f134..22d1f20ff4 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"4a441c50de5618ef066128f9f6f84e6bc13066da" +"ed23062e563f0fbe6c27877bad88426c7f0dc9c9" diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0023dbb5e0..beeaa11c6c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -131,6 +131,51 @@ - in `lebesgue_stieltjes_measure.v`: + definition `lebesgue_display` +- in `unstable.v` + + lemmas `scalecE`, `normcr`, `Im_mul`, `mulrnc`, `complexA`, `normc_natmul`, + `nomrc_mulrn`, `gt0_normc`, `gt0_realC`, `ltc0E`, `ltc0P`, `ltcP`, `lecP`, + `realC_gt0`, `Creal_gtE`, `realC_norm`, `eqCr`, `eqCI`, `neqCr0`, + `real_normc_ler`, `im_normc_ler` + + notations `f %:Rfun`, `v %:Rc` + + lemmas `realCZ`, `realC_alg`, `scalecr`, `scalecV` + +- in `function_spaces.v` + + lemmas `cvg_big`, `continuous_big` + +- file `holomorphy.v` + + instance of `normedModType` on `complex` + + definition `ball_Rcomplex` + + lemmas `entourage_RcomplexE`, `normcZ`, `Rcomplex_findim` + + instance of `normedVectType` on `complex` + + definitions `holomorphic`, `Rdifferentiable`, `realC`, `CauchyRiemannEq` + + lemmas `holomorphicP`, `continuous_realC`, `Rdiff1`, `Rdiffi`, `littleoCo`, + `holo_differentiable`, `holo_CauchyRiemann`, `Diff_CR_holo`, + `holomorphic_Rdiff` + +- in `landau.v` + + lemma `littleoE0` + +- in `normed_module.v` + + structure `normedVectType` + + lemmas `dnbhs0_le`, `nbhs0_le`, `dnbrg0_lt`, `nbhs0_lt` + + definition `pseudometric` + + instance of `normedZmodType`, `pointedType` and `pseudoMetricType` + on `pseudometric` + + definitions `oo_norm`, `oo_space`, + + instance of `normedModType` on `oo_space` + + lemmas `oo_closed_ball_compact`, `equivalence_norms`, + `linear_findim_continuous` + +- in `num_topology.v` + + instance of `pseudoMetricType` on `GRing.regular` + +- in `uniform_structure` + + lemma `within_continuous_withinNx` + +- in `tvs.v` + + lemmas `cvg_sum`, `sum_continuous`, `entourage_nbhsE` + + instance of `UniformZmodule.type` on `GRing.regular` + ### Changed - moved from `measurable_structure.v` to `classical_sets.v`: diff --git a/_CoqProject b/_CoqProject index f0b745c7f6..d9454144e8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -42,6 +42,8 @@ experimental_reals/distr.v reals_stdlib/Rstruct.v reals_stdlib/nsatz_realtype.v +theories/unstable_analysis.v + theories/ereal.v theories/landau.v @@ -97,6 +99,7 @@ theories/trigo.v theories/esum.v theories/derive.v theories/numfun.v +theories/holomorphy.v theories/measure_theory/measurable_structure.v theories/measure_theory/measure_function.v @@ -149,6 +152,7 @@ theories/charge.v theories/kernel.v theories/pi_irrational.v theories/gauss_integral.v +theories/holomorphy.v theories/all_analysis.v diff --git a/classical/unstable.v b/classical/unstable.v index cf8b4ce04a..154accbf4d 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. From mathcomp Require Import vector archimedean interval. diff --git a/default.nix b/default.nix index ec2742873f..1d43290d34 100644 --- a/default.nix +++ b/default.nix @@ -4,8 +4,8 @@ bundle ? null, job ? null, inNixShell ? null, src ? ./., }@args: let auto = fetchGit { - url = "https://github.com/rocq-community/coq-nix-toolbox.git"; - ref = "master"; + url = "https://github.com/proux01/coq-nix-toolbox.git"; + ref = "fix530989"; rev = import .nix/coq-nix-toolbox.nix; }; in diff --git a/theories/Make b/theories/Make index 17da83d2a3..72add687e1 100644 --- a/theories/Make +++ b/theories/Make @@ -9,6 +9,8 @@ # introduced in Rocq 9.3 -arg -w -arg -rewrite-rw +unstable_analysis.v + ereal.v landau.v @@ -118,3 +120,4 @@ pi_irrational.v gauss_integral.v all_analysis.v showcase/summability.v +holomorphy.v diff --git a/theories/derive.v b/theories/derive.v index e4a340616d..15d1a900bb 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -537,6 +537,7 @@ rewrite invrK -ltr_pdivlMr // ger0_norm // ltr_pdivrMr //. by rewrite divfK ?lt0r_neq0// [ltRHS]splitr ltrDl. Qed. + Lemma diff_unique (V W : normedModType R) (f : V -> W) (df : {linear V -> W}) x : continuous df -> f \o shift x = cst (f x) + df +o_ 0 id -> @@ -565,6 +566,29 @@ rewrite [in LHS]littleo_center0 (comp_centerK x id). by rewrite -[- _ in RHS](comp_centerK x). Qed. +Lemma shift_addo (V W : normedModType R) (f l : V -> W) x : + (forall t, f t = f x + l (t - x) +o_(t \near x) (t - x)) + <-> (forall h, f (h + x) = f x + l h +o_(h \near 0) h). +Proof. +split=> [fE t|fE t]. + rewrite fE addrK; congr (_ + _). + by rewrite littleo_center0/= addrK; congr the_littleo; + apply/funext => ?/=; rewrite addrK. +rewrite -[in LHS](@subrK _ x t) fE; congr (_ + _). +by rewrite [in RHS]littleo_center0/=; congr the_littleo; + apply/funext => ?/=; rewrite addrK. +Qed. + +Lemma exists_diff (V W : normedModType R) (f : V -> W) x : + (exists2 l : {linear V -> W}, + continuous l & (forall t, f t = f x + l (t - x) +o_(t \near x) (t - x))) -> + differentiable f x. +Proof. +move=> [l cl hl]. +have fxl : 'd f x = l :> (V -> W) by exact/(diff_unique cl)/funext/shift_addo. +by apply/diffP => //=; split; rewrite fxl => // t; rewrite norm_lim_id. +Qed. + Lemma diff_cst (V W : normedModType R) a x : ('d (cst a) x : V -> W) = 0. Proof. by apply/diff_unique; have [] := dcst a x. Qed. diff --git a/theories/holomorphy.v b/theories/holomorphy.v new file mode 100644 index 0000000000..ef0cf407a6 --- /dev/null +++ b/theories/holomorphy.v @@ -0,0 +1,366 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +(*From mathcomp Require Import ssreflect ssrfun ssrbool fieldext falgebra vector. +From mathcomp Require Import ssrnat eqtype seq choice fintype bigop order. +From mathcomp Require Import ssralg ssrnum ssrfun matrix complex.*) +From mathcomp Require Import boot order algebra complex. +From mathcomp Require Import unstable_analysis boolp reals ereal derive. +From mathcomp Require Import classical_sets functions interval_inference. +From mathcomp Require Import topology normedtype landau. + +(**md**************************************************************************) +(* # Holomorphic functions *) +(* *) +(* This file develops the theory of holomorphic functions. We endow complex *) +(* (denoted C below) and Rcomplex with structures of normedModType. We prove *) +(* that the holomorphic functions are the R-differentiable functions from C *) +(* to C satisfying the Cauchy-Riemann equation. *) +(* *) +(* holomorphic f == f is holomorphic, i.e. C-derivable *) +(* Rdifferentiable f == f is differentiable on Rcomplex *) +(* CauchyRiemannEq f c == The Cauchy-Riemman equation for f at point c *) +(* *) +(******************************************************************************) + +Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) + +Import Order.TTheory GRing.Theory Num.Theory ComplexField Num.Def complex. +Local Open Scope ring_scope. +Local Open Scope classical_set_scope. +Local Open Scope complex_scope. +Import numFieldNormedType.Exports. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +HB.instance Definition _ (R : rcfType) := NormedModule.copy R[i] R[i]^o. +HB.instance Definition _ (R : rcfType) := UniformZmodule.copy R[i] R[i]^o. + +HB.instance Definition _ (R : rcfType) := UniformZmodule.copy (Rcomplex R) R[i]. +HB.instance Definition _ (R : rcfType) := Pointed.copy (Rcomplex R) R[i]. + +Module Rcomplex_NormedModType. +Section Rcomplex_NormedModType. +Variable (R : rcfType). +Import Normc. + +Definition ball_Rcomplex (R : rcfType) : (Rcomplex R) -> R -> set (Rcomplex R) := + ball_ (@normc R). + +(* beware that Re and complex.Re don't look similar *) +Lemma entourage_RcomplexE : entourage = entourage_ (@ball_Rcomplex R). +Proof. +rewrite entourage_nbhsE/= eqEsubset. +split; apply/subsetP => U; rewrite inE => -[]. + move=> V []/= e; rewrite ltcE => /andP[]/eqP/= ei0 e0. + have ->: e = (Re e)%:C by case: e ei0 {e0} => r i/= ->. + move=> /subsetP eV /subsetP VU. + rewrite inE; exists (Re e) => //. + apply/subsetP => -[] a b; rewrite inE/= /ball/= => abe. + by apply: VU; rewrite inE/=; apply: eV; rewrite inE/= add0r opprB ltcR. +move=> e/= e0 /subsetP eU. +rewrite inE; exists (ball_Rcomplex 0 e). + exists e%:C; first by rewrite /= ltcR. + by apply/subsetP => x; rewrite !inE/= ltcR. +apply/subsetP => x; rewrite inE/= inE /ball_Rcomplex/= add0r opprB => xe. +by apply: eU; rewrite inE. +Qed. + +(* Lemmas to be used generally when norm is redefined *) + +(*#[local] Lemma ler_normcD : forall (x y : Rcomplex R), normc (x + y) <= normc x + normc y. +Proof. +Admitted. + +#[local] Lemma normrcMn : forall (x : Rcomplex R) n, normc (x *+ n) = normc x *+ n. +Proof. +Admitted. + +#[local] Lemma normrcN : forall (x : Rcomplex R), normc (- x) = normc x. +Proof. +Admitted. + +HB.instance Definition _ := @Num.Zmodule_isSemiNormed.Build R (Rcomplex R) (@normc R) ler_normcD normrcMn normrcN.*) + +(*#[local] Lemma normrc0_eq0 : forall x : Rcomplex R, normc x = 0 -> x = 0. +Proof. +Admitted. + +HB.instance Definition _ := @Num.SemiNormedZmodule_isPositiveDefinite.Build R (Rcomplex R) normrc0_eq0.*) + +HB.instance Definition _ := Uniform_isPseudoMetric.Build R (Rcomplex R) + ball_norm_center ball_norm_symmetric ball_norm_triangle entourage_RcomplexE. +HB.instance Definition _ := + NormedZmod_PseudoMetric_eq.Build R (Rcomplex R) erefl. + +Lemma normcZ (l : R) (x : Rcomplex R) : `|l *: x| = `|l| * `|x|. +Proof. +by case: x => ??; rewrite /normr/= !exprMn -mulrDr sqrtrM ?sqr_ge0// sqrtr_sqr. +Qed. + +#[export] HB.instance Definition _ := + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (Rcomplex R) normcZ. + + +Lemma Rcomplex_findim : Vector.axiom 2 (Rcomplex R). +Proof. +exists (fun x => \row_(i < 2) [:: Re x; Im x]`_i). + move=> r x y; apply/rowP; move=> i /=; rewrite !mxE. + case: i => i /=; rewrite ltnS leq_eqVlt => /orP[/eqP ->/=|]. + by rewrite raddfD/= linearZ. + by rewrite ltnS leqn0 => /eqP -> /=; rewrite raddfD/= linearZ. +apply: (@Bijective _ _ _ (fun x : 'rV_2 => x ord0 ord0 +i* x ord0 ord_max)). + by case=> x y; rewrite !mxE. +move=> x; apply/rowP => i; rewrite mxE/=. +case: i => i /[dup] + ilt; rewrite ltnS leq_eqVlt => /orP[/eqP /= i1|]. + by rewrite {1}i1/=; congr (x ord0); apply: val_inj. +rewrite ltnS leqn0 => /eqP i0/=. +by rewrite {1}i0/=; congr (x ord0); apply: val_inj. +Qed. + +#[export] HB.instance Definition _ := + Lmodule_hasFinDim.Build R (Rcomplex R) Rcomplex_findim. + +End Rcomplex_NormedModType. +End Rcomplex_NormedModType. +HB.export Rcomplex_NormedModType. + + +Section Holomorphe_der. +Variable R : realType. + + +Local Notation sqrtr := Num.sqrt. +Local Notation C := R[i]. +Local Notation Rc := (Rcomplex R). +Check (Rcomplex R : normedModType R). +Check (Rcomplex R : vectType R). +Check (Rcomplex R : normedVectType R). + + +From mathcomp Require Import ssrAC. + +Lemma normRcomplex (x : R[i]) : `|x : Rc|%:C = `|x|. +Proof. +by []. +Qed. + +(* TODO : put the h at the left *) +Definition holomorphic (f : C -> C) (c : C) := + cvg ((fun (h : C) => h^-1 * (f (c + h) - f c)) @ 0^'). + + +Lemma holomorphicP (f : C -> C) (c : C) : holomorphic f c <-> derivable (f : C^o -> C^o) c 1. +Proof. +rewrite /holomorphic /derivable. +suff ->: (fun h : C => h^-1 * ((f (c + h) - f c))) = + ((fun h : C => h^-1 * ((f \o shift c) (h *: (1 : C^o)) - f c))) by []. +by apply: funext => h; rewrite complexA [X in f X]addrC. +Qed. + + +Definition Rdifferentiable (f : C -> C) (c : C) := differentiable f%:Rfun c%:RC. + +Definition realC : R -> C := (fun r => r%:C). + +Lemma continuous_realC: continuous realC. +Proof. +move=> x A /= [] r /[dup] /realC_gt0 Rer0 /gt0_realC rRe H; exists (Re r) => //. +by move=> z /= nz; apply: (H z%:C); rewrite /= -raddfB realC_norm rRe ltcR. +Qed. + +Lemma Rdiff1 (f : C -> C) (c : C) : + lim ((fun h : C => h^-1 * ((f (c + h) - f c))) @ (realC @ 0^')) + = 'D_1 (f%:Rfun) c%:RC. +Proof. +rewrite /derive. +rewrite -[LHS]/(lim ((fun h : C => h^-1 * ((f (c + h) - f c))) + \o realC @ 0^')). +suff ->: (fun h : C => h^-1 * (f (c + h) - f c)) \o realC + = fun h : R => h^-1 *: ((f \o shift c) (h *: (1%:RC)) - f c)%:RC. + by []. +apply: funext => h /=. +by rewrite -fmorphV realC_alg [X in f X]addrC /realC /= scalerc. +Qed. + +Lemma Rdiffv (f : C -> C) (v c : C) : + lim ((fun h : C => h^-1 * ((f (c + h *: (v : C^o)) - f c))) @ (realC @ 0^')) + = 'D_v (f%:Rfun) c%:RC. +Proof. +rewrite /derive. +rewrite -[LHS]/(lim ((fun h : C => h^-1 * ((f (c + h *: (v : C^o)) - f c))) + \o realC @ 0^')). +suff ->: (fun h : C => h^-1 * (f (c + h *: (v : C^o)) - f c)) \o realC + = fun h : R => h^-1 *: ((f \o shift c) (h *: (v:Rc)) - f c)%:RC. + by []. +apply: funext => h /=. +by rewrite -fmorphV [X in f X]addrC /realC /= scalerc scalerc_regular. (*-scaleCE*) +Qed. + +Lemma Cdiff1 (f : C -> C) (c : C) : + lim ((fun h : C => h^-1 * ((f (h + c) - f c))) @ 0^') + = 'D_1 (f : C^o -> C^o) c. +Proof. +rewrite /derive. +rewrite -[LHS]/(lim ((fun h : C => h^-1 * ((f (h + c) - f c))) @ 0^')). +suff ->: (fun h : C => h^-1 * (f (h + c) - f c)) + = (fun h : C => h^-1 *: (( (f : C^o -> C^o) \o shift c) (h *: 1 : C^o) - f c) : C^o). + by []. +apply: funext => h /=. +by rewrite scalecE scaler1. +Qed. + + +Lemma Rdiffi (f : C^o -> C^o) c: + lim ((fun h : C => h^-1 * ((f (c + h * 'i) - f c))) @ (realC @ 0^')) + = 'D_('i) (f%:Rfun) c%:RC. +Proof. +rewrite /derive. +rewrite -[LHS]/(lim ((fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) + \o realC @ 0^')). +suff -> : (fun h : (R[i]) => h^-1 * (f (c + h * 'i) - f c)) \o realC + = fun h : R => h^-1 *: ((f \o shift c) (h *: ('i%:RC)) - f c)%:RC. + by []. +apply: funext => h /=. +by rewrite -fmorphV scalerc [X in f X]addrC scalerc. +Qed. + +Definition CauchyRiemannEq (f : C -> C) c := + 'i * 'D_1 f%:Rfun c%:RC = 'D_('i) f%:Rfun c%:RC. + + +Lemma is_derive_holo (f : C -> C) (c : C) : + Rdifferentiable f c -> CauchyRiemannEq f c -> + is_derive (c : C^o) 1 (f : C^o -> C^o) ('D_1 (f%:Rfun) c%:RC). Proof. +move => fdiff CR. +suff lem: (h^-1 * (f (h + c) - f c) @[h --> 0^']) --> 'D_1 (f%:Rfun) (c%:RC). + split; last first. + by rewrite -Cdiff1; apply: cvg_lim lem; by []. + apply/cvg_ex. eexists. rewrite /=. under eq_fun do rewrite scaler1/=. exact: lem. +move => /= A. + move => [/= _ /posnumP [r]] /=; rewrite /ball_ /= => H. + near_simpl. + near=> t. + apply: H => /=. + rewrite deriveE => //. + rewrite [f _](@diff_locallyx R Rc Rc) => //=. + rewrite (ACl (1*4*2*3)) /= subrr add0r. + have -> : 'd (f%:Rfun) (c%:RC) (t : Rc) = t * 'd (f%:Rfun) (c%:RC) (1: Rc). + rewrite (complexE t). + rewrite !linearD. + have <- := scalec1 (Re t). + have := scalerc (Im t) 'i%C. + rewrite mulrC => <-. + rewrite !linearZ -!deriveE // -CR /= !scalerc_regular scalerA. + by rewrite -(scalerDl ('D_1 f%:Rfun c : C^o)) !scalecE mulr1. + rewrite mulrDr mulKf //. + by near:t; exact: nbhs_dnbhs_neq. + rewrite opprD addNKr normrN. + near: t. + case: littleo. + move => h /= H. + near=> t. + rewrite normrM normfV ltr_pdivrMl. + by rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. + rewrite (@le_lt_trans _ _ ((r%:num/2 * `|t|))) //. + rewrite -!normRcomplex [r%:num/2]gt0_normc // -rmorphM /= lecR. + near: t; apply: nbhs_dnbhs; near_simpl. + apply: H => //. + rewrite -[Normc.normc _]/(`|_ : Rc|) . + by rewrite normr_gt0. + rewrite mulrC ltr_pM2l //. + by rewrite normr_gt0; near: t; apply: nbhs_dnbhs_neq. + by rewrite gtr_pMr // invf_lt1 // ?ltr1n //. +Unshelve. all: by end_near. +Qed. + +Lemma diff_CR_holo (f : C -> C) (c : C): + Rdifferentiable f c -> CauchyRiemannEq f c -> holomorphic f c. +Proof. +by move=> /is_derive_holo /[apply] ?; exact/holomorphicP. +Qed. + + +Lemma eqaddoPx {K : numDomainType} {T : Type} {V W : normedModType K} + (F : filter_on T) (f g : T -> V) (e : T -> W) : +(forall x, f x = g x +o_(x \near F) e x) <-> + forall eps : K, 0 < eps -> \near F, `|(f - g) F| <= eps * `|e F|. +Proof. +rewrite -eqaddoP; split=> [fE|->]; last exact/eqaddoEx. +by apply/funext=> x; rewrite fctE. +Qed. + +Lemma holo_differentiable (f : C -> C) (c v : C): + holomorphic f c -> Rdifferentiable f c. +Proof. +move => /holomorphicP/derivable1_diffP fdiff. +rewrite /Rdifferentiable. +pose df (v : Rc) : Rc := 'd (f : C^o -> C^o) (c : C^o) v. +have lindf : linear df. + by move=> /= k x y; rewrite !scalerc /df /= linearP. +pose Df : {linear Rc -> Rc} := HB.pack df (@GRing.isLinear.Build _ _ _ _ df lindf). +apply: (exists_diff); exists Df; first exact: linear_findim_continuous. +rewrite /Df /df /=; apply/eqaddoPx => r r0; near=> w. +have /diff_locallyxP [_ ] := fdiff. +move => /(_ (w - c)); rewrite !fctE subrK => ->. +rewrite opprD (AC (3*2) ((1*4)*(2*5)*3)) /= !subrr !add0r. +near: w; case : littleo => /= h heps; near=> w. +rewrite -lecR rmorphM /= !normRcomplex; near: w. +suff: \forall x \near c, `|h (x - c)| <= r%:C * `|x - c| by exact. +apply/nbhs0P; near do rewrite addrC addKr; apply: heps. +by rewrite ltcR. +Unshelve. all: end_near. Qed. + + +Lemma holo_CauchyRiemann (f : C -> C) c: holomorphic f c -> CauchyRiemannEq f c. +Proof. +move=> /cvg_ex; rewrite //= /CauchyRiemannEq. rewrite -Rdiff1 -Rdiffi. +set quotC : C -> C := fun h : R[i] => h^-1 * (f (c + h) - f c). +set quotR : C -> C:= fun h => h^-1 *: ((f (c + h * 'i) - f c) : C^o) . +move => /= [l H]. +have -> : quotR @ (realC @ 0^') = (quotR \o realC) @ 0^' by []. +have realC'0: realC @ 0^' --> 0^'. + rewrite -[0 in X in _ --> X]/(realC 0). + apply: within_continuous_withinNx; first by apply: continuous_realC. + by move => /= x /complexI. +have HR0:(quotC \o (realC) @ 0^') --> l. + by apply: cvg_comp; last by exact: H. +have lem : quotC \o *%R^~ 'i%R @ (realC @ (0 : R)^') --> l. + apply: cvg_comp; last by exact: H. + apply: (@cvg_comp _ _ _ realC ( *%R^~ 'i)); first by exact: realC'0. + rewrite -[0 in X in _ `=>` X](mul0r 'i%C). + apply: within_continuous_withinNx; first by apply: mulrr_continuous. + move=> x /eqP; rewrite mul0r mulIr_eq0; first by apply/rregP; apply: neq0Ci. + exact: eqP. +have HRcomp: cvg (quotC \o *%R^~ 'i%R @ (realC @ ((0 : R)^'))). + by apply/cvg_ex; simpl; exists l. +have ->: lim (quotR @ (realC @ ((0 : R)^'))) + = 'i * lim (quotC \o ( fun h => h *'i) @ (realC @ ((0 : R)^'))). + have: (fun x => 'i) \* quotC \o ( fun h => h *'i) =1 quotR. + move=> h /=; rewrite /quotC /quotR /=. + rewrite invfM mulrA (mulrC _ ('i)^-1) mulrA divff ?complexiE ?neq0Ci //. + by rewrite mul1r scalecE. + move=> /funext <-. rewrite limM ?lim_cst. + by []. + exact: cvg_cst. + by []. + by []. + by []. +suff ->: lim (quotC @ (realC @ ((0 : R)^'))) + = lim (quotC \o *%R^~ 'i%R @ (realC @ ((0 : R)^'))) by []. +suff ->: lim (quotC @ (realC @ ((0 : R)^'))) = l. + by apply/eqP; rewrite eq_sym; apply/eqP; apply: (cvg_lim _ lem). +by apply: cvg_lim; last exact: HR0. +Qed. + + +Lemma holomorphic_Rdiff (f : C -> C) (c : C) : + (Rdifferentiable f c) /\ (CauchyRiemannEq f c) <-> (holomorphic f c). +Proof. +split; first by move => [Rdiff CR]; exact: diff_CR_holo. +split; first by exact: holo_differentiable. +by exact: holo_CauchyRiemann. +Qed. + +End Holomorphe_der. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 31c99d1a4f..9c77c159ba 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -508,6 +508,36 @@ Proof. by move=> k; apply: (cvg_comp2 cvg_id (cvg_cst _) (scale_continuous _ _ (_, _))). Qed. +Lemma dnbhs0_le e : + 0 < e -> \forall x \near (0 : V)^', `|x| <= e. +Proof. +move=> e_gt0; apply/nbhs_ballP; exists e => // x. +rewrite -ball_normE /= sub0r normrN => le_nxe _ . +by rewrite ltW. +Qed. + +Lemma nbhs0_le e : + 0 < e -> \forall x \near (0 : V)^', `|x| <= e. +Proof. +move=> e_gt0; apply/nbhs_ballP; exists e => // x. +rewrite -ball_normE /= sub0r normrN => le_nxe _ . +by rewrite ltW. +Qed. + +Lemma dnbhs0_lt e : + 0 < e -> \forall x \near (0 : V)^', `|x| < e. +Proof. +move=> e_gt0; apply/nbhs_ballP; exists e => // x. +by rewrite -ball_normE /= sub0r normrN. +Qed. + +Lemma nbhs0_lt e : + 0 < e -> \forall x \near (0 : V)^', `|x| < e. +Proof. +move=> e_gt0; apply/nbhs_ballP; exists e => // x. +by rewrite -ball_normE /= sub0r normrN. +Qed. + End NormedModule_numFieldType. Arguments cvg_at_rightE {K V} f x. Arguments cvg_at_leftE {K V} f x. @@ -2568,9 +2598,61 @@ Proof. by rewrite /open_disjoint_itv; case: cid => //= I [_]. Qed. End open_set_disjoint_real_intervals. +(* equip a normedZmodType with a structure of normed module *) + +Definition pseudometric (K : numFieldType) (M : normedZmodType K) : Type := M. + +HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) := + Choice.on (pseudometric M). +HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) := + Num.NormedZmodule.on (pseudometric M). +HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) := + isPointed.Build M 0. + +Section isnormedmodule. +Variables (K : numFieldType) (M' : normedZmodType K). + +Notation M := (pseudometric M'). + +Local Definition ball (x : M) (r : K) : set M := ball_ Num.norm x r. + +Local Definition ent : set_system (M * M) := + entourage_ ball. + +Local Definition nbhs (x : M) : set_system M := + nbhs_ ent x. + +Local Lemma nbhsE : nbhs = nbhs_ ent. Proof. by []. Qed. + +HB.instance Definition _ := hasNbhs.Build M nbhs. + +Local Lemma ball_center x (e : K) : 0 < e -> ball x e x. +Proof. by rewrite /ball/= subrr normr0. Qed. + +Local Lemma ball_sym x y (e : K) : ball x e y -> ball y e x. +Proof. by rewrite /ball /= distrC. Qed. + +Local Lemma ball_triangle x y z e1 e2 : ball x e1 y -> ball y e2 z -> + ball x (e1 + e2) z. +Proof. +rewrite /ball /= => ? ?. +rewrite -[x](subrK y) -(addrA (x + _)). +by rewrite (le_lt_trans (ler_normD _ _))// ltrD. +Qed. + +Local Lemma entourageE : ent = entourage_ ball. +Proof. by []. Qed. + +HB.instance Definition _ := @Nbhs_isPseudoMetric.Build K M + ent nbhsE ball ball_center ball_sym ball_triangle entourageE. + +End isnormedmodule. + Section EquivalenceNorms. Variables (R : realType). +(* TODO : generalize to a numFieldType *) + (* FIXME: Specialize to vector space with basis and expose this definition (see https://github.com/math-comp/analysis/issues/1911). It will also be possible to generalize to `numFieldType`. *) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 41126a781d..978bf936cd 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -20,7 +20,6 @@ From mathcomp Require Import pseudometric_normed_Zmodule. (* PreTopologicalNmodule == HB class, join of Topological and Nmodule *) (* TopologicalNmodule == HB class, PreTopologicalNmodule with a *) (* continuous addition *) -(* PreTopologicalZmodule == HB class, join of Topological and Zmodule *) (* topologicalZmodType == topological abelian group *) (* TopologicalZmodule == HB class, join of TopologicalNmodule and *) (* Zmodule with a continuous opposite operator *) @@ -344,6 +343,27 @@ exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split. by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)). Qed. +Lemma entourage_nbhsE : @entourage M = filter_from (nbhs 0) (fun X => [set x | x.2 - x.1 \in X]). +Proof. +have map_uniform (T U : uniformType) (S : set (U * U)%type) (f : T * T -> U) : unif_continuous f -> entourage S -> exists ST : set (T * T)%type, entourage ST /\ {in ST, forall x, forall y, (f (x.1, y), f (x.2, y)) \in S}. + move=> fu /fu [[]]/= ST1 ST2 [] ? ? /subsetP STf. + exists ST1; split=> // x xST1 y. + have /STf: (x, (y, y)) \in ST1 `*` ST2. + rewrite in_setX xST1/= unfold_in/=. + apply/asboolT. + exact: entourage_refl. + rewrite in_setE/= => -[] [] [] a1 a2 [] b1 b2 /= abS [] <- {2}<- <-/=. + exact: asboolT. +rewrite eqEsubset; split; apply/subsetP => U; rewrite !inE /filter_from/=. + move=> /(map_uniform _ _ _ _ sub_unif_continuous)/= [] V [] Ve VU. + exists (xsection V 0); first exact: nbhs_entourage. + apply/subsetP => [] [] x y; rewrite inE/= mem_xsection => /VU/(_ (-x))/=. + by rewrite opprK -addrA addNr add0r addr0. +move=> [] V /nbhsP[] U' /(map_uniform _ _ _ _ add_unif_continuous)/= [] W [] We WU' /subsetP U'V /subsetP VU. +apply/(filterS _ We)/subsetP => -[] a b /WU'/=/(_ (-a)); rewrite subrr => abU'. +by apply/VU; rewrite inE/=; apply: U'V; rewrite mem_xsection. +Qed. + End UniformZmoduleTheory. HB.structure Definition PreUniformLmodule (K : numDomainType) := @@ -708,7 +728,6 @@ Qed. Let standard_locally_convex_set : exists2 B : set_system R^o, (forall b, b \in B -> convex_set b) & basis B. -Proof. exists [set B | exists x r, B = ball x r]. by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex_set. split; first by move=> B [x] [r] ->; exact: ball_open. @@ -716,8 +735,19 @@ move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. by exists (ball x r) => //=; split; [exists x, r|exact: ballxx]. Qed. +Local Lemma standard_sub_unif_continuous : unif_continuous (fun x : R^o * R^o => x.1 - x.2). +Proof. +move=> /= U; rewrite /nbhs/= -!entourage_ballE => -[]/= e e0 /subsetP eU. +exists (e / 2) => /=; first exact: divr_gt0. +apply/subsetP => -[] [] a1 a2 [] b1 b2/=; rewrite inE/= => -[]/=. +rewrite /ball/= => abe1 abe2. +apply: eU => /=; rewrite inE/= /ball/= opprD addrACA -opprD. +by rewrite (le_lt_trans (ler_normB _ _))// (splitr e) ltrD. +Qed. + HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build R^o standard_add_continuous. +HB.instance Definition _ := PreUniformNmodule_isUniformZmodule.Build R^o standard_sub_unif_continuous. HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R R^o standard_scale_continuous. HB.instance Definition _ := diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v index 44e5ce8742..c821fac598 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.v @@ -297,6 +297,26 @@ by apply/seteqP; split=> y/=; have /contra_neq /(_ yx) := fI y; tauto. Qed. +Lemma within_continuous_withinNx + (T U : topologicalType) (f : T -> U) (x : T) : + {for x, continuous f} -> + (forall y, f y = f x -> y = x) -> f @ x^' --> (f x)^'. +Proof. +move=> cf fI A. +rewrite /nbhs /= /dnbhs !withinE/= => -[] V Vfx AV. +move: (cf _ Vfx); rewrite /nbhs/= -/(nbhs _ _) => Vx. +exists (f @^-1` V) => //. +apply/seteqP; split=> y/= [] fyAV yx; split=> //. + suff: f y \in A `&` (fun y : U => y != f x). + by rewrite AV inE => -[]. + rewrite inE/=; split=> //. + by move: yx; apply: contra => /eqP /fI /eqP. +suff: f y \in V `&` (fun y : U => y != f x). + by rewrite -AV inE => -[]. +rewrite inE/=; split=> //. +by move: yx; apply: contra => /eqP /fI /eqP. +Qed. + (* This property is primarily useful for metrizability on uniform spaces *) Definition countable_uniformity (T : uniformType) := exists R : set_system (T * T), [/\ diff --git a/theories/unstable_analysis.v b/theories/unstable_analysis.v new file mode 100644 index 0000000000..ef68b32b13 --- /dev/null +++ b/theories/unstable_analysis.v @@ -0,0 +1,157 @@ +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. +From mathcomp Require Import vector archimedean interval complex. +From mathcomp.classical Require Export unstable. + +(**md**************************************************************************) +(* # MathComp extra *) +(* *) +(* This files contains lemmas that should eventually be backported *) +(* to mathcomp. These lemmas may change before being backported to mathcomp, *) +(* don't use anything in this file outside of Analysis. For this same reason, *) +(* nothing in this file should be mentionned in the changelog. *) +(* Once a result is backported to mathcomp, please move it to mathcomp_extra.v*) +(* and mention it in the changelog. *) +(******************************************************************************) + +Attributes warn(note="The unstable_analysis.v file should only be used inside analysis.", + cats="internal-analysis"). + +Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Theory. +Local Open Scope complex_scope. +Local Open Scope ring_scope. + +Notation "f %:Rfun" := (f : (Rcomplex _) -> (Rcomplex _)) + (at level 5, format "f %:Rfun") : complex_scope. + +Notation "v %:RC" := (v : (Rcomplex _)) + (at level 5, format "v %:RC") : complex_scope. + +(* TODO: backport to real-closed *) +Section complex_extras. +Variable R : rcfType. +Local Notation sqrtr := Num.sqrt. +Local Notation C := (Rcomplex R). + +Import Normc. +Import Num.Def. +Import complex. + +(*TODO : rename scale regular and put there*) +Lemma scalecE (w v: C^o) : v *: w = v * w. +Proof. by []. Qed. + +Lemma scalerc (h : R) (c : C) : h *: (c : Rcomplex R) = h%:C * c. +Proof. +case : c => x y. +by rewrite /(real_complex _) /(_ *: _) /( _ * _) /= /= /scalec !mul0r subr0 addr0. +Qed. + +(* FIXME: unused *) +Lemma normcr (x : R) : normc (x%:C) = normr x. +Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. + +Lemma Im_mul (x : R) : x *i = x%:C * 'i%C. +Proof. by simpc. Qed. + +Lemma mulrnc (a b : R) k : a +i* b *+ k = (a *+ k) +i* (b *+ k). +Proof. +by elim: k => // k ih; apply/eqP; rewrite !mulrS eq_complex !ih !eqxx. +Qed. + +Lemma complexA (h : C^o) : h%:A = h. +Proof. by rewrite scalecE mulr1. Qed. + +Lemma normc_natmul (k : nat) : normc k%:R = k%:R :> R. +Proof. by rewrite mulrnc /= mul0rn expr0n addr0 sqrtr_sqr normr_nat. Qed. + +Lemma normc_mulrn (x : C) k : normc (x *+ k) = (normc x) *+ k. +Proof. +by rewrite -mulr_natr normcM -[in RHS]mulr_natr normc_natmul. +Qed. + +Lemma gt0_normc (r : C) : 0 < r -> r = (normc r)%:C. +Proof. +case: r => x y /= /andP[] /eqP -> x0. +by rewrite expr0n addr0 sqrtr_sqr gtr0_norm. +Qed. + +Lemma gt0_realC (r : C) : 0 < r -> r = (Re r)%:C. +Proof. by case: r => x y /andP[] /eqP -> _. Qed. + +Lemma ltc0E (k : R): (0 < k%:C) = (0 < k). +Proof. by simpc. Qed. + +Lemma ltc0P (k : R): (0 < k%:C) <-> (0 < k). +Proof. by simpc. Qed. + +Lemma ltcP (k t: R): (t%:C < k%:C) <-> (t < k). +Proof. by simpc. Qed. + +Lemma lecP (k t: R): (t%:C <= k%:C) <-> (t <= k). +Proof. by simpc. Qed. + +(* (*TBA algC *) *) +Lemma realC_gt0 (d : C) : 0 < d -> (0 < Re d :> R). +Proof. by rewrite ltcE => /andP [] //. Qed. + +Lemma Creal_gtE (c d : C) : c < d -> (complex.Re c < complex.Re d). +Proof. by rewrite ltcE => /andP [] //. Qed. + +Lemma realC_norm (b : R) : `|b%:C| = `|b|%:C. +Proof. by rewrite normc_def /= expr0n addr0 sqrtr_sqr. Qed. + +Lemma eqCr (r s : R) : (r%:C == s%:C) = (r == s). +Proof. exact: (inj_eq (@complexI _)). Qed. + +Lemma eqCI (r s : R) : (r *i == s *i) = (r == s). +Proof. by apply/idP/idP => [/eqP[] ->//|/eqP ->]. Qed. + +Lemma neqCr0 (r : R) : (r%:C != 0) = (r != 0). +Proof. by apply/negP/negP; rewrite ?eqCr. Qed. + +Lemma real_normc_ler (x : C) : + `|Re x| <= normc x. +Proof. +case: x => x y /=. +rewrite -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. +rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. +by rewrite lerDl ?sqr_ge0. +Qed. + +Lemma im_normc_ler (x : C) : + `|Im x| <= normc x. +Proof. +case: x => x y /=. +rewrite -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //. +rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=. +by rewrite lerDr ?sqr_ge0. +Qed. + +Lemma realC_alg (a : R) : a *: (1%:RC) = a%:C. +Proof. by rewrite /GRing.scale/= mulr1 mulr0. Qed. + +Lemma scalecV (h: R) (v: Rcomplex R): + h != 0 -> v != 0 -> (h *: v)^-1 = h^-1 *: v^-1. (* scaleCV *) +Proof. +by move=> h0 v0; rewrite scalerc invrM // ?unitfE ?eqCr // mulrC scalerc fmorphV. +Qed. + +(* TODO: clean lemmas about scalec *) +Lemma scalerc_regular (h : R) (c : R[i]): h *: (c : Rcomplex R) = h%:C *: (c : C^o). +Proof. +by rewrite scalecE scalerc. +Qed. + +Lemma scalec1 (h : R) : h *: (1 : C^o) = h%:C. +Proof. +by rewrite scalerc mulr1. +Qed. + +End complex_extras.