From 17060bc5e373ca7d41348c1cb1b1522bdd4b0af1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Iv=C3=A1n=20Renison?= <85908989+IvanRenison@users.noreply.github.com> Date: Sat, 13 Jun 2026 01:31:30 +0000 Subject: [PATCH 01/24] feat(Combinatorics/SimpleGraph/Maps): add theorems about composition (#37624) --- Mathlib/Combinatorics/SimpleGraph/Maps.lean | 35 ++++++++++++++++++--- 1 file changed, 31 insertions(+), 4 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Maps.lean b/Mathlib/Combinatorics/SimpleGraph/Maps.lean index a4d9325a549275..3fbde0b4f959eb 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Maps.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Maps.lean @@ -45,7 +45,7 @@ open Function namespace SimpleGraph -variable {V W X : Type*} (G : SimpleGraph V) (G' : SimpleGraph W) {u v : V} +variable {V W X Y : Type*} (G : SimpleGraph V) (G' : SimpleGraph W) {u v : V} /-! ## Map and comap -/ @@ -420,7 +420,7 @@ theorem le_comap (f : H →g G) : H ≤ G.comap f := theorem nonempty_hom_iff_exists_le_comap : Nonempty (H →g G) ↔ ∃ f, H ≤ G.comap f := ⟨fun ⟨f⟩ ↦ ⟨f, f.le_comap⟩, fun ⟨f, h⟩ ↦ ⟨f, (h ·)⟩⟩ -variable {G'' : SimpleGraph X} +variable {G'' : SimpleGraph X} {G''' : SimpleGraph Y} /-- Composition of graph homomorphisms. -/ abbrev comp (f' : G' →g G'') (f : G →g G') : G →g G'' := @@ -430,6 +430,15 @@ abbrev comp (f' : G' →g G'') (f : G →g G') : G →g G'' := theorem coe_comp (f' : G' →g G'') (f : G →g G') : ⇑(f'.comp f) = f' ∘ f := rfl +theorem comp_assoc (f : G'' →g G''') (g : G' →g G'') (h : G →g G') : + f.comp (g.comp h) = (f.comp g).comp h := rfl + +@[simp] +theorem comp_id (f : G →g G') : f.comp .id = f := rfl + +@[simp] +theorem id_comp (f : G →g G') : .comp .id f = f := rfl + @[simp] theorem comp_comap_ofLE (f : H →g G) : .comp (.comap f G) (.ofLE f.le_comap) = f := rfl @@ -533,7 +542,7 @@ protected def completeGraph {α β : Type*} (f : α ↪ β) : completeGraph α @[simp] lemma coe_completeGraph {α β : Type*} (f : α ↪ β) : ⇑(Embedding.completeGraph f) = f := rfl -variable {G'' : SimpleGraph X} +variable {G'' : SimpleGraph X} {G''' : SimpleGraph Y} /-- Composition of graph embeddings. -/ abbrev comp (f' : G' ↪g G'') (f : G ↪g G') : G ↪g G'' := @@ -543,6 +552,15 @@ abbrev comp (f' : G' ↪g G'') (f : G ↪g G') : G ↪g G'' := theorem coe_comp (f' : G' ↪g G'') (f : G ↪g G') : ⇑(f'.comp f) = f' ∘ f := rfl +theorem comp_assoc (f : G'' ↪g G''') (g : G' ↪g G'') (h : G ↪g G') : + f.comp (g.comp h) = (f.comp g).comp h := rfl + +@[simp] +theorem comp_refl (f : G ↪g G') : f.comp .refl = f := rfl + +@[simp] +theorem refl_comp (f : G ↪g G') : .comp .refl f = f := rfl + /-- Graph embeddings from `G` to `H` are the same thing as graph embeddings from `Gᶜ` to `Hᶜ`. -/ def complEquiv : G ↪g H ≃ Gᶜ ↪g Hᶜ where toFun f := ⟨f.toEmbedding, by simp⟩ @@ -713,7 +731,7 @@ theorem toEmbedding_completeGraph {α β : Type*} (f : α ≃ β) : (Iso.completeGraph f).toEmbedding = Embedding.completeGraph f.toEmbedding := rfl -variable {G'' : SimpleGraph X} +variable {G'' : SimpleGraph X} {G''' : SimpleGraph Y} /-- Composition of graph isomorphisms. -/ abbrev comp (f' : G' ≃g G'') (f : G ≃g G') : G ≃g G'' := @@ -723,6 +741,15 @@ abbrev comp (f' : G' ≃g G'') (f : G ≃g G') : G ≃g G'' := theorem coe_comp (f' : G' ≃g G'') (f : G ≃g G') : ⇑(f'.comp f) = f' ∘ f := rfl +theorem comp_assoc (f : G'' ≃g G''') (g : G' ≃g G'') (h : G ≃g G') : + f.comp (g.comp h) = (f.comp g).comp h := rfl + +@[simp] +theorem comp_refl (f : G ≃g G') : f.comp .refl = f := rfl + +@[simp] +theorem refl_comp (f : G ≃g G') : .comp .refl f = f := rfl + section induce variable {s : Set V} {t : Set W} {r : Set X} From 1680840431e25235216ab3384877c76f073e24a6 Mon Sep 17 00:00:00 2001 From: Bingyu Xia <71547343+BryceT233@users.noreply.github.com> Date: Sat, 13 Jun 2026 09:53:21 +0000 Subject: [PATCH 02/24] feat(RingTheory/Extension): `h1CotangentEquivCotangent` (#39520) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Given `Algebra R S` and an extension `P : Extension R S`, this PR adds `extendScalars` (viewing `P` as an extension of `S` over `P.Ring`), `defaultHom` (the canonical extension homomorphism from the universal extension `R[S] → S` to `P`) and some related linear equivalences on cotangent spaces or the first homology of the naive cotangent complexes. We show the commutativity of the following diagram: 交换图latex Co-authored-by: @chrisflav --- Mathlib.lean | 1 + .../RingTheory/Extension/Cotangent/Basic.lean | 11 ++ .../RingTheory/Extension/ExtendScalars.lean | 167 ++++++++++++++++++ Mathlib/RingTheory/Extension/Generators.lean | 13 ++ Mathlib/RingTheory/Kaehler/JacobiZariski.lean | 5 + 5 files changed, 197 insertions(+) create mode 100644 Mathlib/RingTheory/Extension/ExtendScalars.lean diff --git a/Mathlib.lean b/Mathlib.lean index 2ac87fdbac13e4..09b8c19e674791 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6491,6 +6491,7 @@ public import Mathlib.RingTheory.Extension.Cotangent.Basic public import Mathlib.RingTheory.Extension.Cotangent.Basis public import Mathlib.RingTheory.Extension.Cotangent.Free public import Mathlib.RingTheory.Extension.Cotangent.LocalizationAway +public import Mathlib.RingTheory.Extension.ExtendScalars public import Mathlib.RingTheory.Extension.Generators public import Mathlib.RingTheory.Extension.Presentation.Basic public import Mathlib.RingTheory.Extension.Presentation.Core diff --git a/Mathlib/RingTheory/Extension/Cotangent/Basic.lean b/Mathlib/RingTheory/Extension/Cotangent/Basic.lean index e389a24689ec0e..0f6e4172bbc0d5 100644 --- a/Mathlib/RingTheory/Extension/Cotangent/Basic.lean +++ b/Mathlib/RingTheory/Extension/Cotangent/Basic.lean @@ -68,6 +68,12 @@ def cotangentComplex : P.Cotangent →ₗ[S] P.CotangentSpace := lemma cotangentComplex_mk (x) : P.cotangentComplex (.mk x) = 1 ⊗ₜ .D _ _ x := rfl +lemma Cotangent.mk_C_mem_ker_cotangentComplex {σ : Type*} (G : Generators R S σ) + {r : R} (hr : C r ∈ G.ker) : + Extension.Cotangent.mk ⟨C r, hr⟩ ∈ G.toExtension.cotangentComplex.ker := by + have : D R G.toExtension.Ring (C r) = 0 := Derivation.map_algebraMap .. + simp [this] + section baseChange variable {A : Type*} [CommRing A] [Algebra S A] [Algebra P.Ring A] [IsScalarTower P.Ring S A] @@ -435,6 +441,11 @@ def H1Cotangent.equiv {P₁ P₂ : Extension R S} (f₁ : P₁.Hom P₂) (f₂ : rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ (f₁.comp f₂), Extension.H1Cotangent.map_comp]; rfl +omit [IsScalarTower R S S'] in +lemma Cotangent.map_comp_h1Cotangentι (f : P.Hom P') : + Cotangent.map f ∘ₗ P.h1Cotangentι = + P'.h1Cotangentι.restrictScalars S ∘ₗ H1Cotangent.map f := rfl + end Extension namespace Generators diff --git a/Mathlib/RingTheory/Extension/ExtendScalars.lean b/Mathlib/RingTheory/Extension/ExtendScalars.lean new file mode 100644 index 00000000000000..0037ec8ed4ea75 --- /dev/null +++ b/Mathlib/RingTheory/Extension/ExtendScalars.lean @@ -0,0 +1,167 @@ +/- +Copyright (c) 2024 Bingyu Xia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bingyu Xia +-/ +module + +public import Mathlib.RingTheory.Kaehler.JacobiZariski + +/-! +# Extension of Scalars for Algebra Extensions + +This file provides APIs for extending the base ring of an algebra extension `P : Extension R S` +to its own extension ring `P.Ring`. We introduce canonical maps and isomorphisms between +the cotangent spaces and the first homology of naive cotangent complex associated with +`P.extendScalars` and `P`. We provide commutativity results of these maps and ismorphisms +(See https://github.com/leanprover-community/mathlib4/pull/39520 for an image of the full diagram). +In particular, we show the boundary map of the Jacobi-Zariski sequence of `R → P.Ring → S` +coincides with `P.cotangentComplex` via a canonical isomorphism `P.h1CotangentEquivCotangent`. + +## Main definitions and results + +- `extendScalars`: Views `P : Extension R S` as `Extension P.Ring S`. +- `toExtendScalars`: The canonical homomorphism from `P` to `P.extendScalars` induced by + the identity map on the underlying extension rings. +- `cotangentExtendScalarsEquiv` : The linear equivalence between the cotangent spaces of + `P.extensScalars` and `P` induced by the identity map. +- `h1CotangentExtendScalarsEquiv`: `P.extensScalars` can be used to compute the first homology of + the naive cotangent complex of `S` over `P.Ring`. +- `h1CotangentEquivOfSurjective`: If `R → P.Ring` is surjective, this is the linear isomorphism + induced by `P.h1Cotangentι`. +- `h1CotangentEquivCotangent`: This is the linear equivalence between `H1Cotangent P.Ring S` and + `P.Cotangent` defined by the composition of `h1CotangentExtendScalarsEquiv.symm`, + `h1CotangentEquivOfSurjective` and `cotangentExtendScalarsEquiv`. +- `cotangentComplex_comp_h1CotangentEquivCotangent`, + `h1CotangentEquivCotangent_comp_map`: commutativity results. + +-/ + +@[expose] public section + +open KaehlerDifferential + +namespace Algebra.Extension + +universe w v u + +variable {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] + +/-- Given an extension `P` of `S` over `R`, `P.extendScalars` is the same extension +but viewed as an extension of `S` over `P.Ring`. -/ +@[simps] +def extendScalars {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] + (P : Extension.{w} R S) : Extension P.Ring S where + Ring := P.Ring + σ := P.σ + algebraMap_σ := P.algebraMap_σ + +set_option backward.isDefEq.respectTransparency false in +set_option backward.defeqAttrib.useBackward true in +/-- The canonical homomorphism from `P` to `P.extendScalars` induced by the identity map +on the underlying extension rings. -/ +@[simps!] +noncomputable +def toExtendScalars {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] + (P : Extension.{w} R S) : P.Hom P.extendScalars := + .ofAlgHom (IsScalarTower.toAlgHom R P.Ring P.extendScalars.Ring) + (by dsimp; ext; simp) + +/-- `Extension.extendScalars` does not change the cotangent space of an extension. -/ +noncomputable +def cotangentExtendScalarsEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] + [Algebra R S] (P : Extension.{w} R S) : + P.extendScalars.Cotangent ≃ₗ[S] P.Cotangent := + LinearEquiv.refl _ _ + +@[simp] +lemma cotangentExtendScalarsEquiv_symm_toLinearMap (P : Extension.{w} R S) : + P.cotangentExtendScalarsEquiv.symm.toLinearMap = Cotangent.map P.toExtendScalars := by + ext x + obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x + rfl + +set_option backward.isDefEq.respectTransparency false in +theorem H1Cotangent.map_toExtendScalars_injective (P : Extension.{w} R S) : + Function.Injective (H1Cotangent.map P.toExtendScalars) := by + rw [← LinearMap.ker_eq_bot, H1Cotangent.map, LinearMap.ker_restrict, + ← cotangentExtendScalarsEquiv_symm_toLinearMap, LinearEquiv.ker, + Submodule.comap_bot, Submodule.ker_subtype] + +/-- The first homology of the naive cotangent complex of `P.extendScalars` is +linearly equivalent to that of `S` over `P.Ring`. -/ +@[simps! toLinearMap] +noncomputable +def h1CotangentExtendScalarsEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] + [Algebra R S] (P : Extension.{w} R S) : + P.extendScalars.H1Cotangent ≃ₗ[S] H1Cotangent P.Ring S := + Extension.H1Cotangent.equiv + (.ofAlgHom (Algebra.ofId _ _) (by ext)) P.extendScalars.defaultHom + +@[simp] +lemma h1CotangentExtendScalarsEquiv_symm_toLinearMap (P : Extension.{w} R S) : + P.h1CotangentExtendScalarsEquiv.symm = H1Cotangent.map P.extendScalars.defaultHom := rfl + +/-- Given an extension `P` of `S` over `R` such that `algebraMap R P.Ring` is surjective, +this is the equivalence induced by `P.h1Cotangentι`. -/ +@[simps! toLinearMap] +noncomputable +def h1CotangentEquivOfSurjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] + [Algebra R S] (P : Extension.{w} R S) (h : Function.Surjective (algebraMap R P.Ring)) : + P.H1Cotangent ≃ₗ[S] P.Cotangent where + __ := P.h1Cotangentι + invFun x := ⟨x, by + have : Subsingleton Ω[P.Ring⁄R] := subsingleton_of_surjective R P.Ring h + exact Subsingleton.elim _ _⟩ + +/-- Given an extension `P : Extension R S`, this is the linear equivalence between +the first homology of the naive cotangent complex of `S` over `P.Ring` and +the cotangent space of `P`. -/ +noncomputable +def h1CotangentEquivCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] + [Algebra R S] (P : Extension.{w} R S) : + H1Cotangent P.Ring S ≃ₗ[S] P.Cotangent := + P.h1CotangentExtendScalarsEquiv.symm ≪≫ₗ + P.extendScalars.h1CotangentEquivOfSurjective Function.surjective_id ≪≫ₗ + P.cotangentExtendScalarsEquiv + +theorem cotangentComplex_comp_h1CotangentEquivCotangent (P : Extension.{w} R S) : + P.cotangentComplex.comp P.h1CotangentEquivCotangent.toLinearMap = + H1Cotangent.δ R P.Ring S := by + rw [h1CotangentEquivCotangent, LinearEquiv.coe_trans, LinearEquiv.coe_trans, + h1CotangentEquivOfSurjective_toLinearMap, ← LinearMap.comp_assoc, ← LinearMap.comp_assoc, + LinearEquiv.comp_toLinearMap_symm_eq, LinearMap.comp_assoc, + h1CotangentExtendScalarsEquiv_toLinearMap] + ext ⟨x, _⟩ + obtain ⟨⟨x : P.Ring, x_in : x ∈ P.ker⟩, rfl⟩ := Cotangent.mk_surjective x + trans 1 ⊗ₜ[P.Ring] D R P.Ring x; · exact cotangentComplex_mk P ⟨x, x_in⟩ + let u : (Generators.self P.Ring S).toExtension.ker := + ⟨algebraMap P.Ring (Generators.self P.Ring S).toExtension.Ring x, by + rwa [← Ideal.mem_comap, RingHom.comap_ker, ← IsScalarTower.algebraMap_eq]⟩ + rw [← Generators.H1Cotangent.δ_C _ _ u.prop] + congr + +theorem h1CotangentEquivCotangent_comp_map (P : Extension.{w} R S) : + P.h1CotangentEquivCotangent.toLinearMap.comp (Algebra.H1Cotangent.map R P.Ring S S) = + h1Cotangentι.comp (H1Cotangent.map P.defaultHom) := by + rw [h1CotangentEquivCotangent, LinearEquiv.coe_trans, LinearEquiv.coe_trans, + h1CotangentExtendScalarsEquiv_symm_toLinearMap, h1CotangentEquivOfSurjective_toLinearMap, + LinearMap.comp_assoc, LinearMap.comp_assoc, Algebra.H1Cotangent.map, + ← (H1Cotangent.map P.extendScalars.defaultHom).restrictScalars_self, ← H1Cotangent.map_comp, + eq_comm, ← LinearEquiv.toLinearMap_symm_comp_eq, cotangentExtendScalarsEquiv_symm_toLinearMap, + ← LinearMap.comp_assoc, Cotangent.map_comp_h1Cotangentι, LinearMap.restrictScalars_self, + LinearMap.comp_assoc, ← (H1Cotangent.map P.toExtendScalars).restrictScalars_self, + ← H1Cotangent.map_comp, H1Cotangent.map_eq] + +theorem H1Cotangent.map_defaultHom_surjective (P : Extension.{w} R S) : + Function.Surjective (H1Cotangent.map P.defaultHom) := by + rw [← LinearMap.range_eq_top, + ← (Submodule.map_injective_of_injective h1Cotangentι_injective).eq_iff, + ← LinearMap.range_comp, ← P.h1CotangentEquivCotangent_comp_map, LinearMap.range_comp, + ← (Algebra.H1Cotangent.exact_map_δ R P.Ring S).linearMap_ker_eq, Submodule.map_top, + ← exact_hCotangentι_cotangentComplex.linearMap_ker_eq, Submodule.map_equiv_eq_comap_symm, + LinearMap.ker, LinearMap.ker, ← Submodule.comap_comp] + congr + rw [LinearEquiv.comp_toLinearMap_symm_eq, P.cotangentComplex_comp_h1CotangentEquivCotangent] + +end Algebra.Extension diff --git a/Mathlib/RingTheory/Extension/Generators.lean b/Mathlib/RingTheory/Extension/Generators.lean index a165eabc2a2ff7..1e3ede9f668cb7 100644 --- a/Mathlib/RingTheory/Extension/Generators.lean +++ b/Mathlib/RingTheory/Extension/Generators.lean @@ -798,3 +798,16 @@ lemma toAlgHom_ofComp_localizationAway (g : S) [IsLocalization.Away g T] : end Hom end Algebra.Generators + +namespace Algebra.Extension + +set_option backward.isDefEq.respectTransparency false in +set_option backward.defeqAttrib.useBackward true in +/-- The canonical homomorphism of extensions from the universal extension `R[S] → S` +(given by `Generators.self R S`) to any extension `P` defined via the designated section `P.σ`. -/ +@[simps!] +noncomputable +def defaultHom (P : Extension.{w} R S) : (Generators.self R S).toExtension.Hom P := + .ofAlgHom (MvPolynomial.aeval P.σ) (by dsimp; ext; simp) + +end Algebra.Extension diff --git a/Mathlib/RingTheory/Kaehler/JacobiZariski.lean b/Mathlib/RingTheory/Kaehler/JacobiZariski.lean index 0175dfdec63ab4..1220b5ccd0bf32 100644 --- a/Mathlib/RingTheory/Kaehler/JacobiZariski.lean +++ b/Mathlib/RingTheory/Kaehler/JacobiZariski.lean @@ -400,6 +400,11 @@ lemma δ_eq_δAux (x : Q.ker) (hx) : ((Q.comp P).toExtension.cotangentComplex y) rw [CotangentSpace.fst_compEquiv, Extension.CotangentSpace.map_cotangentComplex, hy, hx] +lemma δ_C {r : S} (hr : C r ∈ Q.ker) : + δ Q P ⟨Extension.Cotangent.mk ⟨C r, hr⟩, Extension.Cotangent.mk_C_mem_ker_cotangentComplex ..⟩ + = 1 ⊗ₜ[S] D R S r := by + rw [δ_eq_δAux, δAux_C] + lemma δ_eq_δ : δ Q P = δ Q P' := by ext ⟨x, hx⟩ obtain ⟨x, rfl⟩ := Extension.Cotangent.mk_surjective x From 9d9fa2436c5971d37e55b6aa8171817dce7bac3c Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Sat, 13 Jun 2026 10:48:58 +0000 Subject: [PATCH 03/24] feat: connections between order, `realPart` and `imaginaryPart` in star ordered rings (#40565) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mainly, this provides the characterization: `a ≤ b ↔ ℜ a ≤ ℜ b ∧ ℑ a = ℑ b`, but also several related lemmas of convenience. --- Mathlib/LinearAlgebra/Complex/Module.lean | 38 +++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/Mathlib/LinearAlgebra/Complex/Module.lean b/Mathlib/LinearAlgebra/Complex/Module.lean index 30edae0cc3b9f8..7db6282b5b709a 100644 --- a/Mathlib/LinearAlgebra/Complex/Module.lean +++ b/Mathlib/LinearAlgebra/Complex/Module.lean @@ -7,11 +7,13 @@ module public import Mathlib.Algebra.Algebra.RestrictScalars public import Mathlib.Algebra.CharP.Invertible +public import Mathlib.Algebra.Order.Star.Basic public import Mathlib.Algebra.Star.Unitary public import Mathlib.Data.Complex.Basic public import Mathlib.Data.Real.Star public import Mathlib.LinearAlgebra.Matrix.ToLin import Mathlib.Algebra.Module.Torsion.Field +import Mathlib.Algebra.Order.Monoid.Submonoid /-! # Complex number as a vector space over `ℝ` @@ -595,6 +597,42 @@ lemma star_mul_self_eq_realPart_sq_add_imaginaryPart_sq (x : A) [hx : IsStarNorm end NonUnitalNonAssocRing +section StarOrderedRing + +variable [NonUnitalRing A] [StarRing A] [PartialOrder A] + [StarOrderedRing A] [Module ℂ A] [StarModule ℂ A] + +lemma nonneg_iff_realPart_imaginaryPart {a : A} : + 0 ≤ a ↔ 0 ≤ ℜ a ∧ ℑ a = 0 := by + refine ⟨fun h ↦ ⟨?_, h.isSelfAdjoint.imaginaryPart⟩, fun h ↦ ?_⟩ + · simpa +singlePass [← h.isSelfAdjoint.coe_realPart] using! h + · rw [← realPart_add_I_smul_imaginaryPart a, h.2] + simpa using! h.1 + +lemma nonpos_iff_realPart_imaginaryPart {a : A} : + a ≤ 0 ↔ ℜ a ≤ 0 ∧ ℑ a = 0 := by + simpa using nonneg_iff_realPart_imaginaryPart (a := -a) + +lemma realPart_nonneg_of_nonneg {a : A} (ha : 0 ≤ a) : 0 ≤ ℜ a := + nonneg_iff_realPart_imaginaryPart.mp ha |>.1 + +lemma realPart_nonpos_of_nonpos {a : A} (ha : a ≤ 0) : ℜ a ≤ 0 := + nonpos_iff_realPart_imaginaryPart.mp ha |>.1 + +lemma le_iff_realPart_imaginaryPart {a b : A} : + a ≤ b ↔ ℜ a ≤ ℜ b ∧ ℑ a = ℑ b := by + simpa [sub_eq_zero, eq_comm (a := ℑ a)] using nonneg_iff_realPart_imaginaryPart (a := b - a) + +lemma imaginaryPart_eq_of_le {a b : A} (hab : a ≤ b) : + ℑ a = ℑ b := + le_iff_realPart_imaginaryPart.mp hab |>.2 + +lemma realPart_mono {a b : A} (hab : a ≤ b) : + ℜ a ≤ ℜ b := + le_iff_realPart_imaginaryPart.mp hab |>.1 + +end StarOrderedRing + @[simp] lemma realPart_one [Ring A] [StarRing A] [Module ℂ A] [StarModule ℂ A] : ℜ (1 : A) = 1 := by From 36ac4e29ee787119d0ee5e1abba9a560ce7e65d9 Mon Sep 17 00:00:00 2001 From: Christian Merten <136261474+chrisflav@users.noreply.github.com> Date: Sat, 13 Jun 2026 12:29:28 +0000 Subject: [PATCH 04/24] chore(CategoryTheory/Filtered): generalise criteria for filteredness of `CostructuredArrow` (#40559) From Proetale and subsequently cleaned up by Claude Fable 5. --- Mathlib/CategoryTheory/Filtered/Final.lean | 37 ++++++++++------------ 1 file changed, 17 insertions(+), 20 deletions(-) diff --git a/Mathlib/CategoryTheory/Filtered/Final.lean b/Mathlib/CategoryTheory/Filtered/Final.lean index bebaba5487036e..edd610db14229d 100644 --- a/Mathlib/CategoryTheory/Filtered/Final.lean +++ b/Mathlib/CategoryTheory/Filtered/Final.lean @@ -60,12 +60,12 @@ theorem Functor.initial_of_isCofiltered_costructuredArrow [∀ d, IsCofiltered (CostructuredArrow F d)] : Initial F where out _ := IsCofiltered.isConnected _ -theorem isFiltered_structuredArrow_of_isFiltered_of_exists [IsFilteredOrEmpty C] - (h₁ : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), - ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) (d : D) : +theorem isFiltered_structuredArrow_of_isFiltered_of_exists [IsFilteredOrEmpty C] (d : D) + (h₁ : ∃ c, Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), + ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) : IsFiltered (StructuredArrow d F) := by have : Nonempty (StructuredArrow d F) := by - obtain ⟨c, ⟨f⟩⟩ := h₁ d + obtain ⟨c, ⟨f⟩⟩ := h₁ exact ⟨.mk f⟩ suffices IsFilteredOrEmpty (StructuredArrow d F) from IsFiltered.mk refine ⟨fun f g => ?_, fun f g η μ => ?_⟩ @@ -78,18 +78,17 @@ theorem isFiltered_structuredArrow_of_isFiltered_of_exists [IsFilteredOrEmpty C] StructuredArrow.homMk (IsFiltered.coeqHom η.right μ.right) (by simp), ?_⟩ simpa using IsFiltered.coeq_condition _ _ -theorem isCofiltered_costructuredArrow_of_isCofiltered_of_exists [IsCofilteredOrEmpty C] - (h₁ : ∀ d, ∃ c, Nonempty (F.obj c ⟶ d)) (h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), - ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') (d : D) : +theorem isCofiltered_costructuredArrow_of_isCofiltered_of_exists [IsCofilteredOrEmpty C] (d : D) + (h₁ : ∃ c, Nonempty (F.obj c ⟶ d)) (h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), + ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') : IsCofiltered (CostructuredArrow F d) := by suffices IsFiltered (CostructuredArrow F d)ᵒᵖ from isCofiltered_of_isFiltered_op _ suffices IsFiltered (StructuredArrow (op d) F.op) from IsFiltered.of_equivalence (costructuredArrowOpEquivalence _ _).symm apply isFiltered_structuredArrow_of_isFiltered_of_exists - · intro d - obtain ⟨c, ⟨t⟩⟩ := h₁ d.unop + · obtain ⟨c, ⟨t⟩⟩ := h₁ exact ⟨op c, ⟨Quiver.Hom.op t⟩⟩ - · intro d c s s' + · intro c s s' obtain ⟨c', t, ht⟩ := h₂ s.unop s'.unop exact ⟨op c', Quiver.Hom.op t, Quiver.Hom.unop_inj ht⟩ @@ -99,7 +98,7 @@ theorem Functor.final_of_exists_of_isFiltered [IsFilteredOrEmpty C] (h₁ : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) : Functor.Final F := by suffices ∀ d, IsFiltered (StructuredArrow d F) from final_of_isFiltered_structuredArrow F - exact isFiltered_structuredArrow_of_isFiltered_of_exists F h₁ h₂ + exact fun d => isFiltered_structuredArrow_of_isFiltered_of_exists F d (h₁ d) h₂ /-- The inclusion of a terminal object is final. -/ theorem Functor.final_const_of_isTerminal [IsFiltered C] {X : D} (hX : IsTerminal X) : @@ -119,7 +118,7 @@ theorem Functor.initial_of_exists_of_isCofiltered [IsCofilteredOrEmpty C] ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') : Functor.Initial F := by suffices ∀ d, IsCofiltered (CostructuredArrow F d) from initial_of_isCofiltered_costructuredArrow F - exact isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h₁ h₂ + exact fun d => isCofiltered_costructuredArrow_of_isCofiltered_of_exists F d (h₁ d) h₂ /-- The inclusion of an initial object is initial. -/ theorem Functor.initial_const_of_isInitial [IsCofiltered C] {X : D} (hX : IsInitial X) : @@ -196,16 +195,14 @@ theorem Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful [IsCofiltered /-- Any under category on a filtered or empty category is filtered. (Note that under categories are always cofiltered since they have an initial object.) -/ instance IsFiltered.under [IsFilteredOrEmpty C] (c : C) : IsFiltered (Under c) := - isFiltered_structuredArrow_of_isFiltered_of_exists _ - (fun c' => ⟨c', ⟨𝟙 _⟩⟩) - (fun s s' => IsFilteredOrEmpty.cocone_maps s s') c + isFiltered_structuredArrow_of_isFiltered_of_exists _ c ⟨c, ⟨𝟙 _⟩⟩ + (fun s s' => IsFilteredOrEmpty.cocone_maps s s') /-- Any over category on a cofiltered or empty category is cofiltered. (Note that over categories are always filtered since they have a terminal object.) -/ instance IsCofiltered.over [IsCofilteredOrEmpty C] (c : C) : IsCofiltered (Over c) := - isCofiltered_costructuredArrow_of_isCofiltered_of_exists _ - (fun c' => ⟨c', ⟨𝟙 _⟩⟩) - (fun s s' => IsCofilteredOrEmpty.cone_maps s s') c + isCofiltered_costructuredArrow_of_isCofiltered_of_exists _ c ⟨c, ⟨𝟙 _⟩⟩ + (fun s s' => IsCofilteredOrEmpty.cone_maps s s') set_option backward.defeqAttrib.useBackward true in /-- The forgetful functor of the under category on any filtered or empty category is final. -/ @@ -296,7 +293,7 @@ theorem Functor.final_iff_isFiltered_structuredArrow [IsFilteredOrEmpty C] : Final F ↔ ∀ d, IsFiltered (StructuredArrow d F) := by refine ⟨?_, fun h => final_of_isFiltered_structuredArrow F⟩ rw [final_iff_of_isFiltered] - exact fun h => isFiltered_structuredArrow_of_isFiltered_of_exists F h.1 h.2 + exact fun h d => isFiltered_structuredArrow_of_isFiltered_of_exists F d (h.1 d) h.2 /-- If `C` is cofiltered, then `F : C ⥤ D` is initial if and only if `CostructuredArrow F d` is cofiltered for all `d : D`. -/ @@ -304,7 +301,7 @@ theorem Functor.initial_iff_isCofiltered_costructuredArrow [IsCofilteredOrEmpty Initial F ↔ ∀ d, IsCofiltered (CostructuredArrow F d) := by refine ⟨?_, fun h => initial_of_isCofiltered_costructuredArrow F⟩ rw [initial_iff_of_isCofiltered] - exact fun h => isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h.1 h.2 + exact fun h d => isCofiltered_costructuredArrow_of_isCofiltered_of_exists F d (h.1 d) h.2 /-- If `C` is filtered, then the structured arrow category on the diagonal functor `C ⥤ C × C` is filtered as well. -/ From 6ca5e2d4f1ab325db1fe867e2da3144302f79904 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Sat, 13 Jun 2026 12:57:04 +0000 Subject: [PATCH 05/24] =?UTF-8?q?feat:=20the=20canonical=20approximate=20u?= =?UTF-8?q?nit=20in=20a=20C=E2=8B=86-algebra=20is=20not=20`=E2=8A=A5`=20(#?= =?UTF-8?q?40566)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We also add a convenience lemma. This is almost trivial from the definition, but it's useful to have the `closedBall` version. --- Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean index ab32228a31290d..0e759020348256 100644 --- a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean +++ b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean @@ -158,6 +158,11 @@ lemma eventually_star_eq {l : Filter A} (hl : l.IsIncreasingApproximateUnit) : ∀ᶠ x in l, star x = x := hl.eventually_isSelfAdjoint.mp <| .of_forall fun _ ↦ IsSelfAdjoint.star_eq +omit [StarOrderedRing A] in +lemma closedBall_mem {l : Filter A} (hl : l.IsIncreasingApproximateUnit) : + Metric.closedBall 0 1 ∈ l := by + simpa [Metric.closedBall] using! hl.eventually_norm + lemma pure_one (A : Type*) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : (pure 1 : Filter A).IsIncreasingApproximateUnit where toIsApproximateUnit := .pure_one A @@ -326,6 +331,8 @@ lemma increasingApproximateUnit : neBot := hasBasis_approximateUnit A |>.neBot_iff.mpr fun hx ↦ ⟨_, ⟨le_rfl, by simpa using hx.2.le⟩⟩ +instance : (approximateUnit A).NeBot := (increasingApproximateUnit A).neBot + end CStarAlgebra end ApproximateUnit From bf69091c35a4c18a1294f4fba3528046966fd3b0 Mon Sep 17 00:00:00 2001 From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> Date: Sat, 13 Jun 2026 13:42:07 +0000 Subject: [PATCH 06/24] =?UTF-8?q?feat(Order/ConditionallyCompleteLattice/F?= =?UTF-8?q?inset):=20`sSup=20s=20=E2=89=A0=20=E2=8A=A4`=20in=20a=20`Comple?= =?UTF-8?q?teLinearOrder`=20for=20a=20finite=20set=20without=20`=E2=8A=A4`?= =?UTF-8?q?=20(#38356)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit and more generally, `sSup s ≠ a` for a finite set `s` without `a`, when `a ≠ ⊥`. Also adds the equivalent `sInf`/`iSup`/`iInf` lemmas. --- .../ConditionallyCompleteLattice/Finset.lean | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean index c6f70a19799255..386e4e5f5ff243 100644 --- a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean +++ b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean @@ -179,6 +179,42 @@ end ListMultiset end ConditionallyCompleteLinearOrder +section CompleteLinearOrder + +variable {α : Type*} [CompleteLinearOrder α] {ι : Sort*} + +theorem sSup_ne_of_notMem {s : Set α} (hfin : s.Finite) {a : α} (hne : a ≠ ⊥) (hmem : a ∉ s) : + sSup s ≠ a := by + rcases s.eq_empty_or_nonempty with rfl | hnonempty + · simp [eq_comm, hne] + exact (hmem <| · ▸ hnonempty.csSup_mem hfin) + +theorem sInf_ne_of_notMem {s : Set α} (hfin : s.Finite) {a : α} (hne : a ≠ ⊤) (hmem : a ∉ s) : + sInf s ≠ a := + sSup_ne_of_notMem (α := αᵒᵈ) hfin hne hmem + +theorem sSup_ne_top [Nontrivial α] {s : Set α} (hfin : s.Finite) (htop : ⊤ ∉ s) : sSup s ≠ ⊤ := + sSup_ne_of_notMem hfin top_ne_bot htop + +theorem sInf_ne_bot [Nontrivial α] {s : Set α} (hfin : s.Finite) (hbot : ⊥ ∉ s) : sInf s ≠ ⊥ := + sSup_ne_top (α := αᵒᵈ) hfin hbot + +theorem iSup_ne_of_notMem [Finite ι] {f : ι → α} {a : α} (hne : a ≠ ⊥) (h : ∀ x, f x ≠ a) : + iSup f ≠ a := + sSup_ne_of_notMem (Set.finite_range f) hne <| by grind + +theorem iInf_ne_of_notMem [Finite ι] {f : ι → α} {a : α} (hne : a ≠ ⊤) (h : ∀ x, f x ≠ a) : + iInf f ≠ a := + iSup_ne_of_notMem (α := αᵒᵈ) hne h + +theorem iSup_ne_top [Finite ι] [Nontrivial α] {f : ι → α} (h : ∀ x, f x ≠ ⊤) : iSup f ≠ ⊤ := + iSup_ne_of_notMem top_ne_bot h + +theorem iInf_ne_bot [Finite ι] [Nontrivial α] {f : ι → α} (h : ∀ x, f x ≠ ⊥) : iInf f ≠ ⊥ := + iSup_ne_top (α := αᵒᵈ) h + +end CompleteLinearOrder + /-! ### Relation between `sSup` / `sInf` and `Finset.sup'` / `Finset.inf'` From e0cf79c4769ba1be20bb3e188bc59130676dda9d Mon Sep 17 00:00:00 2001 From: Hannah Scholz <70071345+scholzhannah@users.noreply.github.com> Date: Sat, 13 Jun 2026 14:25:02 +0000 Subject: [PATCH 07/24] feat: use `alias_in` attribute for CW complexes (#38785) Using the `alias_in` attribute for classical CW complexes to get rid of the `export` sections. --- .../Topology/CWComplex/Classical/Basic.lean | 127 ++++++++++++------ .../Topology/CWComplex/Classical/Finite.lean | 18 +-- .../CWComplex/Classical/Subcomplex.lean | 16 +-- 3 files changed, 103 insertions(+), 58 deletions(-) diff --git a/Mathlib/Topology/CWComplex/Classical/Basic.lean b/Mathlib/Topology/CWComplex/Classical/Basic.lean index 9ddc89d00f237c..97b4720eaba62a 100644 --- a/Mathlib/Topology/CWComplex/Classical/Basic.lean +++ b/Mathlib/Topology/CWComplex/Classical/Basic.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.Normed.Module.RCLike.Real public import Mathlib.Data.ENat.Basic public import Mathlib.Logic.Equiv.PartialEquiv +public import Mathlib.Util.AliasIn /-! # CW complexes @@ -62,6 +63,19 @@ together. cells `cell C` of an absolute CW complex `C`, this actually refers to `RelCWComplex.cell C` through this instance. Again, we want typeclass inference to first consider absolute CW structures. +* The namespaces `CWComplex` and `RelCWComplex` generally should not be opened at the same time + as they contain many declarations with identical names. Still, we want working with absolute + CW complexes to be as convenient as possible. Thus every declaration about relative CW complexes + that doesn't have a modified version for absolute CW complexes should receive an alias in the + `CWComplex` namespace. It is recommended to use the `alias_in` attribute for this here. See + below for a restriction on when we want to create aliases. +* For types and definitions relevant to CW complexes like `cell`, `openCell`, `closedCell`, + `cellFrontier`, `skeletonLT` and similar, we want there to exist only one actually used version, + namely the version in the `RelCWComplex` namespace (and thus no seperate definition in the + `CWComplex` namespace.) This is to avoid unnecessary duplication of lemmas. To achieve this, + definitions from the `RelCWComplex` namespace should be added to the `CWComplex` namespace with + `export` intead of `alias_in`/`alias`. These will then apply to the absolute CW complex through + the instance `CWComplex.instRelCWComplex`. * For statements, the auxiliary construction `skeletonLT` is preferred over `skeleton` as it makes the base case of inductions easier. The statement about `skeleton` should then be derived from the one about `skeletonLT`. @@ -199,7 +213,7 @@ def RelCWComplex.cellFrontier [RelCWComplex C D] (n : ℕ) (i : cell C n) : Set namespace CWComplex -export RelCWComplex (cell map source_eq continuousOn continuousOn_symm mapsTo isClosedBase openCell +export RelCWComplex (cell map source_eq continuousOn continuousOn_symm isClosedBase openCell closedCell cellFrontier) end CWComplex @@ -210,14 +224,17 @@ lemma CWComplex.mapsTo [CWComplex C] (n : ℕ) (i : cell C n) : ∃ I : Π m, Fi simp_rw [empty_union] at this exact this +@[alias_in CWComplex] lemma RelCWComplex.pairwiseDisjoint [RelCWComplex C D] : (univ : Set (Σ n, cell C n)).PairwiseDisjoint (fun ni ↦ openCell ni.1 ni.2) := RelCWComplex.pairwiseDisjoint' +@[alias_in CWComplex] lemma RelCWComplex.disjointBase [RelCWComplex C D] (n : ℕ) (i : cell C n) : Disjoint (openCell n i) D := RelCWComplex.disjointBase' n i +@[alias_in CWComplex] lemma RelCWComplex.disjoint_openCell_of_ne [RelCWComplex C D] {n m : ℕ} {i : cell C n} {j : cell C m} (ne : (⟨n, i⟩ : Σ n, cell C n) ≠ ⟨m, j⟩) : Disjoint (openCell n i) (openCell m j) := @@ -246,23 +263,28 @@ lemma CWComplex.union [CWComplex C] : ⋃ (n : ℕ) (j : cell C n), closedCell n rw [empty_union] at this exact this +@[alias_in CWComplex] lemma RelCWComplex.openCell_subset_closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) : openCell n i ⊆ closedCell n i := image_mono Metric.ball_subset_closedBall +@[alias_in CWComplex] lemma RelCWComplex.cellFrontier_subset_closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) : cellFrontier n i ⊆ closedCell n i := image_mono Metric.sphere_subset_closedBall +@[alias_in CWComplex] lemma RelCWComplex.cellFrontier_union_openCell_eq_closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) : cellFrontier n i ∪ openCell n i = closedCell n i := by rw [cellFrontier, openCell, closedCell, ← image_union] congrm map n i '' ?_ exact sphere_union_ball +@[alias_in CWComplex] lemma RelCWComplex.map_zero_mem_openCell [RelCWComplex C D] (n : ℕ) (i : cell C n) : map n i 0 ∈ openCell n i := by apply mem_image_of_mem simp only [mem_ball, dist_self, zero_lt_one] +@[alias_in CWComplex] lemma RelCWComplex.map_zero_mem_closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) : map n i 0 ∈ closedCell n i := openCell_subset_closedCell _ _ (map_zero_mem_openCell _ _) @@ -298,21 +320,26 @@ lemma CWComplex.eq_of_eq_union_iUnion [CWComplex C] (I J : Π n, Set (cell C n)) apply RelCWComplex.eq_of_eq_union_iUnion simp_rw [empty_union, hIJ] +@[alias_in CWComplex] lemma RelCWComplex.isCompact_closedCell [RelCWComplex C D] {n : ℕ} {i : cell C n} : IsCompact (closedCell n i) := (isCompact_closedBall _ _).image_of_continuousOn (continuousOn n i) +@[alias_in CWComplex] lemma RelCWComplex.isClosed_closedCell [RelCWComplex C D] [T2Space X] {n : ℕ} {i : cell C n} : IsClosed (closedCell n i) := isCompact_closedCell.isClosed +@[alias_in CWComplex] lemma RelCWComplex.isCompact_cellFrontier [RelCWComplex C D] {n : ℕ} {i : cell C n} : IsCompact (cellFrontier n i) := (isCompact_sphere _ _).image_of_continuousOn ((continuousOn n i).mono sphere_subset_closedBall) +@[alias_in CWComplex] lemma RelCWComplex.isClosed_cellFrontier [RelCWComplex C D] [T2Space X] {n : ℕ} {i : cell C n} : IsClosed (cellFrontier n i) := isCompact_cellFrontier.isClosed +@[alias_in CWComplex] lemma RelCWComplex.closure_openCell_eq_closedCell [RelCWComplex C D] [T2Space X] {n : ℕ} {j : cell C n} : closure (openCell n j) = closedCell n j := by apply subset_antisymm (isClosed_closedCell.closure_subset_iff.2 (openCell_subset_closedCell n j)) @@ -332,31 +359,38 @@ lemma CWComplex.closed (C : Set X) [CWComplex C] [T2Space X] (A : Set X) (asubc have := RelCWComplex.closed C A asubc simp_all +@[alias_in CWComplex] lemma RelCWComplex.closedCell_subset_complex [RelCWComplex C D] (n : ℕ) (j : cell C n) : closedCell n j ⊆ C := by simp_rw [← union] exact subset_union_of_subset_right (subset_iUnion₂ _ _) _ +@[alias_in CWComplex] lemma RelCWComplex.openCell_subset_complex [RelCWComplex C D] (n : ℕ) (j : cell C n) : openCell n j ⊆ C := (openCell_subset_closedCell _ _).trans (closedCell_subset_complex _ _) +@[alias_in CWComplex] lemma RelCWComplex.cellFrontier_subset_complex [RelCWComplex C D] (n : ℕ) (j : cell C n) : cellFrontier n j ⊆ C := (cellFrontier_subset_closedCell n j).trans (closedCell_subset_complex n j) +@[alias_in CWComplex] lemma RelCWComplex.closedCell_zero_eq_singleton [RelCWComplex C D] {j : cell C 0} : closedCell 0 j = {map 0 j ![]} := by simp [closedCell, Matrix.empty_eq] +@[alias_in CWComplex] lemma RelCWComplex.openCell_zero_eq_singleton [RelCWComplex C D] {j : cell C 0} : openCell 0 j = {map 0 j ![]} := by simp [openCell, Matrix.empty_eq] +@[alias_in CWComplex] lemma RelCWComplex.cellFrontier_zero_eq_empty [RelCWComplex C D] {j : cell C 0} : cellFrontier 0 j = ∅ := by simp [cellFrontier, sphere_eq_empty_of_subsingleton] +@[alias_in CWComplex] lemma RelCWComplex.nonempty_cellFrontier [CWComplex C] {n : ℕ} (hn : n ≠ 0) (j : cell C n) : (cellFrontier n j).Nonempty := by letI : NeZero n := ⟨hn⟩ @@ -365,6 +399,7 @@ lemma RelCWComplex.nonempty_cellFrontier [CWComplex C] {n : ℕ} (hn : n ≠ 0) use Pi.single 0 1, by simp [Pi.norm_single] /-- If two 0-cells have the same characteristic image point, they are equal. -/ +@[alias_in CWComplex] lemma RelCWComplex.injective_map_zero (C : Set X) [RelCWComplex C D] : Injective ((map 0 · ![]) : cell C 0 → X) := by rintro x z h @@ -372,23 +407,26 @@ lemma RelCWComplex.injective_map_zero (C : Set X) [RelCWComplex C D] : exact not_disjoint_iff.mpr ⟨map 0 x ![], by simp [openCell_zero_eq_singleton, h]⟩ <| disjoint_openCell_of_ne (by grind : (⟨0, x⟩ : Σ n, cell C n) ≠ ⟨0, z⟩) -@[simp] +@[simp, alias_in CWComplex] lemma RelCWComplex.map_zero_eq_self_iff (C : Set X) [RelCWComplex C D] {x z : cell C 0} : map 0 x ![] = map 0 z ![] ↔ x = z := ⟨fun h ↦ injective_map_zero C h, fun h ↦ h ▸ rfl⟩ +@[alias_in CWComplex] lemma RelCWComplex.closedCell_zero_injective (C : Set X) [RelCWComplex C D] : Injective (closedCell 0 : cell C 0 → _) := by intro x y h rw [closedCell_zero_eq_singleton, closedCell_zero_eq_singleton, singleton_eq_singleton_iff] at h exact injective_map_zero C h +@[alias_in CWComplex] lemma RelCWComplex.openCell_zero_injective (C : Set X) [RelCWComplex C D] : Injective (openCell 0 : cell C 0 → _) := by intro x y h rw [openCell_zero_eq_singleton, openCell_zero_eq_singleton, singleton_eq_singleton_iff] at h exact injective_map_zero C h +@[alias_in CWComplex] lemma RelCWComplex.cellFrontier_one_eq [RelCWComplex C D] (e : cell C 1) : cellFrontier 1 e = map 1 e '' {-1, 1} := by rw [cellFrontier] @@ -411,10 +449,12 @@ lemma CWComplex.exists_cellFrontier_one_eq [CWComplex C] (e : cell C 1) : simp [RelCWComplex.cellFrontier_one_eq, image_pair, RelCWComplex.closedCell_zero_eq_singleton, hun1, hv1, pair_comm] +@[alias_in CWComplex] lemma RelCWComplex.base_subset_complex [RelCWComplex C D] : D ⊆ C := by simp_rw [← union] exact subset_union_left +@[alias_in CWComplex] lemma RelCWComplex.isClosed [T2Space X] [RelCWComplex C D] : IsClosed C := by rw [closed C C (by rfl)] constructor @@ -467,6 +507,7 @@ lemma CWComplex.iUnion_openCell_eq_complex [CWComplex C] : simpa using RelCWComplex.union_iUnion_openCell_eq_complex (C := C) /-- The contrapositive of `disjoint_openCell_of_ne`. -/ +@[alias_in CWComplex] lemma RelCWComplex.eq_of_not_disjoint_openCell [RelCWComplex C D] {n : ℕ} {j : cell C n} {m : ℕ} {i : cell C m} (h : ¬ Disjoint (openCell n j) (openCell m i)) : (⟨n, j⟩ : (Σ n, cell C n)) = ⟨m, i⟩ := by @@ -629,13 +670,17 @@ instance : PartialOrder (Subcomplex C) := .ofSetLike (Subcomplex C) X initialize_simps_projections Subcomplex (carrier → coe, as_prefix coe) +@[alias_in CWComplex.Subcomplex] lemma mem_carrier {E : Subcomplex C} {x : X} : x ∈ E.carrier ↔ x ∈ (E : Set X) := Iff.rfl +@[alias_in CWComplex.Subcomplex] lemma coe_eq_carrier {E : Subcomplex C} : (E : Set X) = E.carrier := rfl -@[ext] lemma ext {E F : Subcomplex C} (h : ∀ x, x ∈ E ↔ x ∈ F) : E = F := +@[ext, alias_in CWComplex.Subcomplex] +lemma ext {E F : Subcomplex C} (h : ∀ x, x ∈ E ↔ x ∈ F) : E = F := SetLike.ext h +@[alias_in CWComplex.Subcomplex] lemma eq_iff (E F : Subcomplex C) : E = F ↔ (E : Set X) = F := SetLike.coe_injective.eq_iff.symm @@ -648,10 +693,12 @@ protected def copy (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ℕ) closed' := hF.symm ▸ E.closed' union' := hF.symm ▸ hJ ▸ E.union' } -@[simp] lemma coe_copy (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ℕ) → Set (cell C n)) +@[simp, alias_in CWComplex.Subcomplex] +lemma coe_copy (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ℕ) → Set (cell C n)) (hJ : J = E.I) : (E.copy F hF J hJ : Set X) = F := rfl +@[alias_in CWComplex.Subcomplex] lemma copy_eq (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ℕ) → Set (cell C n)) (hJ : J = E.I) : E.copy F hF J hJ = E := SetLike.coe_injective hF @@ -661,6 +708,7 @@ lemma union (E : Subcomplex C) : rw [E.union'] rfl +@[alias_in CWComplex.Subcomplex] lemma closed (E : Subcomplex C) : IsClosed (E : Set X) := E.closed' end Subcomplex @@ -669,13 +717,9 @@ end RelCWComplex namespace CWComplex -export RelCWComplex (Subcomplex) +export RelCWComplex (Subcomplex Subcomplex.I Subcomplex.copy) -namespace Subcomplex - -export RelCWComplex.Subcomplex (I closed union mem_carrier coe_eq_carrier ext copy coe_copy copy_eq) - -end CWComplex.Subcomplex +end CWComplex lemma CWComplex.Subcomplex.union {C : Set X} [CWComplex C] {E : Subcomplex C} : ⋃ (n : ℕ) (j : E.I n), openCell (C := C) n j = E := by @@ -749,22 +793,18 @@ def CWComplex.Subcomplex.mk'' [T2Space X] (C : Set X) [h : CWComplex C] (E : Set rw [empty_union] exact union +@[alias_in CWComplex.Subcomplex] lemma RelCWComplex.Subcomplex.subset_complex {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) : ↑E ⊆ C := by simp_rw [← union, ← RelCWComplex.union_iUnion_openCell_eq_complex] exact union_subset_union_right _ (iUnion_mono fun _ ↦ iUnion_mono' fun j ↦ ⟨j, subset_rfl⟩) +@[alias_in CWComplex.Subcomplex] lemma RelCWComplex.Subcomplex.base_subset {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) : D ⊆ E := by simp_rw [← union] exact subset_union_left -namespace CWComplex.Subcomplex - -export RelCWComplex.Subcomplex (subset_complex base_subset) - -end CWComplex.Subcomplex - end Subcomplex section skeleton @@ -778,7 +818,7 @@ This allows the base case of induction to be about the base instead of being abo the base and some points. The standard `skeleton` is defined in terms of `skeletonLT`. `skeletonLT` is preferred in statements. You should then derive the statement about `skeleton`. -/ -@[simps! -isSimp, irreducible] +@[simps! (attr := alias_in CWComplex) -isSimp, irreducible] def skeletonLT (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) : Subcomplex C := Subcomplex.mk' _ (D ∪ ⋃ (m : ℕ) (_ : m < n) (j : cell C m), closedCell m j) (fun l ↦ {x : cell C l | l < n}) @@ -803,7 +843,7 @@ end RelCWComplex namespace CWComplex -export RelCWComplex (skeletonLT coe_skeletonLT skeletonLT_I skeleton) +export RelCWComplex (skeletonLT skeleton) end CWComplex @@ -813,11 +853,14 @@ lemma RelCWComplex.skeletonLT_zero_eq_base [RelCWComplex C D] : skeletonLT C 0 = lemma CWComplex.skeletonLT_zero_eq_empty [CWComplex C] : (skeletonLT C 0 : Set X) = ∅ := RelCWComplex.skeletonLT_zero_eq_base -@[simp] lemma RelCWComplex.skeletonLT_top [RelCWComplex C D] : skeletonLT C ⊤ = C := by +@[simp, alias_in CWComplex] lemma RelCWComplex.skeletonLT_top [RelCWComplex C D] : + skeletonLT C ⊤ = C := by simp [coe_skeletonLT, union] -@[simp] lemma RelCWComplex.skeleton_top [RelCWComplex C D] : skeleton C ⊤ = C := skeletonLT_top +@[simp, alias_in CWComplex] lemma RelCWComplex.skeleton_top [RelCWComplex C D] : skeleton C ⊤ = C := + skeletonLT_top +@[alias_in CWComplex] lemma RelCWComplex.skeletonLT_mono [RelCWComplex C D] {n m : ℕ∞} (h : m ≤ n) : (skeletonLT C m : Set X) ⊆ skeletonLT C n := by simp_rw [coe_skeletonLT] @@ -827,16 +870,20 @@ lemma RelCWComplex.skeletonLT_mono [RelCWComplex C D] {n m : ℕ∞} (h : m ≤ obtain ⟨l, lltm, xmeml⟩ := xmem exact ⟨l, lt_of_lt_of_le lltm h, xmeml⟩ +@[alias_in CWComplex] lemma RelCWComplex.skeletonLT_monotone [RelCWComplex C D] : Monotone (skeletonLT C) := fun _ _ h ↦ skeletonLT_mono h +@[alias_in CWComplex] lemma RelCWComplex.skeleton_mono [RelCWComplex C D] {n m : ℕ∞} (h : m ≤ n) : (skeleton C m : Set X) ⊆ skeleton C n := skeletonLT_mono (by gcongr) +@[alias_in CWComplex] lemma RelCWComplex.skeleton_monotone [RelCWComplex C D] : Monotone (skeleton C) := fun _ _ h ↦ skeleton_mono h +@[alias_in CWComplex] lemma RelCWComplex.closedCell_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j : cell C n) : closedCell n j ⊆ skeletonLT C (n + 1) := by intro x xmem @@ -845,18 +892,22 @@ lemma RelCWComplex.closedCell_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j simp_rw [mem_iUnion, exists_prop] refine ⟨n, (by norm_cast; exact lt_add_one n), ⟨j,xmem⟩⟩ +@[alias_in CWComplex] lemma RelCWComplex.closedCell_subset_skeleton [RelCWComplex C D] (n : ℕ) (j : cell C n) : closedCell n j ⊆ skeleton C n := closedCell_subset_skeletonLT n j +@[alias_in CWComplex] lemma RelCWComplex.openCell_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j : cell C n) : openCell n j ⊆ skeletonLT C (n + 1) := (openCell_subset_closedCell _ _).trans (closedCell_subset_skeletonLT _ _) +@[alias_in CWComplex] lemma RelCWComplex.openCell_subset_skeleton [RelCWComplex C D] (n : ℕ) (j : cell C n) : openCell n j ⊆ skeleton C n := (openCell_subset_closedCell _ _).trans (closedCell_subset_skeleton _ _) +@[alias_in CWComplex] lemma RelCWComplex.cellFrontier_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j : cell C n) : cellFrontier n j ⊆ skeletonLT C n := by obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell n j @@ -868,18 +919,22 @@ lemma RelCWComplex.cellFrontier_subset_skeletonLT [RelCWComplex C D] (n : ℕ) ( obtain ⟨i, iltn, j, _, xmem⟩ := xmem exact ⟨i, by norm_cast, j, xmem⟩ +@[alias_in CWComplex] lemma RelCWComplex.cellFrontier_subset_skeleton [RelCWComplex C D] (n : ℕ) (j : cell C (n + 1)) : cellFrontier (n + 1) j ⊆ skeleton C n := cellFrontier_subset_skeletonLT _ _ +@[alias_in CWComplex] lemma RelCWComplex.iUnion_cellFrontier_subset_skeletonLT [RelCWComplex C D] (l : ℕ) : ⋃ (j : cell C l), cellFrontier l j ⊆ skeletonLT C l := iUnion_subset (fun _ ↦ cellFrontier_subset_skeletonLT _ _) +@[alias_in CWComplex] lemma RelCWComplex.iUnion_cellFrontier_subset_skeleton [RelCWComplex C D] (l : ℕ) : ⋃ (j : cell C l), cellFrontier l j ⊆ skeleton C l := (iUnion_cellFrontier_subset_skeletonLT l).trans (skeletonLT_mono le_self_add) +@[alias_in CWComplex] lemma RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ [RelCWComplex C D] (n : ℕ) : (skeletonLT C n : Set X) ∪ ⋃ (j : cell C n), closedCell n j = skeletonLT C (n + 1) := by @@ -888,6 +943,7 @@ lemma RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ [RelCWC norm_cast exact (biUnion_lt_succ _ _).symm +@[alias_in CWComplex] lemma RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ [RelCWComplex C D] (n : ℕ) : (skeleton C n : Set X) ∪ ⋃ (j : cell C (n + 1)), closedCell (n + 1) j = skeleton C (n + 1) := skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ _ @@ -909,6 +965,7 @@ lemma CWComplex.iUnion_openCell_eq_skeleton [CWComplex C] (n : ℕ∞) : ⋃ (m : ℕ) (_ : m < n + 1) (j : cell C m), openCell m j = skeleton C n := iUnion_openCell_eq_skeletonLT _ +@[alias_in CWComplex] lemma RelCWComplex.iUnion_skeletonLT_eq_complex [RelCWComplex C D] : ⋃ (n : ℕ), skeletonLT C n = C := by apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeletonLT C _).subset_complex) @@ -916,6 +973,7 @@ lemma RelCWComplex.iUnion_skeletonLT_eq_complex [RelCWComplex C D] : exact ⟨subset_iUnion_of_subset 0 (skeletonLT C 0).base_subset, fun n i ↦ subset_iUnion_of_subset _ (openCell_subset_skeletonLT n i)⟩ +@[alias_in CWComplex] lemma RelCWComplex.iUnion_skeleton_eq_complex [RelCWComplex C D] : ⋃ (n : ℕ), skeleton C n = C := by apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeleton C _).subset_complex) @@ -940,11 +998,15 @@ lemma RelCWComplex.mem_skeleton_iff [RelCWComplex C D] {n : ℕ∞} {x : X} : · simp · rw [← Nat.cast_one, ← Nat.cast_add, Nat.cast_lt, Nat.cast_le, Order.lt_add_one_iff] -lemma CWComplex.exists_mem_openCell_of_mem_skeleton [CWComplex C] {n : ℕ∞} {x : X} : +lemma CWComplex.mem_skeleton_iff [CWComplex C] {n : ℕ∞} {x : X} : x ∈ skeleton C n ↔ ∃ (m : ℕ) (_ : m ≤ n) (j : cell C m), x ∈ openCell m j := by rw [RelCWComplex.mem_skeleton_iff, mem_empty_iff_false, false_or] +@[deprecated (since := "2026-04-30")] alias CWComplex.exists_mem_openCell_of_mem_skeleton := + CWComplex.mem_skeleton_iff + /-- A skeleton and an open cell of a higher dimension are disjoint. -/ +@[alias_in CWComplex] lemma RelCWComplex.disjoint_skeletonLT_openCell [RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : cell C m} (hnm : n ≤ m) : Disjoint (skeletonLT C n : Set X) (openCell m j) := by -- This is a consequence of `iUnion_openCell_eq_skeletonLT` and `disjoint_openCell_of_ne` @@ -957,12 +1019,14 @@ lemma RelCWComplex.disjoint_skeletonLT_openCell [RelCWComplex C D] {n : ℕ∞} exact (lt_self_iff_false m).mp (ENat.coe_lt_coe.1 (hln.trans_le hnm)) /-- A skeleton and an open cell of a higher dimension are disjoint. -/ +@[alias_in CWComplex] lemma RelCWComplex.disjoint_skeleton_openCell [RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : cell C m} (nlem : n < m) : Disjoint (skeleton C n : Set X) (openCell m j) := disjoint_skeletonLT_openCell (Order.add_one_le_of_lt nlem) /-- A skeleton intersected with a closed cell of a higher dimension is the skeleton intersected with the boundary of the cell. -/ +@[alias_in CWComplex] lemma RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier [RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : cell C m} (hnm : n ≤ m) : (skeletonLT C n : Set X) ∩ closedCell m j = (skeletonLT C n : Set X) ∩ cellFrontier m j := by @@ -973,6 +1037,7 @@ lemma RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier exact empty_subset _ /-- Version of `skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier` using `skeleton`. -/ +@[alias_in CWComplex] lemma RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier [RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : cell C m} (hnm : n < m) : (skeleton C n : Set X) ∩ closedCell m j = (skeleton C n : Set X) ∩ cellFrontier m j := @@ -996,24 +1061,4 @@ lemma RelCWComplex.disjoint_interior_base_iUnion_closedCell [T2Space X] [RelCWCo simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, disjoint_interior_base_closedCell.inter_eq, iUnion_empty] -namespace CWComplex - -export RelCWComplex (pairwiseDisjoint disjoint_openCell_of_ne openCell_subset_closedCell - cellFrontier_subset_closedCell cellFrontier_union_openCell_eq_closedCell map_zero_mem_openCell - map_zero_mem_closedCell isCompact_closedCell isClosed_closedCell isCompact_cellFrontier - isClosed_cellFrontier closure_openCell_eq_closedCell skeletonLT_top skeleton_top skeletonLT_mono - skeleton_mono skeletonLT_monotone skeleton_monotone closedCell_subset_skeletonLT - closedCell_subset_skeleton closedCell_subset_complex openCell_subset_skeletonLT - openCell_subset_skeleton - openCell_subset_complex cellFrontier_subset_skeletonLT cellFrontier_subset_skeleton - cellFrontier_subset_complex iUnion_cellFrontier_subset_skeletonLT - iUnion_cellFrontier_subset_skeleton closedCell_zero_eq_singleton openCell_zero_eq_singleton - cellFrontier_zero_eq_empty isClosed skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ - skeleton_union_iUnion_closedCell_eq_skeleton_succ iUnion_skeletonLT_eq_complex - iUnion_skeleton_eq_complex eq_of_not_disjoint_openCell disjoint_skeletonLT_openCell - disjoint_skeleton_openCell skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier - skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier) - -end CWComplex - end Topology diff --git a/Mathlib/Topology/CWComplex/Classical/Finite.lean b/Mathlib/Topology/CWComplex/Classical/Finite.lean index f28ba68f9b5798..993561d306d25e 100644 --- a/Mathlib/Topology/CWComplex/Classical/Finite.lean +++ b/Mathlib/Topology/CWComplex/Classical/Finite.lean @@ -42,18 +42,24 @@ class RelCWComplex.FiniteDimensional.{u} {X : Type u} [TopologicalSpace X] (C : /-- For some natural number `n`, the type `cell C m` is empty for all `m ≥ n`. -/ eventually_isEmpty_cell : ∀ᶠ n in Filter.atTop, IsEmpty (cell C n) +alias CWComplex.FiniteDimensional.eventually_isEmpty_cell := + RelCWComplex.FiniteDimensional.eventually_isEmpty_cell + /-- A CW complex is of finite type if `cell C n` is finite for every `n`. -/ class RelCWComplex.FiniteType.{u} {X : Type u} [TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] : Prop where /-- `cell C n` is finite for every `n`. -/ finite_cell (n : ℕ) : Finite (cell C n) +alias CWComplex.FiniteType.finite_cell := RelCWComplex.FiniteType.finite_cell + /-- A CW complex is finite if it is finite dimensional and of finite type. -/ class RelCWComplex.Finite {X : Type*} [TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] extends FiniteDimensional C, FiniteType C variable {X : Type*} [TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] +@[alias_in CWComplex] lemma RelCWComplex.finite_of_finiteDimensional_finiteType [FiniteDimensional C] [FiniteType C] : Finite C where eventually_isEmpty_cell := FiniteDimensional.eventually_isEmpty_cell @@ -61,8 +67,7 @@ lemma RelCWComplex.finite_of_finiteDimensional_finiteType [FiniteDimensional C] namespace CWComplex -export RelCWComplex (FiniteDimensional FiniteType Finite FiniteDimensional.eventually_isEmpty_cell - FiniteType.finite_cell finite_of_finiteDimensional_finiteType) +export RelCWComplex (FiniteDimensional FiniteType Finite) end CWComplex @@ -306,6 +311,7 @@ variable {X : Type*} [TopologicalSpace X] {C D : Set X} [RelCWComplex C D] /-- If the collection of all cells (of any dimension) of a relative CW complex `C` is finite, then `C` is finite as a CW complex. -/ +@[alias_in CWComplex] lemma RelCWComplex.finite_of_finite_cells (finite : _root_.Finite (Σ n, cell C n)) : Finite C where eventually_isEmpty_cell := by simp only [Filter.eventually_atTop] @@ -329,6 +335,7 @@ lemma RelCWComplex.finite_of_finite_cells (finite : _root_.Finite (Σ n, cell C /-- If `C` is finite as a CW complex then the collection of all cells (of any dimension) is finite. -/ +@[alias_in CWComplex] lemma RelCWComplex.finite_cells_of_finite [finite : Finite C] : _root_.Finite (Σ n, cell C n) := by -- We show that there is a bijection between `Σ n, cell C n` and -- `Σ (m : {m : ℕ // m < n}), cell C m`. @@ -348,13 +355,8 @@ lemma RelCWComplex.finite_cells_of_finite [finite : Finite C] : _root_.Finite ( exact Finite.instSigma /-- A CW complex is finite iff the total number of its cells is finite. -/ +@[alias_in CWComplex] lemma RelCWComplex.finite_iff_finite_cells : Finite C ↔ _root_.Finite (Σ n, cell C n) := ⟨fun h ↦ finite_cells_of_finite (finite := h), finite_of_finite_cells⟩ -namespace CWComplex - -export RelCWComplex (finite_of_finite_cells finite_cells_of_finite finite_iff_finite_cells) - -end CWComplex - end Topology diff --git a/Mathlib/Topology/CWComplex/Classical/Subcomplex.lean b/Mathlib/Topology/CWComplex/Classical/Subcomplex.lean index 438323f8296faf..3c8c3994156c1d 100644 --- a/Mathlib/Topology/CWComplex/Classical/Subcomplex.lean +++ b/Mathlib/Topology/CWComplex/Classical/Subcomplex.lean @@ -32,6 +32,7 @@ namespace Topology variable {X : Type*} [t : TopologicalSpace X] {C D : Set X} +@[alias_in CWComplex.Subcomplex] lemma RelCWComplex.Subcomplex.closedCell_subset_of_mem [T2Space X] [RelCWComplex C D] (E : Subcomplex C) {n : ℕ} {i : cell C n} (hi : i ∈ E.I n) : closedCell n i ⊆ E := by @@ -40,11 +41,13 @@ lemma RelCWComplex.Subcomplex.closedCell_subset_of_mem [T2Space X] [RelCWComplex exact subset_iUnion_of_subset n (subset_iUnion (fun (j : ↑(E.I n)) ↦ openCell (C := C) n j) ⟨i, hi⟩) +@[alias_in CWComplex.Subcomplex] lemma RelCWComplex.Subcomplex.openCell_subset_of_mem [T2Space X] [RelCWComplex C D] (E : Subcomplex C) {n : ℕ} {i : cell C n} (hi : i ∈ E.I n) : openCell n i ⊆ E := (openCell_subset_closedCell n i).trans (closedCell_subset_of_mem E hi) +@[alias_in CWComplex.Subcomplex] lemma RelCWComplex.Subcomplex.cellFrontier_subset_of_mem [T2Space X] [RelCWComplex C D] (E : Subcomplex C) {n : ℕ} {i : cell C n} (hi : i ∈ E.I n) : cellFrontier n i ⊆ E := @@ -66,6 +69,7 @@ lemma CWComplex.Subcomplex.union_closedCell [T2Space X] [CWComplex C] (E : Subco ⋃ (n : ℕ) (j : E.I n), closedCell (C := C) n j = E := (empty_union _).symm.trans (RelCWComplex.Subcomplex.union_closedCell E) +@[alias_in CWComplex.Subcomplex] lemma RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem [RelCWComplex C D] (E : Subcomplex C) {n : ℕ} {i : cell C n} (h : i ∉ E.I n) : Disjoint (openCell n i) E := by simp_rw [← union, disjoint_union_right, disjoint_iUnion_right] @@ -142,12 +146,14 @@ lemma RelCWComplex.Subcomplex.cellFrontier_eq [T2Space X] [RelCWComplex C D] (E (n : ℕ) (i : E.I n) : cellFrontier (C := E) n i = cellFrontier n (i : cell C n) := by rfl +@[alias_in CWComplex.Subcomplex] instance RelCWComplex.Subcomplex.finiteType_subcomplex_of_finiteType [T2Space X] [RelCWComplex C D] [FiniteType C] (E : Subcomplex C) : FiniteType (E : Set X) where finite_cell n := let _ := FiniteType.finite_cell (C := C) (D := D) n Subtype.finite +@[alias_in CWComplex.Subcomplex] instance RelCWComplex.Subcomplex.finiteDimensional_subcomplex_of_finiteDimensional [T2Space X] [RelCWComplex C D] [FiniteDimensional C] (E : Subcomplex C) : FiniteDimensional (E : Set X) where @@ -156,17 +162,9 @@ instance RelCWComplex.Subcomplex.finiteDimensional_subcomplex_of_finiteDimension simp [isEmpty_subtype] /-- A subcomplex of a finite CW complex is again finite. -/ +@[alias_in CWComplex.Subcomplex] instance RelCWComplex.Subcomplex.finite_subcomplex_of_finite [T2Space X] [RelCWComplex C D] [Finite C] (E : Subcomplex C) : Finite (E : Set X) := finite_of_finiteDimensional_finiteType _ -namespace CWComplex.Subcomplex - -export RelCWComplex.Subcomplex (closedCell_subset_of_mem openCell_subset_of_mem - cellFrontier_subset_of_mem disjoint_openCell_subcomplex_of_not_mem subset_complex - finiteType_subcomplex_of_finiteType finiteDimensional_subcomplex_of_finiteDimensional - finite_subcomplex_of_finite) - -end CWComplex.Subcomplex - end Topology From c3c39061306554f18e141a8008b30778118c3285 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= <4094732+RemyDegenne@users.noreply.github.com> Date: Sat, 13 Jun 2026 14:25:04 +0000 Subject: [PATCH 08/24] feat(Probability/Decision): Bayes estimators (#39810) This PR adds the concept of a Bayes estimator for an estimation problem: an estimator that attains the Bayes risk. We can get such estimators by taking an argmin of an integral involving a posterior kernel, when a measurable version of that argmin exists. Co-authored-by: Lorenzo Luccioli @LorenzoLuccioli Co-authored-by: Remy Degenne --- Mathlib.lean | 1 + .../Probability/Decision/BayesEstimator.lean | 168 ++++++++++++++++++ 2 files changed, 169 insertions(+) create mode 100644 Mathlib/Probability/Decision/BayesEstimator.lean diff --git a/Mathlib.lean b/Mathlib.lean index 09b8c19e674791..2ba33f02117f1e 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6202,6 +6202,7 @@ public import Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs public import Mathlib.Probability.CondVar public import Mathlib.Probability.ConditionalExpectation public import Mathlib.Probability.ConditionalProbability +public import Mathlib.Probability.Decision.BayesEstimator public import Mathlib.Probability.Decision.Risk.Basic public import Mathlib.Probability.Decision.Risk.Countable public import Mathlib.Probability.Decision.Risk.Defs diff --git a/Mathlib/Probability/Decision/BayesEstimator.lean b/Mathlib/Probability/Decision/BayesEstimator.lean new file mode 100644 index 00000000000000..7f3991f3a74edc --- /dev/null +++ b/Mathlib/Probability/Decision/BayesEstimator.lean @@ -0,0 +1,168 @@ +/- +Copyright (c) 2025 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne, Lorenzo Luccioli +-/ +module + +public import Mathlib.Probability.Decision.Risk.Defs +public import Mathlib.Probability.Kernel.Posterior + +import Mathlib.Probability.Decision.Risk.Basic + +/-! +# Bayes estimator + +Let `Θ` be a parameter space, `𝓧` a data space, `𝓨` a prediction space, `P : Kernel Θ 𝓧` a +data generating kernel, `π` a prior on the parameter space, and `ℓ : Θ → 𝓨 → ℝ≥0∞` a loss function. + +An estimator (a `Kernel 𝓧 𝓨`) is said to be a Bayes estimator if it attains the Bayes risk for +the estimation problem. +It can be written as a measurable function `x ↦ argmin_y P†π(x)[θ ↦ ℓ θ y]` +for `(P ∘ₘ π)`-almost every `x`, where `P†π` is the posterior kernel, whenever we can select +the argmin in a measurable way. + +## Main definitions + +* `IsBayesEstimator`: an estimator is a Bayes estimator if it attains the Bayes risk for the prior. +* `IsArgminEstimator`: a measurable function `f : 𝓧 → 𝓨` is an argmin estimator + if for `(P ∘ₘ π)`-almost every `x` the value `f x` belongs to `argmin_y P†π(x)[θ ↦ ℓ θ y]`. +* `HasArgminEstimator`: the estimation problem admits an argmin estimator. + That is, we can choose the argmin of the posterior expected loss in a measurable way. + +## Main statements + +* `lintegral_iInf_posterior_le_bayesRisk`: the Bayes risk with respect to a prior is bounded + from below by the integral over the data (with distribution `P ∘ₘ π`) of the infimum over the + possible predictions `y` of the posterior loss `∫⁻ θ, ℓ θ y ∂((P†π) x)`: + `∫⁻ x, ⨅ y : 𝓨, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π) ≤ bayesRisk ℓ P π` +* `IsArgminEstimator.isBayesEstimator`: an argmin Bayes estimator is a Bayes estimator. + That is, it minimizes the Bayesian risk. +* `bayesRisk_eq_of_hasArgminEstimator`: if the estimation problem admits an argmin estimator, + then the Bayesian risk attains the risk lower bound `∫⁻ x, ⨅ y, ∫⁻ θ, ℓ θ y ∂(P†π) x ∂(P ∘ₘ π)`. + +## TODO + +Once Mathlib has measurable selection theorems, we will be able to prove `HasArgminEstimator` under +general conditions on the measurable spaces `𝓧` and/or `𝓨`. + +-/ + +@[expose] public section + +open MeasureTheory +open scoped ENNReal NNReal + +namespace ProbabilityTheory + +variable {Θ 𝓧 𝓨 : Type*} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} + {ℓ : Θ → 𝓨 → ℝ≥0∞} {P : Kernel Θ 𝓧} {κ : Kernel 𝓧 𝓨} {π : Measure Θ} + +section Posterior + +variable [StandardBorelSpace Θ] [Nonempty Θ] + +/-- The average risk of an estimator `κ` with respect to a prior `π` can be expressed as +an integral in the following way: `R_π(κ) = ((P†π × κ) ∘ P ∘ π)[(θ, y) ↦ ℓ θ y]`. -/ +lemma avgRisk_eq_lintegral_posterior_prod + (hl : Measurable (Function.uncurry ℓ)) (P : Kernel Θ 𝓧) [IsFiniteKernel P] + (κ : Kernel 𝓧 𝓨) [IsSFiniteKernel κ] (π : Measure Θ) [IsFiniteMeasure π] : + avgRisk ℓ P κ π = ∫⁻ θy, ℓ θy.1 θy.2 ∂(((P†π) ×ₖ κ) ∘ₘ (P ∘ₘ π)) := by + rw [avgRisk, ← Measure.lintegral_compProd (f := fun θy ↦ ℓ θy.1 θy.2) (by fun_prop)] + congr + calc π ⊗ₘ (κ ∘ₖ P) = (Kernel.id ∥ₖ κ) ∘ₘ (π ⊗ₘ P) := Measure.parallelComp_comp_compProd.symm + _ = (Kernel.id ∥ₖ κ) ∘ₘ ((P†π) ×ₖ Kernel.id) ∘ₘ P ∘ₘ π := by rw [posterior_prod_id_comp] + _ = ((P†π) ×ₖ κ) ∘ₘ P ∘ₘ π := by + rw [Measure.comp_assoc, Kernel.parallelComp_comp_prod, Kernel.id_comp, Kernel.comp_id] + +lemma avgRisk_eq_lintegral_lintegral_lintegral + (hl : Measurable (Function.uncurry ℓ)) (P : Kernel Θ 𝓧) [IsFiniteKernel P] + (κ : Kernel 𝓧 𝓨) [IsSFiniteKernel κ] (π : Measure Θ) [IsFiniteMeasure π] : + avgRisk ℓ P κ π = ∫⁻ x, ∫⁻ y, ∫⁻ θ, ℓ θ y ∂(P†π) x ∂κ x ∂(P ∘ₘ π) := by + rw [avgRisk_eq_lintegral_posterior_prod hl, Measure.lintegral_bind (by fun_prop) (by fun_prop)] + congr with x + rw [Kernel.prod_apply, lintegral_prod_symm' _ (by fun_prop)] + +lemma lintegral_iInf_posterior_le_avgRisk + (hl : Measurable (Function.uncurry ℓ)) (P : Kernel Θ 𝓧) [IsFiniteKernel P] + (κ : Kernel 𝓧 𝓨) [IsMarkovKernel κ] (π : Measure Θ) [IsFiniteMeasure π] : + ∫⁻ x, ⨅ y : 𝓨, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π) ≤ avgRisk ℓ P κ π := by + rw [avgRisk_eq_lintegral_lintegral_lintegral hl] + gcongr with x + exact iInf_le_lintegral _ + +lemma lintegral_iInf_posterior_le_bayesRisk + (hl : Measurable (Function.uncurry ℓ)) (P : Kernel Θ 𝓧) [IsFiniteKernel P] + (π : Measure Θ) [IsFiniteMeasure π] : + ∫⁻ x, ⨅ y : 𝓨, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π) ≤ bayesRisk ℓ P π := + le_iInf₂ fun κ _ ↦ lintegral_iInf_posterior_le_avgRisk hl P κ π + +end Posterior + +/-- An estimator is a Bayes estimator for a prior `π` if it attains the Bayes risk for `π`. -/ +def IsBayesEstimator (ℓ : Θ → 𝓨 → ℝ≥0∞) (P : Kernel Θ 𝓧) (κ : Kernel 𝓧 𝓨) (π : Measure Θ) : Prop := + avgRisk ℓ P κ π = bayesRisk ℓ P π + +variable [StandardBorelSpace Θ] [Nonempty Θ] {f : 𝓧 → 𝓨} [IsFiniteKernel P] [IsFiniteMeasure π] + +/-- We say that a measurable function `f : 𝓧 → 𝓨` is an argmin estimator +with respect to the prior `π` if for `(P ∘ₘ π)`-almost every `x` it is of +the form `x ↦ argmin_y P†π(x)[θ ↦ ℓ θ y]`. -/ +structure IsArgminEstimator {𝓨 : Type*} [MeasurableSpace 𝓨] + (ℓ : Θ → 𝓨 → ℝ≥0∞) (P : Kernel Θ 𝓧) [IsFiniteKernel P] + (π : Measure Θ) [IsFiniteMeasure π] (f : 𝓧 → 𝓨) : Prop where + measurable : Measurable f + property : ∀ᵐ x ∂(P ∘ₘ π), ∫⁻ θ, ℓ θ (f x) ∂(P†π) x = ⨅ y, ∫⁻ θ, ℓ θ y ∂(P†π) x + +/-- Given an argmin estimator `f`, we can define a deterministic kernel. -/ +protected noncomputable +abbrev IsArgminEstimator.kernel (h : IsArgminEstimator ℓ P π f) : Kernel 𝓧 𝓨 := + Kernel.deterministic f h.measurable + +/-- The risk of an argmin estimator is the risk lower bound +`∫⁻ x, ⨅ z, ∫⁻ θ, ℓ θ z ∂(P†π) x ∂(P ∘ₘ π)`. -/ +lemma IsArgminEstimator.avgRisk_eq_lintegral_iInf (hf : IsArgminEstimator ℓ P π f) + (hl : Measurable (Function.uncurry ℓ)) : + avgRisk ℓ P hf.kernel π = ∫⁻ x, ⨅ y, ∫⁻ θ, ℓ θ y ∂(P†π) x ∂(P ∘ₘ π) := by + rw [avgRisk_eq_lintegral_lintegral_lintegral hl] + refine lintegral_congr_ae ?_ + filter_upwards [hf.property] with x hx + rwa [Kernel.lintegral_deterministic' _ (by fun_prop)] + +/-- An argmin estimator is a Bayes estimator: that is, it minimizes the Bayesian risk. -/ +lemma IsArgminEstimator.isBayesEstimator (hf : IsArgminEstimator ℓ P π f) + (hl : Measurable (Function.uncurry ℓ)) : + IsBayesEstimator ℓ P hf.kernel π := by + refine le_antisymm ?_ (bayesRisk_le_avgRisk _ _ _ _) + rw [hf.avgRisk_eq_lintegral_iInf hl] + exact lintegral_iInf_posterior_le_bayesRisk hl _ _ + +/-- The estimation problem admits an argmin estimator with respect to the prior `π`. +That is, we can choose the argmin of the posterior expected loss in a measurable way. -/ +structure HasArgminEstimator {𝓨 : Type*} [MeasurableSpace 𝓨] + (ℓ : Θ → 𝓨 → ℝ≥0∞) (P : Kernel Θ 𝓧) [IsFiniteKernel P] (π : Measure Θ) [IsFiniteMeasure π] : + Prop where + exists_isArgminEstimator : ∃ f : 𝓧 → 𝓨, IsArgminEstimator ℓ P π f + +namespace HasArgminEstimator + +/-- An estimator for an estimation problem that for `(P ∘ₘ π)`-almost every `x` is of +the form `x ↦ argmin_y P†π(x)[θ ↦ ℓ θ y]`. -/ +noncomputable +def argminEstimator (h : HasArgminEstimator ℓ P π) : 𝓧 → 𝓨 := + h.exists_isArgminEstimator.choose + +lemma isArgminEstimator_argminEstimator (h : HasArgminEstimator ℓ P π) : + IsArgminEstimator ℓ P π h.argminEstimator := + h.exists_isArgminEstimator.choose_spec + +/-- If the estimation problem admits an argmin estimator, then the Bayesian risk +attains the risk lower bound `∫⁻ x, ⨅ y, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π)`. -/ +lemma bayesRisk_eq (hl : Measurable (Function.uncurry ℓ)) (h : HasArgminEstimator ℓ P π) : + bayesRisk ℓ P π = ∫⁻ x, ⨅ y, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π) := by + rw [← h.isArgminEstimator_argminEstimator.isBayesEstimator hl, + h.isArgminEstimator_argminEstimator.avgRisk_eq_lintegral_iInf hl] + +end HasArgminEstimator + +end ProbabilityTheory From b55fea0a288e55a0ccc12c183d203073951e5861 Mon Sep 17 00:00:00 2001 From: "mathlib-splicebot[bot]" <261196803+mathlib-splicebot[bot]@users.noreply.github.com> Date: Sat, 13 Jun 2026 14:25:06 +0000 Subject: [PATCH 09/24] feat: variants of lemmas in CondJensen with a.e. inequalities for the trimmed measure (#39819) This PR was automatically created from PR #35349 by @RemyDegenne via a [review comment](https://github.com/leanprover-community/mathlib4/pull/35349#discussion_r3298163528) by @RemyDegenne. Co-authored-by: RemyDegenne <4094732+RemyDegenne@users.noreply.github.com> --- .../ConditionalExpectation/CondJensen.lean | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean index 2fe493d15670d3..7d25c166b20b66 100644 --- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean +++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean @@ -181,6 +181,15 @@ theorem ConvexOn.map_condExp_le (hm : m ≤ mα) [SigmaFinite (μ.trim hm)] filter_upwards [h1, h2, h3] with a ha hb hc simpa [← ha, ← hb] +theorem ConvexOn.map_condExp_le_trim {mE : MeasurableSpace E} [BorelSpace E] + (hm : m ≤ mα) [SigmaFinite (μ.trim hm)] + (hφ_cvx : ConvexOn ℝ s φ) (hφ_cont : LowerSemicontinuousOn φ s) + (hφ_meas : StronglyMeasurable φ) (hf : ∀ᵐ a ∂μ, f a ∈ s) + (hs : IsClosed s) (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) : + φ ∘ μ[f | m] ≤ᵐ[μ.trim hm] μ[φ ∘ f | m] := by + rw [StronglyMeasurable.ae_le_trim_iff hm (by fun_prop) (by fun_prop)] + exact hφ_cvx.map_condExp_le hm hφ_cont hf hs hf_int hφ_int + theorem ConcaveOn.condExp_map_le (hm : m ≤ mα) [SigmaFinite (μ.trim hm)] (hφ_cvx : ConcaveOn ℝ s φ) (hφ_cont : UpperSemicontinuousOn φ s) (hf : ∀ᵐ a ∂μ, f a ∈ s) (hs : IsClosed s) (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) : @@ -189,6 +198,15 @@ theorem ConcaveOn.condExp_map_le (hm : m ≤ mα) [SigmaFinite (μ.trim hm)] condExp_neg (φ ∘ f) m] with a h ha simp_all [Pi.neg_comp] +theorem ConcaveOn.condExp_map_le_trim {mE : MeasurableSpace E} [BorelSpace E] + (hm : m ≤ mα) [SigmaFinite (μ.trim hm)] + (hφ_cvx : ConcaveOn ℝ s φ) (hφ_cont : UpperSemicontinuousOn φ s) + (hφ_meas : StronglyMeasurable φ) (hf : ∀ᵐ a ∂μ, f a ∈ s) + (hs : IsClosed s) (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) : + μ[φ ∘ f | m] ≤ᵐ[μ.trim hm] φ ∘ μ[f | m] := by + rw [StronglyMeasurable.ae_le_trim_iff hm (by fun_prop) (by fun_prop)] + exact hφ_cvx.condExp_map_le hm hφ_cont hf hs hf_int hφ_int + /-- **Conditional Jensen's inequality**: in a Banach space `E` with a measure `μ` that is σ-finite on a sub-σ-algebra `m`, if `φ : E → ℝ` is convex and lower-semicontinuous, then for any `f : α → E` such that `f` and `φ ∘ f` are integrable, we have `φ (𝔼[f | m]) ≤ᵐ[μ] 𝔼[φ ∘ f | m]`. -/ @@ -199,6 +217,14 @@ theorem ConvexOn.map_condExp_le_univ (hm : m ≤ mα) [SigmaFinite (μ.trim hm)] ConvexOn.map_condExp_le hm hφ_cvx (lowerSemicontinuousOn_univ_iff.2 hφ_cont) (by simp) isClosed_univ hf_int hφ_int +theorem ConvexOn.map_condExp_le_trim_univ {mE : MeasurableSpace E} [BorelSpace E] + (hm : m ≤ mα) [SigmaFinite (μ.trim hm)] + (hφ_cvx : ConvexOn ℝ univ φ) (hφ_cont : LowerSemicontinuous φ) + (hφ_meas : StronglyMeasurable φ) (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) : + φ ∘ μ[f | m] ≤ᵐ[μ.trim hm] μ[φ ∘ f | m] := by + rw [StronglyMeasurable.ae_le_trim_iff hm (by fun_prop) (by fun_prop)] + exact hφ_cvx.map_condExp_le_univ hm hφ_cont hf_int hφ_int + theorem ConcaveOn.condExp_map_le_univ (hm : m ≤ mα) [SigmaFinite (μ.trim hm)] (hφ_cvx : ConcaveOn ℝ univ φ) (hφ_cont : UpperSemicontinuous φ) (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) : @@ -207,6 +233,14 @@ theorem ConcaveOn.condExp_map_le_univ (hm : m ≤ mα) [SigmaFinite (μ.trim hm) condExp_neg (φ ∘ f) m] with a h ha simp_all [Pi.neg_comp] +theorem ConcaveOn.condExp_map_le_trim_univ {mE : MeasurableSpace E} [BorelSpace E] + (hm : m ≤ mα) [SigmaFinite (μ.trim hm)] + (hφ_cvx : ConcaveOn ℝ univ φ) (hφ_cont : UpperSemicontinuous φ) + (hφ_meas : StronglyMeasurable φ) (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) : + μ[φ ∘ f | m] ≤ᵐ[μ.trim hm] φ ∘ μ[f | m] := by + rw [StronglyMeasurable.ae_le_trim_iff hm (by fun_prop) (by fun_prop)] + exact hφ_cvx.condExp_map_le_univ hm hφ_cont hf_int hφ_int + /-- In a Banach space `E` with a measure `μ`, then for any `f : α → E`, we have `‖𝔼[f | m]‖ ≤ᵐ[μ] 𝔼[‖f‖ | m]`. -/ theorem norm_condExp_le : (‖μ[f | m] ·‖) ≤ᵐ[μ] μ[(‖f ·‖) | m] := by From 06b9dc81c6231b5b67ef260d241f1821e3a7b1ed Mon Sep 17 00:00:00 2001 From: Felix Pernegger <188575194+felixpernegger@users.noreply.github.com> Date: Sat, 13 Jun 2026 14:25:07 +0000 Subject: [PATCH 10/24] chore: replace `(by rfl)` with `rfl` (#40371) Replaces `(by rfl)` with `rfl` whenever possible. Co-authored-by: Batixx --- Archive/Imo/Imo1982Q1.lean | 2 +- Counterexamples/CharPZeroNeCharZero.lean | 2 +- Mathlib/Algebra/DirectSum/Internal.lean | 2 +- Mathlib/Algebra/Order/CauSeq/Completion.lean | 4 ++-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean | 2 +- Mathlib/CategoryTheory/Category/PartialFun.lean | 2 +- Mathlib/CategoryTheory/Sites/Sheaf.lean | 2 +- Mathlib/Data/Vector/Basic.lean | 2 +- Mathlib/Dynamics/Flow.lean | 2 +- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean | 2 +- Mathlib/GroupTheory/FreeGroup/Basic.lean | 2 +- Mathlib/GroupTheory/MonoidLocalization/Basic.lean | 2 +- Mathlib/NumberTheory/BernoulliPolynomials.lean | 2 +- Mathlib/Order/Filter/Germ/Basic.lean | 2 +- Mathlib/RepresentationTheory/Intertwining.lean | 2 +- Mathlib/RingTheory/AdicCompletion/Completeness.lean | 6 +++--- Mathlib/RingTheory/Adjoin/Singleton.lean | 2 +- Mathlib/RingTheory/Algebraic/Basic.lean | 2 +- 18 files changed, 21 insertions(+), 21 deletions(-) diff --git a/Archive/Imo/Imo1982Q1.lean b/Archive/Imo/Imo1982Q1.lean index ef97cd79289882..544af84ecc0474 100644 --- a/Archive/Imo/Imo1982Q1.lean +++ b/Archive/Imo/Imo1982Q1.lean @@ -93,7 +93,7 @@ lemma part_1 : 660 ≤ f (1980) := by lemma part_2 : f 1980 ≤ 660 := by have h : 5 * f 1980 + 33 * f 3 ≤ 5 * 660 + 33 := by calc (5 : ℕ+) * f 1980 + (33 : ℕ+) * f 3 ≤ f (5 * 1980 + 33 * 3) := by apply hf.superlinear - _ = f 9999 := by rfl + _ = f 9999 := rfl _ = 5 * 660 + 33 := by rw [hf.f_9999] rw [hf.f₃, mul_one] at h -- from 5 * f 1980 + 33 ≤ 5 * 660 + 33 we show f 1980 ≤ 660 diff --git a/Counterexamples/CharPZeroNeCharZero.lean b/Counterexamples/CharPZeroNeCharZero.lean index 39e01fe8e56397..fcb0eb5e258ee4 100644 --- a/Counterexamples/CharPZeroNeCharZero.lean +++ b/Counterexamples/CharPZeroNeCharZero.lean @@ -24,7 +24,7 @@ namespace Counterexample @[simp] theorem add_one_eq_one (x : WithZero Unit) : x + 1 = 1 := - WithZero.cases_on x (by rfl) fun h => by rfl + WithZero.cases_on x rfl fun h => by rfl theorem withZero_unit_charP_zero : CharP (WithZero Unit) 0 := ⟨fun x => by cases x <;> simp⟩ diff --git a/Mathlib/Algebra/DirectSum/Internal.lean b/Mathlib/Algebra/DirectSum/Internal.lean index 4aeb4fab711013..b0f553a0a9d362 100644 --- a/Mathlib/Algebra/DirectSum/Internal.lean +++ b/Mathlib/Algebra/DirectSum/Internal.lean @@ -320,7 +320,7 @@ theorem Submodule.iSup_eq_toSubmodule_range [AddMonoid ι] [CommSemiring S] [Sem theorem DirectSum.coeAlgHom_of [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R] (A : ι → Submodule S R) [SetLike.GradedMonoid A] (i : ι) (x : A i) : DirectSum.coeAlgHom A (DirectSum.of (fun i => A i) i x) = x := - DirectSum.toSemiring_of _ (by rfl) (fun _ _ => (by rfl)) _ _ + DirectSum.toSemiring_of _ rfl (fun _ _ => rfl) _ _ end DirectSum diff --git a/Mathlib/Algebra/Order/CauSeq/Completion.lean b/Mathlib/Algebra/Order/CauSeq/Completion.lean index b48635495389f0..9d8794438abc3f 100644 --- a/Mathlib/Algebra/Order/CauSeq/Completion.lean +++ b/Mathlib/Algebra/Order/CauSeq/Completion.lean @@ -142,7 +142,7 @@ theorem ofRat_injective : Function.Injective (ofRat : β → Cauchy abv) := fun simpa [ofRat, mk_eq, ← const_sub, const_limZero, sub_eq_zero] using h instance Cauchy.ring : Ring (Cauchy abv) := fast_instance% - Function.Surjective.ring mk Quotient.mk'_surjective (by rfl) (by rfl) + Function.Surjective.ring mk Quotient.mk'_surjective rfl rfl (fun _ _ => (mk_add _ _).symm) (fun _ _ => (mk_mul _ _).symm) (fun _ => (mk_neg _).symm) (fun _ _ => (mk_sub _ _).symm) (fun _ _ => (mk_smul _ _).symm) (fun _ _ => (mk_smul _ _).symm) (fun _ _ => (mk_pow _ _).symm) (fun _ => rfl) fun _ => rfl @@ -170,7 +170,7 @@ variable {α : Type*} [Field α] [LinearOrder α] [IsStrictOrderedRing α] variable {β : Type*} [CommRing β] {abv : β → α} [IsAbsoluteValue abv] instance Cauchy.commRing : CommRing (Cauchy abv) := fast_instance% - Function.Surjective.commRing mk Quotient.mk'_surjective (by rfl) (by rfl) + Function.Surjective.commRing mk Quotient.mk'_surjective rfl rfl (fun _ _ => (mk_add _ _).symm) (fun _ _ => (mk_mul _ _).symm) (fun _ => (mk_neg _).symm) (fun _ _ => (mk_sub _ _).symm) (fun _ _ => (mk_smul _ _).symm) (fun _ _ => (mk_smul _ _).symm) (fun _ _ => (mk_pow _ _).symm) (fun _ => rfl) fun _ => rfl diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean index 9fe6d6e66a330f..40edeb5bc6a42d 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean @@ -242,7 +242,7 @@ theorem GammaSeq_add_one_left (s : ℂ) {n : ℕ} (hn : n ≠ 0) : ← mul_assoc, mul_comm _ (Finset.prod _ _)] congr 3 · rw [cpow_add _ _ (Nat.cast_ne_zero.mpr hn), cpow_one, mul_comm] - · refine Finset.prod_congr (by rfl) fun x _ => ?_ + · refine Finset.prod_congr rfl fun x _ => ?_ push_cast; ring · abel diff --git a/Mathlib/CategoryTheory/Category/PartialFun.lean b/Mathlib/CategoryTheory/Category/PartialFun.lean index b6a34630701d81..d544ff514b4e8e 100644 --- a/Mathlib/CategoryTheory/Category/PartialFun.lean +++ b/Mathlib/CategoryTheory/Category/PartialFun.lean @@ -146,7 +146,7 @@ noncomputable def partialFunEquivPointed : PartialFun.{u} ≌ Pointed where exact hw.symm counitIso := NatIso.ofComponents - (fun X ↦ Pointed.Iso.mk (by classical exact Equiv.optionSubtypeNe X.point) (by rfl)) + (fun X ↦ Pointed.Iso.mk (by classical exact Equiv.optionSubtypeNe X.point) rfl) fun {X Y} f ↦ Pointed.Hom.ext <| funext fun a ↦ by obtain _ | ⟨a, ha⟩ := a · exact f.map_point.symm diff --git a/Mathlib/CategoryTheory/Sites/Sheaf.lean b/Mathlib/CategoryTheory/Sites/Sheaf.lean index 0483c6977df99f..1ee14826e07ea4 100644 --- a/Mathlib/CategoryTheory/Sites/Sheaf.lean +++ b/Mathlib/CategoryTheory/Sites/Sheaf.lean @@ -103,7 +103,7 @@ def conesEquivSieveCompatibleFamily : toFun π := ⟨fun _ f h => π.app (op ⟨Over.mk f, h⟩), fun X Y f g hf => by let φ : S.arrows.categoryMk (g ≫ f) (S.downward_closed hf g) ⟶ - S.arrows.categoryMk f hf := ObjectProperty.homMk (Over.homMk _ (by rfl)) + S.arrows.categoryMk f hf := ObjectProperty.homMk (Over.homMk _ rfl) simpa using! π.naturality φ.op⟩ invFun x := { app := fun f => x.1 f.unop.1.hom f.unop.2 diff --git a/Mathlib/Data/Vector/Basic.lean b/Mathlib/Data/Vector/Basic.lean index 7ceba21415a26f..a056a01b21f9fc 100644 --- a/Mathlib/Data/Vector/Basic.lean +++ b/Mathlib/Data/Vector/Basic.lean @@ -522,7 +522,7 @@ def casesOn₃ {motive : ∀ {n}, Vector α n → Vector β n → Vector γ n /-- Cast a vector to an array. -/ def toArray : Vector α n → Array α - | ⟨xs, _⟩ => cast (by rfl) xs.toArray + | ⟨xs, _⟩ => xs.toArray section InsertIdx diff --git a/Mathlib/Dynamics/Flow.lean b/Mathlib/Dynamics/Flow.lean index 6c6fe71cb8f661..bad8543dece3ee 100644 --- a/Mathlib/Dynamics/Flow.lean +++ b/Mathlib/Dynamics/Flow.lean @@ -247,7 +247,7 @@ theorem IsFactorOf.trans (h₁ : IsFactorOf ϕ ψ) (h₂ : IsFactorOf ψ χ) : I h₁.elim fun π hπ => h₂.elim fun ρ hρ => ⟨π ∘ ρ, hρ.comp χ ψ ϕ hπ⟩ /-- Every flow is a factor of itself. -/ -theorem IsFactorOf.self : IsFactorOf ϕ ϕ := ⟨id, (isSemiconjugacy_id_iff_eq ϕ ϕ).mpr (by rfl)⟩ +theorem IsFactorOf.self : IsFactorOf ϕ ϕ := ⟨id, (isSemiconjugacy_id_iff_eq ϕ ϕ).mpr rfl⟩ end Flow diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean index 12e8258353a615..3f596fe43485df 100644 --- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean +++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean @@ -601,7 +601,7 @@ instance : Algebra A⟮b⟯ A⟮(algebraMap B C) b⟯ := RingHom.toAlgebra (RingHom.adjoinAlgebraMap _) instance : IsScalarTower A⟮b⟯ A⟮(algebraMap B C) b⟯ C := - IsScalarTower.of_algebraMap_eq' (by rfl) + IsScalarTower.of_algebraMap_eq' rfl end AdjoinSimple diff --git a/Mathlib/GroupTheory/FreeGroup/Basic.lean b/Mathlib/GroupTheory/FreeGroup/Basic.lean index 8a1e4753bdb254..3a4a00e0b12b57 100644 --- a/Mathlib/GroupTheory/FreeGroup/Basic.lean +++ b/Mathlib/GroupTheory/FreeGroup/Basic.lean @@ -931,7 +931,7 @@ def freeGroupUnitEquivInt : FreeGroup Unit ≃ ℤ where rintro ⟨L⟩ simp only [quot_mk_eq_mk, map.mk, sum_mk, List.map_map] exact List.recOn L - (by rfl) + rfl (fun ⟨⟨⟩, b⟩ tl ih => by cases b <;> simp [zpow_add, ih] <;> rfl) right_inv x := diff --git a/Mathlib/GroupTheory/MonoidLocalization/Basic.lean b/Mathlib/GroupTheory/MonoidLocalization/Basic.lean index b8440d8c517a69..6b2cb8e36d0c07 100644 --- a/Mathlib/GroupTheory/MonoidLocalization/Basic.lean +++ b/Mathlib/GroupTheory/MonoidLocalization/Basic.lean @@ -235,7 +235,7 @@ then `f` is defined on the whole `AddLocalization S`. -/] def rec {p : Localization S → Sort u} (f : ∀ (a : M) (b : S), p (mk a b)) (H : ∀ {a c : M} {b d : S} (h : r S (a, b) (c, d)), (Eq.ndrec (f a b) (mk_eq_mk_iff.mpr h) : p (mk c d)) = f c d) (x) : p x := - Quot.rec (fun y ↦ Eq.ndrec (f y.1 y.2) (by rfl)) + Quot.rec (fun y ↦ f y.1 y.2) (fun y z h ↦ by cases y; cases z; exact H (r_iff_oreEqv_r.mpr h)) x /-- Copy of `Quotient.recOnSubsingleton₂` for `Localization` -/ diff --git a/Mathlib/NumberTheory/BernoulliPolynomials.lean b/Mathlib/NumberTheory/BernoulliPolynomials.lean index 6adffaddb78dfa..51e293fd0ad465 100644 --- a/Mathlib/NumberTheory/BernoulliPolynomials.lean +++ b/Mathlib/NumberTheory/BernoulliPolynomials.lean @@ -111,7 +111,7 @@ theorem derivative_bernoulli_add_one (k : ℕ) : rw [range_add_one, sum_insert notMem_range_self, tsub_self, cast_zero, mul_zero, map_zero, zero_add, mul_sum] -- the rest of the sum is termwise equal: - refine sum_congr (by rfl) fun m _ => ?_ + refine sum_congr rfl fun m _ => ?_ conv_rhs => rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_natCast, C_mul_monomial, mul_comm] rw [mul_assoc, mul_assoc, ← Nat.cast_mul, ← Nat.cast_mul] congr 3 diff --git a/Mathlib/Order/Filter/Germ/Basic.lean b/Mathlib/Order/Filter/Germ/Basic.lean index 7390a26c100c7e..dd0aa8723d3e62 100644 --- a/Mathlib/Order/Filter/Germ/Basic.lean +++ b/Mathlib/Order/Filter/Germ/Basic.lean @@ -406,7 +406,7 @@ theorem const_pow [Pow G M] (a : G) (n : M) : (↑(a ^ n) : Germ l G) = (↑a : -- TODO: https://github.com/leanprover-community/mathlib4/pull/7432 @[to_additive] instance instMonoid [Monoid M] : Monoid (Germ l M) := - { Function.Surjective.monoid ofFun Quot.mk_surjective (by rfl) + { Function.Surjective.monoid ofFun Quot.mk_surjective rfl (fun _ _ => by rfl) fun _ _ => by rfl with toSemigroup := instSemigroup toOne := instOne diff --git a/Mathlib/RepresentationTheory/Intertwining.lean b/Mathlib/RepresentationTheory/Intertwining.lean index a4931239af1b82..ebcc0244e85ec0 100644 --- a/Mathlib/RepresentationTheory/Intertwining.lean +++ b/Mathlib/RepresentationTheory/Intertwining.lean @@ -498,7 +498,7 @@ noncomputable def equivAlgEnd : IntertwiningMap ρ ρ ≃ₐ[A] Module.End A[G] ρ.asModule := AlgEquiv.ofLinearEquiv (equivLinearMapAsModule ρ ρ) - (by rfl) + rfl (by intro f g; rfl) theorem isIntertwiningMap_of_mem_center (g : G) (hg : g ∈ Submonoid.center G) : diff --git a/Mathlib/RingTheory/AdicCompletion/Completeness.lean b/Mathlib/RingTheory/AdicCompletion/Completeness.lean index ef7db25d3cb756..5f8b5b456c3b61 100644 --- a/Mathlib/RingTheory/AdicCompletion/Completeness.lean +++ b/Mathlib/RingTheory/AdicCompletion/Completeness.lean @@ -102,8 +102,8 @@ def ofValEqZero {n : ℕ} {x : AdicCompletion I M} (hxn : x.val n = 0) : val i := ofValEqZeroAux I (Eq.refl (i + n)) hxn property {i j} h := by obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h - rw [← (powSMulQuotInclusion_injective I (by rfl) ⊤).eq_iff, ofValEqZeroAux_prop, - ← LinearMap.comp_apply, ← factorPow_comp_powSMulQuotInclusion I (by rfl) + rw [← (powSMulQuotInclusion_injective I rfl ⊤).eq_iff, ofValEqZeroAux_prop, + ← LinearMap.comp_apply, ← factorPow_comp_powSMulQuotInclusion I rfl (show i + k + n = k + (i + n) by ring), LinearMap.comp_apply, ofValEqZeroAux_prop] exact x.prop (by lia) @@ -112,7 +112,7 @@ theorem ofPowSMul_ofValEqZero {n : ℕ} {x : AdicCompletion I M} (hxn : x.val n ofPowSMul I M n (ofValEqZero I hxn) = x := by ext i; by_cases! h : n ≤ i · obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' h - rw [ofPowSMul_val_apply _ (by rfl), ofValEqZero, ofValEqZeroAux_prop] + rw [ofPowSMul_val_apply _ rfl, ofValEqZero, ofValEqZeroAux_prop] rw [ofPowSMul_val_apply_eq_zero _ h.le, ← x.prop h.le, hxn, _root_.map_zero] theorem restrictScalars_range_ofPowSMul_eq_ker_eval {n : ℕ} : diff --git a/Mathlib/RingTheory/Adjoin/Singleton.lean b/Mathlib/RingTheory/Adjoin/Singleton.lean index 1bde86bb66cd0c..2b26c1ddf9c972 100644 --- a/Mathlib/RingTheory/Adjoin/Singleton.lean +++ b/Mathlib/RingTheory/Adjoin/Singleton.lean @@ -55,7 +55,7 @@ instance : Algebra A[b] A[(algebraMap B C) b] := RingHom.toAlgebra (RingHom.adjoinAlgebraMap b) instance : IsScalarTower A[b] A[(algebraMap B C) b] C := - IsScalarTower.of_algebraMap_eq' (by rfl) + IsScalarTower.of_algebraMap_eq' rfl /-- If the `algebraMap` injective then we have a Ring isomorphism between A[b] and A[↑b]. -/ noncomputable def RingHom.adjoinAlgebraMapEquiv [FaithfulSMul B C] : diff --git a/Mathlib/RingTheory/Algebraic/Basic.lean b/Mathlib/RingTheory/Algebraic/Basic.lean index d1fefdb9b42f5a..e4771691dbe162 100644 --- a/Mathlib/RingTheory/Algebraic/Basic.lean +++ b/Mathlib/RingTheory/Algebraic/Basic.lean @@ -343,7 +343,7 @@ theorem isAlgebraic_of_isAlgebraic_bot {x : S} (halg : IsAlgebraic (⊥ : Subalg theorem isAlgebraic_bot_iff (h : Function.Injective (algebraMap R S)) {x : S} : IsAlgebraic (⊥ : Subalgebra R S) x ↔ IsAlgebraic R x := isAlgebraic_ringHom_iff_of_comp_eq (Algebra.botEquivOfInjective h).symm (RingHom.id S) - Function.injective_id (by rfl) + Function.injective_id rfl variable (R S) in theorem algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left From f1ceb733fa418759932c458de4f14076f8d15efe Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Sat, 13 Jun 2026 14:25:09 +0000 Subject: [PATCH 11/24] feat: clean up `PositiveLinearMap` and add API (#40492) Among other things, this removes the coercion from the morphism class into the morphism type, and renames the underlying convenience constructor to `PositiveLinearMap.ofClass`. --- .../Order/Module/PositiveLinearMap.lean | 46 ++++++++++++++----- .../CStarAlgebra/PositiveLinearMap.lean | 2 +- 2 files changed, 36 insertions(+), 12 deletions(-) diff --git a/Mathlib/Algebra/Order/Module/PositiveLinearMap.lean b/Mathlib/Algebra/Order/Module/PositiveLinearMap.lean index b5141ae70a6e97..e32de62a976895 100644 --- a/Mathlib/Algebra/Order/Module/PositiveLinearMap.lean +++ b/Mathlib/Algebra/Order/Module/PositiveLinearMap.lean @@ -38,7 +38,7 @@ add_decl_doc PositiveLinearMap.toOrderHom /-- Notation for a `PositiveLinearMap`. -/ notation:25 E " →ₚ[" R:25 "] " F:0 => PositiveLinearMap R E F -namespace PositiveLinearMapClass +section PositiveLinearMapClass variable {F R E₁ E₂ : Type*} [Semiring R] [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] @@ -46,16 +46,15 @@ variable {F R E₁ E₂ : Type*} [Semiring R] [OrderHomClass F E₁ E₂] /-- Reinterpret an element of a type of positive linear maps as a positive linear map. -/ -def toPositiveLinearMap (f : F) : E₁ →ₚ[R] E₂ := +def PositiveLinearMap.ofClass (f : F) : E₁ →ₚ[R] E₂ := { (f : E₁ →ₗ[R] E₂), (f : E₁ →o E₂) with } -/-- Reinterpret an element of a type of positive linear maps as a positive linear map. -/ -instance instCoeToLinearMap : CoeHead F (E₁ →ₚ[R] E₂) where - coe f := toPositiveLinearMap f +@[deprecated (since := "2026-06-10")] +alias PositiveLinearMapClass.toPositiveLinearMap := PositiveLinearMap.ofClass -/-- An additive group homomorphism that maps nonnegative elements to nonnegative elements -is an order homomorphism. -/ -lemma _root_.OrderHomClass.of_addMonoidHom {F' E₁' E₂' : Type*} [FunLike F' E₁' E₂'] [AddGroup E₁'] +/-- A type of additive group homomorphisms that map nonnegative elements to nonnegative elements +is also a type of order homomorphisms. -/ +lemma OrderHomClass.of_addMonoidHom {F' E₁' E₂' : Type*} [FunLike F' E₁' E₂'] [AddGroup E₁'] [LE E₁'] [AddRightMono E₁'] [AddGroup E₂'] [LE E₂'] [AddRightMono E₂'] [AddMonoidHomClass F' E₁' E₂'] (h : ∀ f : F', ∀ x, 0 ≤ x → 0 ≤ f x) : OrderHomClass F' E₁' E₂' where @@ -67,9 +66,11 @@ namespace PositiveLinearMap section general -variable {R E₁ E₂ : Type*} [Semiring R] - [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂] - [Module R E₁] [Module R E₂] +variable {R E₁ E₂ E₃ : Type*} [Semiring R] + [AddCommMonoid E₁] [PartialOrder E₁] + [AddCommMonoid E₂] [PartialOrder E₂] + [AddCommMonoid E₃] [PartialOrder E₃] + [Module R E₁] [Module R E₂] [Module R E₃] instance : FunLike (E₁ →ₚ[R] E₂) E₁ E₂ where coe f := f.toFun @@ -80,10 +81,33 @@ instance : FunLike (E₁ →ₚ[R] E₂) E₁ E₂ where apply DFunLike.coe_injective exact h +initialize_simps_projections PositiveLinearMap (toFun → apply, as_prefix toLinearMap) + @[ext] lemma ext {f g : E₁ →ₚ[R] E₂} (h : ∀ x, f x = g x) : f = g := DFunLike.ext f g h +variable (R E₁) in +/-- The identity as a positive linear map. -/ +@[simps! apply toLinearMap] protected def id : E₁ →ₚ[R] E₁ where + __ := LinearMap.id + __ := OrderHom.id + +@[simp] lemma toOrderHom_id : (PositiveLinearMap.id R E₁).toOrderHom = .id := rfl + +/-- The composition of positive linear maps is again a positive linear map. -/ +@[simps! apply toLinearMap] +def comp (g : E₂ →ₚ[R] E₃) (f : E₁ →ₚ[R] E₂) : E₁ →ₚ[R] E₃ where + toLinearMap := g.toLinearMap.comp f.toLinearMap + monotone' := g.monotone'.comp f.monotone' + +@[simp] lemma toOrderHom_comp (g : E₂ →ₚ[R] E₃) (f : E₁ →ₚ[R] E₂) : + (g.comp f).toOrderHom = g.toOrderHom.comp f.toOrderHom := + rfl + +@[simp] lemma comp_id (f : E₁ →ₚ[R] E₂) : f.comp (.id R E₁) = f := rfl +@[simp] lemma id_comp (f : E₁ →ₚ[R] E₂) : (PositiveLinearMap.id R E₂).comp f = f := rfl + instance : LinearMapClass (E₁ →ₚ[R] E₂) R E₁ E₂ where map_add f := map_add f.toLinearMap map_smulₛₗ f := f.toLinearMap.map_smul' diff --git a/Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean b/Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean index dc4dabe59f7fbd..a5d0adb3aab838 100644 --- a/Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean +++ b/Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean @@ -130,7 +130,7 @@ instance {F : Type*} [FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] [Ord ContinuousLinearMapClass F ℂ A₁ A₂ where map_continuous f := by have hbound : ∃ C : ℝ, ∀ a, ‖f a‖ ≤ C * ‖a‖ := by - obtain ⟨C, h⟩ := exists_norm_apply_le (f : A₁ →ₚ[ℂ] A₂) + obtain ⟨C, h⟩ := exists_norm_apply_le (.ofClass f) exact ⟨C, h⟩ exact (LinearMap.mkContinuousOfExistsBound (f : A₁ →ₗ[ℂ] A₂) hbound).continuous From dab4b77c11870a1b54bd22fa185abdbf74bada85 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Sat, 13 Jun 2026 14:25:11 +0000 Subject: [PATCH 12/24] feat: selfadjointness for comparable elements in a star ordered ring (#40513) --- Mathlib/Algebra/Order/Star/Basic.lean | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Order/Star/Basic.lean b/Mathlib/Algebra/Order/Star/Basic.lean index 5e2ab31abba409..99fa9e39b070f5 100644 --- a/Mathlib/Algebra/Order/Star/Basic.lean +++ b/Mathlib/Algebra/Order/Star/Basic.lean @@ -171,7 +171,7 @@ section NonUnitalSemiring variable [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] -lemma IsSelfAdjoint.mono {x y : R} (h : x ≤ y) (hx : IsSelfAdjoint x) : IsSelfAdjoint y := by +lemma IsSelfAdjoint.of_ge {x y : R} (h : x ≤ y) (hx : IsSelfAdjoint x) : IsSelfAdjoint y := by rw [StarOrderedRing.le_iff] at h obtain ⟨d, hd, rfl⟩ := h rw [IsSelfAdjoint, star_add, hx.star_eq] @@ -180,9 +180,11 @@ lemma IsSelfAdjoint.mono {x y : R} (h : x ≤ y) (hx : IsSelfAdjoint x) : IsSelf rintro - ⟨s, rfl⟩ simp +@[deprecated (since := "2026-06-12")] alias IsSelfAdjoint.mono := IsSelfAdjoint.of_ge + @[aesop 10% apply, grind ←] lemma IsSelfAdjoint.of_nonneg {x : R} (hx : 0 ≤ x) : IsSelfAdjoint x := - .mono hx <| .zero R + .of_ge hx <| .zero R /-- An alias of `IsSelfAdjoint.of_nonneg` for use with dot notation. -/ alias LE.le.isSelfAdjoint := IsSelfAdjoint.of_nonneg @@ -204,6 +206,7 @@ protected theorem IsSelfAdjoint.mul_self_nonneg {a : R} (ha : IsSelfAdjoint a) : simpa [ha.star_eq] using star_mul_self_nonneg a /-- A star projection is non-negative in a star-ordered ring. -/ +@[grind →, aesop safe forward (rule_sets := [CStarAlgebra])] theorem IsStarProjection.nonneg {p : R} (hp : IsStarProjection p) : 0 ≤ p := hp.isIdempotentElem ▸ hp.isSelfAdjoint.mul_self_nonneg @@ -316,6 +319,19 @@ theorem mul_star_self_pos [Nontrivial R] {x : R} (hx : IsRegular x) : 0 < x * st end NonUnitalSemiring +section NonUnitalRing + +variable [NonUnitalRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] + +lemma IsSelfAdjoint.iff_of_le {a b : R} (hab : a ≤ b) : + IsSelfAdjoint a ↔ IsSelfAdjoint b := by + replace hab := (sub_nonneg.mpr hab).isSelfAdjoint + aesop (add simp IsSelfAdjoint) + +alias ⟨_, IsSelfAdjoint.of_le⟩ := IsSelfAdjoint.iff_of_le + +end NonUnitalRing + section Semiring variable [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] From 9e7b1c1166169f7aa90a08054ce9b97948d44083 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta <29959226+b-mehta@users.noreply.github.com> Date: Sat, 13 Jun 2026 17:40:35 +0000 Subject: [PATCH 13/24] feat(Analysis/Complex/Exponential): add new bounds on exponential (#39690) We add new upper bounds on Real.exp in terms of 2x/(2+x), and use these to move some bounds on log higher in mathlib. We also add a lemma for the common bound (1+1/n)^n <= e, though this is a special-case of `one_sub_div_pow_le_exp_neg` (immediately before), but is added for convenience and discoverability, as this is a "well-known" bound. --- Mathlib/Analysis/Complex/Exponential.lean | 25 +++++++++++++++++++ .../Analysis/Complex/ExponentialBounds.lean | 2 +- .../Analysis/SpecialFunctions/Log/Basic.lean | 10 ++++++++ .../Analysis/SpecialFunctions/Log/Deriv.lean | 10 -------- 4 files changed, 36 insertions(+), 11 deletions(-) diff --git a/Mathlib/Analysis/Complex/Exponential.lean b/Mathlib/Analysis/Complex/Exponential.lean index d2ba768f73a164..4fbc28c76c4d3e 100644 --- a/Mathlib/Analysis/Complex/Exponential.lean +++ b/Mathlib/Analysis/Complex/Exponential.lean @@ -11,6 +11,8 @@ public import Mathlib.Algebra.Order.CauSeq.BigOperators public import Mathlib.Algebra.Order.Star.Basic public import Mathlib.Data.Complex.BigOperators public import Mathlib.Data.Nat.Choose.Sum +public import Mathlib.Tactic.NormNum.BigOperators +public import Mathlib.Tactic.NormNum.NatFactorial /-! # Exponential Function @@ -648,12 +650,35 @@ theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t · exact one_sub_le_exp_neg _ _ = rexp (-t) := by rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]; positivity +lemma one_add_inv_pow_le_exp {n : ℕ} : (1 + (n : ℝ)⁻¹) ^ n ≤ exp 1 := by + convert one_sub_div_pow_le_exp_neg (n := n) (t := -1) (by grind) using 1 + · field + · simp + lemma le_inv_mul_exp (x : ℝ) {c : ℝ} (hc : 0 < c) : x ≤ c⁻¹ * exp (c * x) := by rw [le_inv_mul_iff₀ hc] calc c * x _ ≤ c * x + 1 := le_add_of_nonneg_right zero_le_one _ ≤ _ := Real.add_one_le_exp (c * x) +lemma exp_lt_two_add_div_two_sub {x : ℝ} (hx : 0 < x) (hx' : x < 2) : + exp x < (2 + x) / (2 - x) := by calc + _ = exp (x / 2) ^ 2 := by grind [Real.exp_nat_mul (x / 2) 2] + _ ≤ _ := by + grw [Real.exp_bound' (x := x / 2) (by grind) (by grind) (n := 3) (by simp)] + apply Real.exp_nonneg + _ < (2 + x) / (2 - x) := by + rw [lt_div_iff₀ (by linarith), ← sub_pos] + simp only [Finset.sum_range_succ] + ring_nf + positivity + +lemma exp_le_two_add_div_two_sub {x : ℝ} (hx : 0 ≤ x) (hx' : x < 2) : + exp x ≤ (2 + x) / (2 - x) := by + obtain rfl | hx₀ := hx.eq_or_lt + · simp + · exact (exp_lt_two_add_div_two_sub hx₀ hx').le + theorem prod_one_add_le_exp_sum {ι : Type*} (s : Finset ι) {f : ι → ℝ} (hf : ∀ i, 0 ≤ f i) : ∏ i ∈ s, (1 + f i) ≤ exp (∑ i ∈ s, f i) := (Finset.prod_le_prod (fun i _ ↦ add_nonneg zero_le_one (hf i)) diff --git a/Mathlib/Analysis/Complex/ExponentialBounds.lean b/Mathlib/Analysis/Complex/ExponentialBounds.lean index 56d1b556a6c820..190f489b95125a 100644 --- a/Mathlib/Analysis/Complex/ExponentialBounds.lean +++ b/Mathlib/Analysis/Complex/ExponentialBounds.lean @@ -77,7 +77,7 @@ theorem log_two_near_10 : |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10 := by norm_num1 at z rw [one_div (2 : ℝ), log_inv, ← sub_eq_add_neg, _root_.abs_sub_comm] at z apply le_trans (_root_.abs_sub_le _ _ _) (add_le_add z _) - norm_num [sum_range_succ] + norm_num theorem log_two_gt_d9 : 0.6931471803 < log 2 := lt_of_lt_of_le (by norm_num1) (sub_le_comm.1 (abs_sub_le_iff.1 log_two_near_10).2) diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean index 04ddb94fdc1d91..ab6a43aa827bb2 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean @@ -336,6 +336,16 @@ theorem abs_log_mul_self_lt (x : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) : |log x * x| rw [← abs_of_nonneg aux, neg_mul, abs_neg] at this exact this +lemma le_log_one_add_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 2 * x / (x + 2) ≤ log (1 + x) := by + rw [le_log_iff_exp_le (by grind)] + convert exp_le_two_add_div_two_sub (x := 2 * x / (x + 2)) (by positivity) _ using 1 + all_goals field_simp; grind + +lemma lt_log_one_add_of_pos {x : ℝ} (hx : 0 < x) : 2 * x / (x + 2) < log (1 + x) := by + rw [lt_log_iff_exp_lt (by grind)] + convert exp_lt_two_add_div_two_sub (x := 2 * x / (x + 2)) (by positivity) _ using 1 + all_goals field_simp; grind + /-- The real logarithm function tends to `+∞` at `+∞`. -/ theorem tendsto_log_atTop : Tendsto log atTop atTop := tendsto_comp_exp_atTop.1 <| by simpa only [log_exp] using! tendsto_id diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean index a8ca2fea64a7fa..99ebf667e962ce 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean @@ -423,14 +423,4 @@ theorem hasSum_log_one_add {a : ℝ} (h : 0 ≤ a) : · convert! hasSum_log_one_add_inv (inv_pos.mpr (lt_of_le_of_ne h ha0.symm)) using 4 all_goals simp [field, add_comm] -lemma le_log_one_add_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 2 * x / (x + 2) ≤ log (1 + x) := by - convert! le_hasSum (hasSum_log_one_add hx) 0 (by intros; positivity) using 1 - simp [field] - -lemma lt_log_one_add_of_pos {x : ℝ} (hx : 0 < x) : 2 * x / (x + 2) < log (1 + x) := by - convert! - lt_hasSum (hasSum_log_one_add hx.le) 0 (by intros; positivity) 1 (by positivity) - (by positivity) using 1 - simp [field] - end Real From 57249a69cc0b63f6eb5d0d3f1b06c34f16a22e52 Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sat, 13 Jun 2026 19:59:05 -0700 Subject: [PATCH 14/24] Add to_dual tags for conditionally complete lattice lemmas --- .../ConditionallyCompleteLattice/Basic.lean | 17 +- .../ConditionallyCompleteLattice/Indexed.lean | 229 ++++-------------- 2 files changed, 58 insertions(+), 188 deletions(-) diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean index 31ad01f242423e..9237a25656763b 100644 --- a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean +++ b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean @@ -68,7 +68,7 @@ theorem WithTop.sInf_eq [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) sInf s = ↑(sInf ((↑) ⁻¹' s) : α) := if_neg <| by simp [hs, h's] -@[simp] +@[to_dual (attr := simp)] theorem WithTop.sInf_empty [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ := if_pos <| by simp @@ -105,10 +105,6 @@ theorem WithTop.coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) : · exact Option.some_injective _ · rintro ⟨x, _, ⟨⟩⟩ -@[simp] -theorem WithBot.sSup_empty [SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥ := - WithTop.sInf_empty (α := αᵒᵈ) - @[to_dual] theorem WithTop.sSup_empty (α : Type*) [CompleteLattice α] : (sSup ∅ : WithTop α) = ⊥ := by rw [sSup_eq (by simp) (OrderTop.bddAbove _), Set.preimage_empty, _root_.sSup_empty, coe_bot] @@ -264,19 +260,16 @@ theorem notMem_of_csSup_lt {x : α} {s : Set α} (h : sSup s < x) (hs : BddAbove /-- Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that `b` is larger than all elements of `s`, and that this is not the case of any `wb`. +See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/] theorem csSup_eq_of_forall_le_of_forall_lt_exists_gt (hs : s.Nonempty) (H : ∀ a ∈ s, a ≤ b) (H' : ∀ w, w < b → ∃ a ∈ s, w < a) : sSup s = b := (eq_of_le_of_not_lt (csSup_le hs H)) fun hb => let ⟨_, ha, ha'⟩ := H' _ hb lt_irrefl _ <| ha'.trans_le <| le_csSup ⟨b, H⟩ ha -/-- Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b` -is smaller than all elements of `s`, and that this is not the case of any `w>b`. -See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/ -theorem csInf_eq_of_forall_ge_of_forall_gt_exists_lt : - s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ w, b < w → ∃ a ∈ s, a < w) → sInf s = b := - csSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ) - /-- `b < sSup s` when there is an element `a` in `s` with `b < a`, when `s` is bounded above. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness above for one direction, nonemptiness and linear diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean index 65502dab75bcbf..558f50fc38df58 100644 --- a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean +++ b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean @@ -33,30 +33,21 @@ Extension of `iSup` and `iInf` from a preorder `α` to `WithTop α` and `WithBot variable [Preorder α] -@[simp] +@[to_dual (attr := simp)] theorem WithTop.iInf_empty [IsEmpty ι] [InfSet α] (f : ι → WithTop α) : - ⨅ i, f i = ⊤ := by rw [iInf, range_eq_empty, WithTop.sInf_empty] + ⨅ i, f i = ⊤ := by + rw [iInf_of_isEmpty, WithTop.sInf_empty] -@[norm_cast] +@[to_dual (attr := norm_cast)] theorem WithTop.coe_iInf [Nonempty ι] [InfSet α] {f : ι → α} (hf : BddBelow (range f)) : ↑(⨅ i, f i) = (⨅ i, f i : WithTop α) := by rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def] -@[norm_cast] +@[to_dual (attr := norm_cast)] theorem WithTop.coe_iSup [SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) : ↑(⨆ i, f i) = (⨆ i, f i : WithTop α) := by rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def] -@[simp] -theorem WithBot.ciSup_empty [IsEmpty ι] [SupSet α] (f : ι → WithBot α) : - ⨆ i, f i = ⊥ := - WithTop.iInf_empty (α := αᵒᵈ) _ - -@[norm_cast] -theorem WithBot.coe_iSup [Nonempty ι] [SupSet α] {f : ι → α} (hf : BddAbove (range f)) : - ↑(⨆ i, f i) = (⨆ i, f i : WithBot α) := - WithTop.coe_iInf (α := αᵒᵈ) hf - theorem WithBot.coe_biSup {ι : Type*} {s : Set ι} (hs : s.Nonempty) {α : Type*} [CompleteLattice α] (f : ι → α) : ⨆ i ∈ s, f i = ⨆ i ∈ s, (f i : WithBot α) := by @@ -69,11 +60,6 @@ theorem WithBot.coe_biSup {ι : Type*} {s : Set ι} (hs : s.Nonempty) · simpa only [iSup_pos h] using by apply le_biSup _ h · simpa only [iSup_neg h] using le_trans (by simp) (le_biSup _ hj) -@[norm_cast] -theorem WithBot.coe_iInf [InfSet α] (f : ι → α) (h : BddBelow (Set.range f)) : - ↑(⨅ i, f i) = (⨅ i, f i : WithBot α) := - WithTop.coe_iSup (α := αᵒᵈ) _ h - theorem WithBot.coe_biInf {ι : Type*} {s : Set ι} {α : Type*} [CompleteLattice α] (f : ι → α) : ⨅ i ∈ s, f i = ⨅ i ∈ s, (f i : WithBot α) := by refine le_antisymm (by simpa using fun _ ↦ biInf_le _) <| @@ -88,65 +74,56 @@ section ConditionallyCompleteLattice variable [ConditionallyCompleteLattice α] {a b : α} +@[to_dual] theorem isLUB_ciSup [Nonempty ι] {f : ι → α} (H : BddAbove (range f)) : IsLUB (range f) (⨆ i, f i) := isLUB_csSup (range_nonempty f) H +@[to_dual] theorem isLUB_ciSup_set {f : β → α} {s : Set β} (H : BddAbove (f '' s)) (Hne : s.Nonempty) : IsLUB (f '' s) (⨆ i : s, f i) := by rw [← sSup_image'] exact isLUB_csSup (Hne.image _) H -theorem isGLB_ciInf [Nonempty ι] {f : ι → α} (H : BddBelow (range f)) : - IsGLB (range f) (⨅ i, f i) := - isGLB_csInf (range_nonempty f) H - -theorem isGLB_ciInf_set {f : β → α} {s : Set β} (H : BddBelow (f '' s)) (Hne : s.Nonempty) : - IsGLB (f '' s) (⨅ i : s, f i) := - isLUB_ciSup_set (α := αᵒᵈ) H Hne - +@[to_dual le_ciInf_iff] theorem ciSup_le_iff [Nonempty ι] {f : ι → α} {a : α} (hf : BddAbove (range f)) : iSup f ≤ a ↔ ∀ i, f i ≤ a := (isLUB_le_iff <| isLUB_ciSup hf).trans forall_mem_range -theorem le_ciInf_iff [Nonempty ι] {f : ι → α} {a : α} (hf : BddBelow (range f)) : - a ≤ iInf f ↔ ∀ i, a ≤ f i := - (le_isGLB_iff <| isGLB_ciInf hf).trans forall_mem_range - +@[to_dual le_ciInf_set_iff] theorem ciSup_set_le_iff {ι : Type*} {s : Set ι} {f : ι → α} {a : α} (hs : s.Nonempty) (hf : BddAbove (f '' s)) : ⨆ i : s, f i ≤ a ↔ ∀ i ∈ s, f i ≤ a := (isLUB_le_iff <| isLUB_ciSup_set hf hs).trans forall_mem_image -theorem le_ciInf_set_iff {ι : Type*} {s : Set ι} {f : ι → α} {a : α} (hs : s.Nonempty) - (hf : BddBelow (f '' s)) : (a ≤ ⨅ i : s, f i) ↔ ∀ i ∈ s, a ≤ f i := - (le_isGLB_iff <| isGLB_ciInf_set hf hs).trans forall_mem_image - +@[to_dual] theorem IsLUB.ciSup_eq [Nonempty ι] {f : ι → α} (H : IsLUB (range f) a) : ⨆ i, f i = a := H.csSup_eq (range_nonempty f) +@[to_dual] theorem IsLUB.ciSup_set_eq {s : Set β} {f : β → α} (H : IsLUB (f '' s) a) (Hne : s.Nonempty) : ⨆ i : s, f i = a := IsLUB.csSup_eq (image_eq_range f s ▸ H) (image_eq_range f s ▸ Hne.image f) -theorem IsGLB.ciInf_eq [Nonempty ι] {f : ι → α} (H : IsGLB (range f) a) : ⨅ i, f i = a := - H.csInf_eq (range_nonempty f) - -theorem IsGLB.ciInf_set_eq {s : Set β} {f : β → α} (H : IsGLB (f '' s) a) (Hne : s.Nonempty) : - ⨅ i : s, f i = a := - IsGLB.csInf_eq (image_eq_range f s ▸ H) (image_eq_range f s ▸ Hne.image f) - -/-- The indexed supremum of a function is bounded above by a uniform bound -/ +/-- The indexed supremum of a function is bounded above by a uniform bound. -/ +@[to_dual le_ciInf /-- The indexed minimum of a function is bounded below by a uniform lower +bound. -/] theorem ciSup_le [Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, f x ≤ c) : iSup f ≤ c := csSup_le (range_nonempty f) (by rwa [forall_mem_range]) /-- The indexed supremum of a function is bounded below by the value taken at one point -/ +@[to_dual ciInf_le /-- The indexed infimum of a function is bounded above by the value taken +at one point. -/] theorem le_ciSup {f : ι → α} (H : BddAbove (range f)) (c : ι) : f c ≤ iSup f := le_csSup H (mem_range_self _) +@[to_dual ciInf_le_of_le] theorem le_ciSup_of_le {f : ι → α} (H : BddAbove (range f)) (c : ι) (h : a ≤ f c) : a ≤ iSup f := le_trans h (le_ciSup H c) /-- If the set of all `f i j` is bounded above, then so is the set of the supremums of every row -/ +@[to_dual + /-- If the set of all `f i j` is bounded below, then so is the set of the infimums + of every row -/] theorem BddAbove.range_iSup_of_iUnion_range {κ : ι → Sort*} {f : ∀ i, κ i → α} (H : BddAbove <| ⋃ i, range (f i)) : BddAbove <| range fun i ↦ ⨆ j, f i j := by have ⟨a, h⟩ := H @@ -155,19 +132,23 @@ theorem BddAbove.range_iSup_of_iUnion_range {κ : ι → Sort*} {f : ∀ i, κ i · exact iSup_of_empty' (f i) ▸ le_sup_right exact ciSup_le fun j ↦ le_sup_of_le_left <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩ +@[to_dual ciInf₂_le] theorem le_ciSup₂ {κ : ι → Sort*} {f : ∀ i, κ i → α} (H : BddAbove <| ⋃ i, range (f i)) (i : ι) (j : κ i) : f i j ≤ ⨆ (i) (j), f i j := le_ciSup_of_le H.range_iSup_of_iUnion_range i <| le_ciSup (H.mono <| subset_iUnion (range <| f ·) i) j /-- The indexed suprema of two functions are comparable if the functions are pointwise comparable -/ -@[gcongr low] +@[to_dual (attr := gcongr low) +/-- The indexed infimum of two functions are comparable if the functions are pointwise +comparable -/] theorem ciSup_mono {f g : ι → α} (B : BddAbove (range g)) (H : ∀ x, f x ≤ g x) : iSup f ≤ iSup g := by cases isEmpty_or_nonempty ι · rw [iSup_of_empty', iSup_of_empty'] · exact ciSup_le fun x => le_ciSup_of_le B x (H x) +@[to_dual] theorem ciSup_sup_eq {f g : ι → α} (Hf : BddAbove <| range f) (Hg : BddAbove <| range g) : ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ (⨆ x, g x) := by cases isEmpty_or_nonempty ι @@ -176,60 +157,21 @@ theorem ciSup_sup_eq {f g : ι → α} (Hf : BddAbove <| range f) (Hg : BddAbove have := bbdAbove_range_sup Hf Hg exact sup_le (ciSup_mono this fun _ ↦ le_sup_left) (ciSup_mono this fun _ ↦ le_sup_right) +@[to_dual ciInf_set_le] theorem le_ciSup_set {f : β → α} {s : Set β} (H : BddAbove (f '' s)) {c : β} (hc : c ∈ s) : f c ≤ ⨆ i : s, f i := (le_csSup H <| mem_image_of_mem f hc).trans_eq sSup_image' -/-- The indexed infimum of two functions are comparable if the functions are pointwise comparable -/ -@[gcongr low] -theorem ciInf_mono {f g : ι → α} (B : BddBelow (range f)) (H : ∀ x, f x ≤ g x) : iInf f ≤ iInf g := - ciSup_mono (α := αᵒᵈ) B H - -theorem ciInf_inf_eq {f g : ι → α} (Hf : BddBelow <| range f) (Hg : BddBelow <| range g) : - ⨅ x, f x ⊓ g x = (⨅ x, f x) ⊓ (⨅ x, g x) := - ciSup_sup_eq (α := αᵒᵈ) Hf Hg - -/-- The indexed minimum of a function is bounded below by a uniform lower bound -/ -theorem le_ciInf [Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, c ≤ f x) : c ≤ iInf f := - ciSup_le (α := αᵒᵈ) H - -/-- The indexed infimum of a function is bounded above by the value taken at one point -/ -theorem ciInf_le {f : ι → α} (H : BddBelow (range f)) (c : ι) : iInf f ≤ f c := - le_ciSup (α := αᵒᵈ) H c - -theorem ciInf_le_of_le {f : ι → α} (H : BddBelow (range f)) (c : ι) (h : f c ≤ a) : iInf f ≤ a := - le_ciSup_of_le (α := αᵒᵈ) H c h - +@[to_dual] theorem ciSup_mono_of_forall_exists {ι'} [Nonempty ι] {f : ι → α} {g : ι' → α} (hg : BddAbove <| range g) (h : ∀ i, ∃ i', f i ≤ g i') : ⨆ i, f i ≤ ⨆ i', g i' := ciSup_le fun i ↦ h i |>.elim <| le_ciSup_of_le hg -theorem ciInf_mono_of_forall_exists {ι'} [Nonempty ι'] {f : ι → α} {g : ι' → α} - (hf : BddBelow <| range f) (h : ∀ i', ∃ i, f i ≤ g i') : ⨅ i, f i ≤ ⨅ i', g i' := - ciSup_mono_of_forall_exists (α := αᵒᵈ) hf h - -/-- If the set of all `f i j` is bounded below, then so is the set of the infimums of every row -/ -theorem BddBelow.range_iInf_of_iUnion_range {κ : ι → Sort*} {f : ∀ i, κ i → α} - (H : BddBelow <| ⋃ i, range (f i)) : BddBelow <| range fun i ↦ ⨅ j, f i j := by - have ⟨a, h⟩ := H - refine ⟨a ⊓ (sInf ∅), fun x ⟨i, hx⟩ ↦ hx ▸ ?_⟩ - cases isEmpty_or_nonempty <| κ i - · exact iInf_of_isEmpty (f i) ▸ inf_le_right - exact le_ciInf fun j ↦ inf_le_of_left_le <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩ - -theorem ciInf₂_le {κ : ι → Sort*} {f : ∀ i, κ i → α} (H : BddBelow <| ⋃ i, range (f i)) (i : ι) - (j : κ i) : ⨅ (i) (j), f i j ≤ f i j := - ciInf_le_of_le H.range_iInf_of_iUnion_range i <| - ciInf_le (H.mono <| subset_iUnion (range <| f ·) i) j - -theorem ciInf_set_le {f : β → α} {s : Set β} (H : BddBelow (f '' s)) {c : β} (hc : c ∈ s) : - ⨅ i : s, f i ≤ f c := - le_ciSup_set (α := αᵒᵈ) H hc - lemma ciInf_le_ciSup [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) (hf' : BddAbove (range f)) : ⨅ i, f i ≤ ⨆ i, f i := (ciInf_le hf (Classical.arbitrary _)).trans <| le_ciSup hf' (Classical.arbitrary _) +@[to_dual] lemma ciSup_prod {f : β × γ → α} (hf : BddAbove (Set.range f)) : ⨆ p, f p = ⨆ b, ⨆ c, f (b, c) := by rcases isEmpty_or_nonempty β @@ -251,34 +193,25 @@ lemma ciSup_prod {f : β × γ → α} (hf : BddAbove (Set.range f)) : conv_rhs => enter [b]; rw [ciSup_le_iff (h₂ b)] simp [Prod.forall] -lemma ciInf_prod {f : β × γ → α} (hf : BddBelow (Set.range f)) : - ⨅ p, f p = ⨅ b, ⨅ c, f (b, c) := - ciSup_prod (α := αᵒᵈ) hf - /-- Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b` is larger than `f i` for all `i`, and that this is not the case of any `wb`. +See `iInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/] theorem ciSup_eq_of_forall_le_of_forall_lt_exists_gt [Nonempty ι] {f : ι → α} (h₁ : ∀ i, f i ≤ b) (h₂ : ∀ w, w < b → ∃ i, w < f i) : ⨆ i : ι, f i = b := csSup_eq_of_forall_le_of_forall_lt_exists_gt (range_nonempty f) (forall_mem_range.mpr h₁) fun w hw => exists_range_iff.mpr <| h₂ w hw -/-- Introduction rule to prove that `b` is the infimum of `f`: it suffices to check that `b` -is smaller than `f i` for all `i`, and that this is not the case of any `w>b`. -See `iInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/ -theorem ciInf_eq_of_forall_ge_of_forall_gt_exists_lt [Nonempty ι] {f : ι → α} (h₁ : ∀ i, b ≤ f i) - (h₂ : ∀ w, b < w → ∃ i, f i < w) : ⨅ i : ι, f i = b := - ciSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ) h₁ h₂ - +@[to_dual] lemma Set.Iic_ciInf [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) : Iic (⨅ i, f i) = ⋂ i, Iic (f i) := by ext simpa using le_ciInf_iff hf -lemma Set.Ici_ciSup [Nonempty ι] {f : ι → α} (hf : BddAbove (range f)) : - Ici (⨆ i, f i) = ⋂ i, Ici (f i) := - Iic_ciInf (α := αᵒᵈ) hf - +@[to_dual] theorem ciSup_subtype {p : ι → Prop} {f : Subtype p → α} (hf : BddAbove (Set.range f)) (hf' : sSup ∅ ≤ iSup f) : iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩ := by @@ -300,11 +233,7 @@ theorem ciSup_subtype {p : ι → Prop} {f : Subtype p → α} · exact le_ciSup hf ?_ · exact hf' -theorem ciInf_subtype {p : ι → Prop} {f : Subtype p → α} - (hf : BddBelow (Set.range f)) (hf' : iInf f ≤ sInf ∅) : - iInf f = ⨅ (i) (h : p i), f ⟨i, h⟩ := - ciSup_subtype (α := αᵒᵈ) hf hf' - +@[to_dual] theorem cbiSup_eq_ciSup_subtype {p : ι → Prop} {f : ∀ i, p i → α} (hf : BddAbove (Set.range (fun i : Subtype p ↦ f i i.prop))) (hf' : sSup ∅ ≤ ⨆ (i : Subtype p), f i i.prop) : @@ -313,14 +242,9 @@ theorem cbiSup_eq_ciSup_subtype {p : ι → Prop} {f : ∀ i, p i → α} @[deprecated (since := "2026-04-04")] alias ciSup_subtype' := cbiSup_eq_ciSup_subtype -theorem cbiInf_eq_ciInf_subtype {p : ι → Prop} {f : ∀ i, p i → α} - (hf : BddBelow (Set.range (fun i : Subtype p ↦ f i i.prop))) - (hf' : ⨅ (i : Subtype p), f i i.prop ≤ sInf ∅) : - ⨅ (i) (h), f i h = ⨅ x : Subtype p, f x x.property := - (ciInf_subtype (f := fun x => f x.val x.property) hf hf').symm - @[deprecated (since := "2026-04-04")] alias ciInf_subtype' := cbiInf_eq_ciInf_subtype +@[to_dual] theorem ciSup_subtype_fun {ι} {s : Set ι} {f : ι → α} (hf : BddAbove (Set.range fun i : s ↦ f i)) (hf' : sSup ∅ ≤ ⨆ i : s, f i) : ⨆ i : s, f i = ⨆ (t : ι) (_ : t ∈ s), f t := @@ -328,33 +252,21 @@ theorem ciSup_subtype_fun {ι} {s : Set ι} {f : ι → α} @[deprecated (since := "2026-04-04")] alias ciSup_subtype'' := ciSup_subtype_fun -theorem ciInf_subtype_fun {ι} {s : Set ι} {f : ι → α} - (hf : BddBelow (Set.range fun i : s ↦ f i)) (hf' : ⨅ i : s, f i ≤ sInf ∅) : - ⨅ i : s, f i = ⨅ (t : ι) (_ : t ∈ s), f t := - ciInf_subtype hf hf' - @[deprecated (since := "2026-04-04")] alias ciInf_subtype'' := ciInf_subtype_fun +@[to_dual] theorem csSup_image {s : Set β} {f : β → α} (hf : BddAbove (Set.range fun i : s ↦ f i)) (hf' : sSup ∅ ≤ ⨆ i : s, f i) : sSup (f '' s) = ⨆ a ∈ s, f a := by rw [← ciSup_subtype_fun hf hf', iSup, Set.image_eq_range] -theorem csInf_image {s : Set β} {f : β → α} - (hf : BddBelow (Set.range fun i : s ↦ f i)) (hf' : ⨅ i : s, f i ≤ sInf ∅) : - sInf (f '' s) = ⨅ a ∈ s, f a := - csSup_image (α := αᵒᵈ) hf hf' - +@[to_dual] theorem cbiSup_id {s : Set α} (hs : BddAbove s) (h : sSup ∅ ≤ sSup s) : ⨆ i ∈ s, i = sSup s := by rw [← csSup_image (Subtype.range_coe ▸ hs), Set.image_id'] · convert! h rw [← sSup_range, Subtype.range_coe] -theorem cbiInf_id {s : Set α} (hs : BddBelow s) (h : sInf s ≤ sInf ∅) : ⨅ i ∈ s, i = sInf s := by - rw [← csInf_image (Subtype.range_coe ▸ hs), Set.image_id'] - · convert! h - rw [← sInf_range, Subtype.range_coe] - +@[to_dual] lemma ciSup_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α} (hf : BddAbove (Set.range fun i : s ↦ g (f i))) (hg' : sSup ∅ ≤ ⨆ i : s, g (f i)) : ⨆ i ∈ (f '' s), g i = ⨆ x ∈ s, g (f x) := by @@ -375,13 +287,9 @@ lemma ciSup_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α simpa [bddAbove_def] using hf rw [← csSup_image hg hf', ← csSup_image hf hg', ← Set.image_comp, comp_def] -lemma ciInf_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α} - (hf : BddBelow (Set.range fun i : s ↦ g (f i))) (hg' : ⨅ i : s, g (f i) ≤ sInf ∅) : - ⨅ i ∈ (f '' s), g i = ⨅ x ∈ s, g (f x) := - ciSup_image (α := αᵒᵈ) hf hg' - /-- Note that equality need not hold: consider `ι := Bool, p := (·), α := ℤ, f := fun _ ↦ -1`, then the LHS is `-1` but the RHS is `-1 ⊔ sSup ∅ = -1 ⊔ 0 = 0`. -/ +@[to_dual] theorem ciSup_exists_le {p : ι → Prop} {f : Exists p → α} : ⨆ ih, f ih ≤ ⨆ (i) (h), f ⟨i, h⟩ := by by_cases! h : Exists p · have : Nonempty <| Exists p := ⟨h⟩ @@ -391,15 +299,10 @@ theorem ciSup_exists_le {p : ι → Prop} {f : Exists p → α} : ⨆ ih, f ih · cases isEmpty_or_nonempty ι <;> simp [h, iSup_of_empty', ciSup_const] -theorem le_ciInf_exists {p : ι → Prop} {f : Exists p → α} : ⨅ (i) (h), f ⟨i, h⟩ ≤ ⨅ ih, f ih := - ciSup_exists_le (α := αᵒᵈ) - +@[to_dual] theorem ciSup_and {p q : Prop} {f : p ∧ q → α} : ⨆ ih, f ih = ⨆ (h₁) (h₂), f ⟨h₁, h₂⟩ := by by_cases hp : p <;> by_cases hq : q <;> simp [hp, hq, iSup_of_empty'] -theorem ciInf_and {p q : Prop} {f : p ∧ q → α} : ⨅ ih, f ih = ⨅ (h₁) (h₂), f ⟨h₁, h₂⟩ := - ciSup_and (α := αᵒᵈ) - end ConditionallyCompleteLattice section ConditionallyCompleteLinearOrder @@ -421,16 +324,14 @@ theorem ciInf_inf_le {f g : ι → α} : (⨅ x, f x) ⊓ (⨅ x, g x) ≤ ⨅ x /-- Indexed version of `exists_lt_of_lt_csSup`. When `b < iSup f`, there is an element `i` such that `b < f i`. -/ +@[to_dual +/-- Indexed version of `exists_lt_of_csInf_lt`. +When `iInf f < a`, there is an element `i` such that `f i < a`. +-/] theorem exists_lt_of_lt_ciSup [Nonempty ι] {f : ι → α} (h : b < iSup f) : ∃ i, b < f i := let ⟨_, ⟨i, rfl⟩, h⟩ := exists_lt_of_lt_csSup (range_nonempty f) h ⟨i, h⟩ -/-- Indexed version of `exists_lt_of_csInf_lt`. -When `iInf f < a`, there is an element `i` such that `f i < a`. --/ -theorem exists_lt_of_ciInf_lt [Nonempty ι] {f : ι → α} (h : iInf f < a) : ∃ i, f i < a := - exists_lt_of_lt_ciSup (α := αᵒᵈ) h - theorem lt_ciSup_iff [Nonempty ι] {f : ι → α} (hb : BddAbove (range f)) : a < iSup f ↔ ∃ i, a < f i := by simpa only [mem_range, exists_exists_eq_and] using! lt_csSup_iff hb (range_nonempty _) @@ -566,38 +467,26 @@ namespace GaloisConnection variable [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι] {l : α → β} {u : β → α} +@[to_dual u_csInf] theorem l_csSup (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : l (sSup s) = ⨆ x : s, l x := Eq.symm <| IsLUB.ciSup_set_eq (gc.isLUB_l_image <| isLUB_csSup hne hbdd) hne +@[to_dual u_csInf'] theorem l_csSup' (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : l (sSup s) = sSup (l '' s) := by rw [gc.l_csSup hne hbdd, sSup_image'] +@[to_dual u_ciInf] theorem l_ciSup (gc : GaloisConnection l u) {f : ι → α} (hf : BddAbove (range f)) : l (⨆ i, f i) = ⨆ i, l (f i) := by rw [iSup, gc.l_csSup (range_nonempty _) hf, iSup_range'] +@[to_dual u_ciInf_set] theorem l_ciSup_set (gc : GaloisConnection l u) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s)) (hne : s.Nonempty) : l (⨆ i : s, f i) = ⨆ i : s, l (f i) := by haveI := hne.to_subtype rw [image_eq_range] at hf exact gc.l_ciSup hf -theorem u_csInf (gc : GaloisConnection l u) {s : Set β} (hne : s.Nonempty) (hbdd : BddBelow s) : - u (sInf s) = ⨅ x : s, u x := - gc.dual.l_csSup hne hbdd - -theorem u_csInf' (gc : GaloisConnection l u) {s : Set β} (hne : s.Nonempty) (hbdd : BddBelow s) : - u (sInf s) = sInf (u '' s) := - gc.dual.l_csSup' hne hbdd - -theorem u_ciInf (gc : GaloisConnection l u) {f : ι → β} (hf : BddBelow (range f)) : - u (⨅ i, f i) = ⨅ i, u (f i) := - gc.dual.l_ciSup hf - -theorem u_ciInf_set (gc : GaloisConnection l u) {s : Set γ} {f : γ → β} (hf : BddBelow (f '' s)) - (hne : s.Nonempty) : u (⨅ i : s, f i) = ⨅ i : s, u (f i) := - gc.dual.l_ciSup_set hf hne - end GaloisConnection namespace OrderIso @@ -605,38 +494,26 @@ namespace OrderIso section ConditionallyCompleteLattice variable [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι] +@[to_dual] theorem map_csSup (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : e (sSup s) = ⨆ x : s, e x := e.to_galoisConnection.l_csSup hne hbdd +@[to_dual] theorem map_csSup' (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : e (sSup s) = sSup (e '' s) := e.to_galoisConnection.l_csSup' hne hbdd +@[to_dual] theorem map_ciSup (e : α ≃o β) {f : ι → α} (hf : BddAbove (range f)) : e (⨆ i, f i) = ⨆ i, e (f i) := e.to_galoisConnection.l_ciSup hf +@[to_dual] theorem map_ciSup_set (e : α ≃o β) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s)) (hne : s.Nonempty) : e (⨆ i : s, f i) = ⨆ i : s, e (f i) := e.to_galoisConnection.l_ciSup_set hf hne -theorem map_csInf (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) : - e (sInf s) = ⨅ x : s, e x := - e.dual.map_csSup hne hbdd - -theorem map_csInf' (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) : - e (sInf s) = sInf (e '' s) := - e.dual.map_csSup' hne hbdd - -theorem map_ciInf (e : α ≃o β) {f : ι → α} (hf : BddBelow (range f)) : - e (⨅ i, f i) = ⨅ i, e (f i) := - e.dual.map_ciSup hf - -theorem map_ciInf_set (e : α ≃o β) {s : Set γ} {f : γ → α} (hf : BddBelow (f '' s)) - (hne : s.Nonempty) : e (⨅ i : s, f i) = ⨅ i : s, e (f i) := - e.dual.map_ciSup_set hf hne - end ConditionallyCompleteLattice section ConditionallyCompleteLinearOrderBot From 48e6e57aac375c42afb73d83e0007a4440dbd1d8 Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sat, 13 Jun 2026 11:36:48 -0700 Subject: [PATCH 15/24] Add finset supremum convergence lemmas --- .../Topology/Order/MonotoneConvergence.lean | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/Mathlib/Topology/Order/MonotoneConvergence.lean b/Mathlib/Topology/Order/MonotoneConvergence.lean index 525b8006cece8f..2ce07750fb97c4 100644 --- a/Mathlib/Topology/Order/MonotoneConvergence.lean +++ b/Mathlib/Topology/Order/MonotoneConvergence.lean @@ -5,6 +5,7 @@ Authors: Heather Macbeth, Yury Kudryashov -/ module +public import Mathlib.Order.CompleteLattice.Finset public import Mathlib.Topology.Order.Basic /-! @@ -164,6 +165,35 @@ end iInf end +section FinsetSup + +variable {ι α : Type*} [TopologicalSpace α] + +theorem tendsto_finset_sup_iSup [CompleteLattice α] [SupConvergenceClass α] (a : ι → α) : + Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by + have hmono : Monotone (fun F : Finset ι => F.sup a) := + fun F G hFG => Finset.sup_mono hFG + simpa [Finset.sup_eq_iSup, ← iSup_eq_iSup_finset a] using tendsto_atTop_iSup hmono + +theorem tendsto_finset_sup_ciSup [ConditionallyCompleteLattice α] [OrderBot α] + [SupConvergenceClass α] [Nonempty ι] (a : ι → α) (ha : BddAbove (Set.range a)) : + Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by + have hmono : Monotone (fun F : Finset ι => F.sup a) := + fun F G hFG => Finset.sup_mono hFG + have hbdd : BddAbove (Set.range fun F : Finset ι => F.sup a) := by + refine ⟨⨆ i, a i, ?_⟩ + rintro _ ⟨F, rfl⟩ + exact Finset.sup_le fun i _ => le_ciSup ha i + have hsup : (⨆ F : Finset ι, F.sup a) = ⨆ i, a i := by + refine le_antisymm ?_ ?_ + · exact ciSup_le fun F => Finset.sup_le fun i _ => le_ciSup ha i + · exact ciSup_le fun i => + (Finset.le_sup (s := ({i} : Finset ι)) (f := a) (by simp)).trans + (le_ciSup hbdd ({i} : Finset ι)) + simpa [hsup] using tendsto_atTop_ciSup hmono hbdd + +end FinsetSup + instance Prod.supConvergenceClass [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [SupConvergenceClass α] [SupConvergenceClass β] : SupConvergenceClass (α × β) := by From 87213eeb1cd68058e298f6fb7797dedcb415d69a Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sat, 13 Jun 2026 13:19:48 -0700 Subject: [PATCH 16/24] Add finset infimum convergence lemmas --- .../Topology/Order/MonotoneConvergence.lean | 27 +++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Order/MonotoneConvergence.lean b/Mathlib/Topology/Order/MonotoneConvergence.lean index 2ce07750fb97c4..9ff4b140a8158d 100644 --- a/Mathlib/Topology/Order/MonotoneConvergence.lean +++ b/Mathlib/Topology/Order/MonotoneConvergence.lean @@ -165,7 +165,7 @@ end iInf end -section FinsetSup +section FinsetSupInf variable {ι α : Type*} [TopologicalSpace α] @@ -192,7 +192,30 @@ theorem tendsto_finset_sup_ciSup [ConditionallyCompleteLattice α] [OrderBot α] (le_ciSup hbdd ({i} : Finset ι)) simpa [hsup] using tendsto_atTop_ciSup hmono hbdd -end FinsetSup +theorem tendsto_finset_inf_iInf [CompleteLattice α] [InfConvergenceClass α] (a : ι → α) : + Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := by + have hanti : Antitone (fun F : Finset ι => F.inf a) := + fun F G hFG => Finset.inf_mono hFG + simpa [Finset.inf_eq_iInf, ← iInf_eq_iInf_finset a] using tendsto_atTop_iInf hanti + +theorem tendsto_finset_inf_ciInf [ConditionallyCompleteLattice α] [OrderTop α] + [InfConvergenceClass α] [Nonempty ι] (a : ι → α) (ha : BddBelow (Set.range a)) : + Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := by + have hanti : Antitone (fun F : Finset ι => F.inf a) := + fun F G hFG => Finset.inf_mono hFG + have hbdd : BddBelow (Set.range fun F : Finset ι => F.inf a) := by + refine ⟨⨅ i, a i, ?_⟩ + rintro _ ⟨F, rfl⟩ + exact Finset.le_inf fun i _ => ciInf_le ha i + have hinf : (⨅ F : Finset ι, F.inf a) = ⨅ i, a i := by + refine le_antisymm ?_ ?_ + · exact le_ciInf fun i => + (ciInf_le hbdd ({i} : Finset ι)).trans + (Finset.inf_le (s := ({i} : Finset ι)) (f := a) (by simp)) + · exact le_ciInf fun F => Finset.le_inf fun i _ => ciInf_le ha i + simpa [hinf] using tendsto_atTop_ciInf hanti hbdd + +end FinsetSupInf instance Prod.supConvergenceClass [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] From d3d402c26130abdf5d079a2a41b02c2cd3637056 Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sat, 13 Jun 2026 14:08:18 -0700 Subject: [PATCH 17/24] Rework finset convergence lemmas via ciSup --- .../Topology/Order/MonotoneConvergence.lean | 79 +++++++++++-------- 1 file changed, 48 insertions(+), 31 deletions(-) diff --git a/Mathlib/Topology/Order/MonotoneConvergence.lean b/Mathlib/Topology/Order/MonotoneConvergence.lean index 9ff4b140a8158d..205cb16c796ca6 100644 --- a/Mathlib/Topology/Order/MonotoneConvergence.lean +++ b/Mathlib/Topology/Order/MonotoneConvergence.lean @@ -5,7 +5,6 @@ Authors: Heather Macbeth, Yury Kudryashov -/ module -public import Mathlib.Order.CompleteLattice.Finset public import Mathlib.Topology.Order.Basic /-! @@ -167,53 +166,71 @@ end section FinsetSupInf -variable {ι α : Type*} [TopologicalSpace α] +variable {ι α : Type*} -theorem tendsto_finset_sup_iSup [CompleteLattice α] [SupConvergenceClass α] (a : ι → α) : - Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by - have hmono : Monotone (fun F : Finset ι => F.sup a) := - fun F G hFG => Finset.sup_mono hFG - simpa [Finset.sup_eq_iSup, ← iSup_eq_iSup_finset a] using tendsto_atTop_iSup hmono +theorem ciSup_eq_ciSup_finset [ConditionallyCompleteLattice α] [OrderBot α] [Nonempty ι] + (a : ι → α) (ha : BddAbove (Set.range a)) : + ⨆ i, a i = ⨆ F : Finset ι, F.sup a := by + have hbdd : BddAbove (Set.range fun F : Finset ι => F.sup a) := by + refine ⟨⨆ i, a i, ?_⟩ + rintro _ ⟨F, rfl⟩ + exact Finset.sup_le fun i _ => le_ciSup ha i + refine le_antisymm ?_ ?_ + · exact ciSup_le fun i => + (Finset.le_sup (s := ({i} : Finset ι)) (f := a) (by simp)).trans + (le_ciSup hbdd ({i} : Finset ι)) + · exact ciSup_le fun F => Finset.sup_le fun i _ => le_ciSup ha i + +theorem ciInf_eq_ciInf_finset [ConditionallyCompleteLattice α] [OrderTop α] [Nonempty ι] + (a : ι → α) (ha : BddBelow (Set.range a)) : + ⨅ i, a i = ⨅ F : Finset ι, F.inf a := by + have hbdd : BddBelow (Set.range fun F : Finset ι => F.inf a) := by + refine ⟨⨅ i, a i, ?_⟩ + rintro _ ⟨F, rfl⟩ + exact Finset.le_inf fun i _ => ciInf_le ha i + refine le_antisymm ?_ ?_ + · exact le_ciInf fun F => Finset.le_inf fun i _ => ciInf_le ha i + · exact le_ciInf fun i => + (ciInf_le hbdd ({i} : Finset ι)).trans + (Finset.inf_le (s := ({i} : Finset ι)) (f := a) (by simp)) + +variable [TopologicalSpace α] theorem tendsto_finset_sup_ciSup [ConditionallyCompleteLattice α] [OrderBot α] [SupConvergenceClass α] [Nonempty ι] (a : ι → α) (ha : BddAbove (Set.range a)) : Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by - have hmono : Monotone (fun F : Finset ι => F.sup a) := - fun F G hFG => Finset.sup_mono hFG + have hmono : Monotone (fun F : Finset ι => F.sup a) := fun F G hFG => Finset.sup_mono hFG have hbdd : BddAbove (Set.range fun F : Finset ι => F.sup a) := by refine ⟨⨆ i, a i, ?_⟩ rintro _ ⟨F, rfl⟩ exact Finset.sup_le fun i _ => le_ciSup ha i - have hsup : (⨆ F : Finset ι, F.sup a) = ⨆ i, a i := by - refine le_antisymm ?_ ?_ - · exact ciSup_le fun F => Finset.sup_le fun i _ => le_ciSup ha i - · exact ciSup_le fun i => - (Finset.le_sup (s := ({i} : Finset ι)) (f := a) (by simp)).trans - (le_ciSup hbdd ({i} : Finset ι)) - simpa [hsup] using tendsto_atTop_ciSup hmono hbdd - -theorem tendsto_finset_inf_iInf [CompleteLattice α] [InfConvergenceClass α] (a : ι → α) : - Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := by - have hanti : Antitone (fun F : Finset ι => F.inf a) := - fun F G hFG => Finset.inf_mono hFG - simpa [Finset.inf_eq_iInf, ← iInf_eq_iInf_finset a] using tendsto_atTop_iInf hanti + simpa [ciSup_eq_ciSup_finset a ha] using tendsto_atTop_ciSup hmono hbdd theorem tendsto_finset_inf_ciInf [ConditionallyCompleteLattice α] [OrderTop α] [InfConvergenceClass α] [Nonempty ι] (a : ι → α) (ha : BddBelow (Set.range a)) : Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := by - have hanti : Antitone (fun F : Finset ι => F.inf a) := - fun F G hFG => Finset.inf_mono hFG + have hanti : Antitone (fun F : Finset ι => F.inf a) := fun F G hFG => Finset.inf_mono hFG have hbdd : BddBelow (Set.range fun F : Finset ι => F.inf a) := by refine ⟨⨅ i, a i, ?_⟩ rintro _ ⟨F, rfl⟩ exact Finset.le_inf fun i _ => ciInf_le ha i - have hinf : (⨅ F : Finset ι, F.inf a) = ⨅ i, a i := by - refine le_antisymm ?_ ?_ - · exact le_ciInf fun i => - (ciInf_le hbdd ({i} : Finset ι)).trans - (Finset.inf_le (s := ({i} : Finset ι)) (f := a) (by simp)) - · exact le_ciInf fun F => Finset.le_inf fun i _ => ciInf_le ha i - simpa [hinf] using tendsto_atTop_ciInf hanti hbdd + simpa [ciInf_eq_ciInf_finset a ha] using tendsto_atTop_ciInf hanti hbdd + +theorem tendsto_finset_sup_iSup [CompleteLattice α] [SupConvergenceClass α] (a : ι → α) : + Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by + cases isEmpty_or_nonempty ι + · haveI := ‹IsEmpty ι› + simpa [iSup_of_empty] using + (tendsto_const_nhds : Tendsto (fun _ : Finset ι => (⊥ : α)) atTop (𝓝 ⊥)) + · exact tendsto_finset_sup_ciSup a (OrderTop.bddAbove _) + +theorem tendsto_finset_inf_iInf [CompleteLattice α] [InfConvergenceClass α] (a : ι → α) : + Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := by + cases isEmpty_or_nonempty ι + · haveI := ‹IsEmpty ι› + simpa [iInf_of_empty] using + (tendsto_const_nhds : Tendsto (fun _ : Finset ι => (⊤ : α)) atTop (𝓝 ⊤)) + · exact tendsto_finset_inf_ciInf a (OrderBot.bddBelow _) end FinsetSupInf From b5e47b3543f7244d6f63b0c0f7d5e75f9c2e8f76 Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sat, 13 Jun 2026 14:40:03 -0700 Subject: [PATCH 18/24] Use order dual for finset infimum lemmas --- .../Topology/Order/MonotoneConvergence.lean | 26 ++++--------------- 1 file changed, 5 insertions(+), 21 deletions(-) diff --git a/Mathlib/Topology/Order/MonotoneConvergence.lean b/Mathlib/Topology/Order/MonotoneConvergence.lean index 205cb16c796ca6..f31ea28c1053d7 100644 --- a/Mathlib/Topology/Order/MonotoneConvergence.lean +++ b/Mathlib/Topology/Order/MonotoneConvergence.lean @@ -184,15 +184,8 @@ theorem ciSup_eq_ciSup_finset [ConditionallyCompleteLattice α] [OrderBot α] [N theorem ciInf_eq_ciInf_finset [ConditionallyCompleteLattice α] [OrderTop α] [Nonempty ι] (a : ι → α) (ha : BddBelow (Set.range a)) : ⨅ i, a i = ⨅ F : Finset ι, F.inf a := by - have hbdd : BddBelow (Set.range fun F : Finset ι => F.inf a) := by - refine ⟨⨅ i, a i, ?_⟩ - rintro _ ⟨F, rfl⟩ - exact Finset.le_inf fun i _ => ciInf_le ha i - refine le_antisymm ?_ ?_ - · exact le_ciInf fun F => Finset.le_inf fun i _ => ciInf_le ha i - · exact le_ciInf fun i => - (ciInf_le hbdd ({i} : Finset ι)).trans - (Finset.inf_le (s := ({i} : Finset ι)) (f := a) (by simp)) + rw [← OrderDual.toDual_inj] + simpa using ciSup_eq_ciSup_finset (α := αᵒᵈ) (OrderDual.toDual ∘ a) ha variable [TopologicalSpace α] @@ -209,27 +202,18 @@ theorem tendsto_finset_sup_ciSup [ConditionallyCompleteLattice α] [OrderBot α] theorem tendsto_finset_inf_ciInf [ConditionallyCompleteLattice α] [OrderTop α] [InfConvergenceClass α] [Nonempty ι] (a : ι → α) (ha : BddBelow (Set.range a)) : Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := by - have hanti : Antitone (fun F : Finset ι => F.inf a) := fun F G hFG => Finset.inf_mono hFG - have hbdd : BddBelow (Set.range fun F : Finset ι => F.inf a) := by - refine ⟨⨅ i, a i, ?_⟩ - rintro _ ⟨F, rfl⟩ - exact Finset.le_inf fun i _ => ciInf_le ha i - simpa [ciInf_eq_ciInf_finset a ha] using tendsto_atTop_ciInf hanti hbdd + convert! tendsto_finset_sup_ciSup (α := αᵒᵈ) (OrderDual.toDual ∘ a) ha using 1 theorem tendsto_finset_sup_iSup [CompleteLattice α] [SupConvergenceClass α] (a : ι → α) : Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by cases isEmpty_or_nonempty ι - · haveI := ‹IsEmpty ι› - simpa [iSup_of_empty] using - (tendsto_const_nhds : Tendsto (fun _ : Finset ι => (⊥ : α)) atTop (𝓝 ⊥)) + · simp_all [iSup_of_empty, tendsto_const_nhds] · exact tendsto_finset_sup_ciSup a (OrderTop.bddAbove _) theorem tendsto_finset_inf_iInf [CompleteLattice α] [InfConvergenceClass α] (a : ι → α) : Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := by cases isEmpty_or_nonempty ι - · haveI := ‹IsEmpty ι› - simpa [iInf_of_empty] using - (tendsto_const_nhds : Tendsto (fun _ : Finset ι => (⊤ : α)) atTop (𝓝 ⊤)) + · simp_all [iInf_of_empty, tendsto_const_nhds] · exact tendsto_finset_inf_ciInf a (OrderBot.bddBelow _) end FinsetSupInf From fd840e603783c4a1b999647b1ffb21828a4c9d4f Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sat, 13 Jun 2026 20:03:17 -0700 Subject: [PATCH 19/24] Use to_dual for finset supremum identity --- .../ConditionallyCompleteLattice/Finset.lean | 20 ++++++++++ .../Topology/Order/MonotoneConvergence.lean | 39 +++++-------------- 2 files changed, 29 insertions(+), 30 deletions(-) diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean index c6f70a19799255..a3e806afade5b3 100644 --- a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean +++ b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean @@ -179,6 +179,26 @@ end ListMultiset end ConditionallyCompleteLinearOrder +section ConditionallyCompleteLattice + +variable [ConditionallyCompleteLattice α] + +/-- Supremum of `a i`, `i : ι`, is equal to the supremum over finite suprema of `a`. -/ +@[to_dual +/-- Infimum of `a i`, `i : ι`, is equal to the infimum over finite infima of `a`. -/] +theorem ciSup_eq_ciSup_finset [OrderBot α] [Nonempty ι] {a : ι → α} + (ha : BddAbove (range a)) : + ⨆ i, a i = ⨆ F : Finset ι, F.sup a := by + have hbdd : BddAbove (Set.range fun F : Finset ι => F.sup a) := by + refine ⟨⨆ i, a i, ?_⟩ + rintro _ ⟨F, rfl⟩ + exact Finset.sup_le fun i _ => le_ciSup ha i + refine le_antisymm ?_ ?_ + · exact ciSup_le fun i => (Finset.le_sup (by simp)).trans (le_ciSup hbdd ({i} : Finset ι)) + · exact ciSup_le fun F => Finset.sup_le fun i _ => le_ciSup ha i + +end ConditionallyCompleteLattice + /-! ### Relation between `sSup` / `sInf` and `Finset.sup'` / `Finset.inf'` diff --git a/Mathlib/Topology/Order/MonotoneConvergence.lean b/Mathlib/Topology/Order/MonotoneConvergence.lean index f31ea28c1053d7..29b617cf3fac2f 100644 --- a/Mathlib/Topology/Order/MonotoneConvergence.lean +++ b/Mathlib/Topology/Order/MonotoneConvergence.lean @@ -168,53 +168,32 @@ section FinsetSupInf variable {ι α : Type*} -theorem ciSup_eq_ciSup_finset [ConditionallyCompleteLattice α] [OrderBot α] [Nonempty ι] - (a : ι → α) (ha : BddAbove (Set.range a)) : - ⨆ i, a i = ⨆ F : Finset ι, F.sup a := by - have hbdd : BddAbove (Set.range fun F : Finset ι => F.sup a) := by - refine ⟨⨆ i, a i, ?_⟩ - rintro _ ⟨F, rfl⟩ - exact Finset.sup_le fun i _ => le_ciSup ha i - refine le_antisymm ?_ ?_ - · exact ciSup_le fun i => - (Finset.le_sup (s := ({i} : Finset ι)) (f := a) (by simp)).trans - (le_ciSup hbdd ({i} : Finset ι)) - · exact ciSup_le fun F => Finset.sup_le fun i _ => le_ciSup ha i - -theorem ciInf_eq_ciInf_finset [ConditionallyCompleteLattice α] [OrderTop α] [Nonempty ι] - (a : ι → α) (ha : BddBelow (Set.range a)) : - ⨅ i, a i = ⨅ F : Finset ι, F.inf a := by - rw [← OrderDual.toDual_inj] - simpa using ciSup_eq_ciSup_finset (α := αᵒᵈ) (OrderDual.toDual ∘ a) ha - variable [TopologicalSpace α] theorem tendsto_finset_sup_ciSup [ConditionallyCompleteLattice α] [OrderBot α] - [SupConvergenceClass α] [Nonempty ι] (a : ι → α) (ha : BddAbove (Set.range a)) : + [SupConvergenceClass α] [Nonempty ι] {a : ι → α} (ha : BddAbove (range a)) : Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by have hmono : Monotone (fun F : Finset ι => F.sup a) := fun F G hFG => Finset.sup_mono hFG have hbdd : BddAbove (Set.range fun F : Finset ι => F.sup a) := by refine ⟨⨆ i, a i, ?_⟩ rintro _ ⟨F, rfl⟩ exact Finset.sup_le fun i _ => le_ciSup ha i - simpa [ciSup_eq_ciSup_finset a ha] using tendsto_atTop_ciSup hmono hbdd + simpa [ciSup_eq_ciSup_finset ha] using tendsto_atTop_ciSup hmono hbdd theorem tendsto_finset_inf_ciInf [ConditionallyCompleteLattice α] [OrderTop α] - [InfConvergenceClass α] [Nonempty ι] (a : ι → α) (ha : BddBelow (Set.range a)) : - Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := by - convert! tendsto_finset_sup_ciSup (α := αᵒᵈ) (OrderDual.toDual ∘ a) ha using 1 + [InfConvergenceClass α] [Nonempty ι] (a : ι → α) (ha : BddBelow (range a)) : + Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := + tendsto_finset_sup_ciSup (α := αᵒᵈ) ha theorem tendsto_finset_sup_iSup [CompleteLattice α] [SupConvergenceClass α] (a : ι → α) : Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by - cases isEmpty_or_nonempty ι - · simp_all [iSup_of_empty, tendsto_const_nhds] - · exact tendsto_finset_sup_ciSup a (OrderTop.bddAbove _) + have hmono : Monotone (fun F : Finset ι => F.sup a) := fun F G hFG => Finset.sup_mono hFG + simpa [Finset.sup_eq_iSup, ← iSup_eq_iSup_finset a] using tendsto_atTop_iSup hmono theorem tendsto_finset_inf_iInf [CompleteLattice α] [InfConvergenceClass α] (a : ι → α) : Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := by - cases isEmpty_or_nonempty ι - · simp_all [iInf_of_empty, tendsto_const_nhds] - · exact tendsto_finset_inf_ciInf a (OrderBot.bddBelow _) + have hanti : Antitone (fun F : Finset ι => F.inf a) := fun F G hFG => Finset.inf_mono hFG + simpa [Finset.inf_eq_iInf, ← iInf_eq_iInf_finset a] using tendsto_atTop_iInf hanti end FinsetSupInf From 4e6adfdf75c263af0e8d78cfec95c9e64750de6d Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sat, 13 Jun 2026 21:30:00 -0700 Subject: [PATCH 20/24] update MC --- .../Topology/Order/MonotoneConvergence.lean | 73 ++++++++++--------- 1 file changed, 40 insertions(+), 33 deletions(-) diff --git a/Mathlib/Topology/Order/MonotoneConvergence.lean b/Mathlib/Topology/Order/MonotoneConvergence.lean index 29b617cf3fac2f..a2e0766531a8ab 100644 --- a/Mathlib/Topology/Order/MonotoneConvergence.lean +++ b/Mathlib/Topology/Order/MonotoneConvergence.lean @@ -111,6 +111,8 @@ end IsGLB section CiSup +section ConditionallyCompletePartialOrder + variable [ConditionallyCompletePartialOrderSup α] [SupConvergenceClass α] {f : ι → α} theorem tendsto_atTop_ciSup (h_mono : Monotone f) (hbdd : BddAbove <| range f) : @@ -124,10 +126,28 @@ theorem tendsto_atTop_ciSup (h_mono : Monotone f) (hbdd : BddAbove <| range f) : theorem tendsto_atBot_ciSup (h_anti : Antitone f) (hbdd : BddAbove <| range f) : Tendsto f atBot (𝓝 (⨆ i, f i)) := by convert! tendsto_atTop_ciSup h_anti.dual hbdd.dual using 1 +end ConditionallyCompletePartialOrder + +section ConditionallyCompleteLattice + +theorem tendsto_finset_sup_ciSup {ι} [ConditionallyCompleteLattice α] [OrderBot α] + [SupConvergenceClass α] [Nonempty ι] {a : ι → α} (ha : BddAbove (range a)) : + Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by + have hmono : Monotone (fun F : Finset ι => F.sup a) := fun F G hFG => Finset.sup_mono hFG + have hbdd : BddAbove (Set.range fun F : Finset ι => F.sup a) := by + refine ⟨⨆ i, a i, ?_⟩ + rintro _ ⟨F, rfl⟩ + exact Finset.sup_le fun i _ => le_ciSup ha i + simpa [ciSup_eq_ciSup_finset ha] using tendsto_atTop_ciSup hmono hbdd + +end ConditionallyCompleteLattice + end CiSup section CiInf +section ConditionallyCompletePartialOrder + variable [ConditionallyCompletePartialOrderInf α] [InfConvergenceClass α] {f : ι → α} theorem tendsto_atBot_ciInf (h_mono : Monotone f) (hbdd : BddBelow <| range f) : @@ -136,6 +156,17 @@ theorem tendsto_atBot_ciInf (h_mono : Monotone f) (hbdd : BddBelow <| range f) : theorem tendsto_atTop_ciInf (h_anti : Antitone f) (hbdd : BddBelow <| range f) : Tendsto f atTop (𝓝 (⨅ i, f i)) := by convert! tendsto_atBot_ciSup h_anti.dual hbdd.dual using 1 +end ConditionallyCompletePartialOrder + +section ConditionallyCompleteLattice + +theorem tendsto_finset_inf_ciInf {ι} [ConditionallyCompleteLattice α] [OrderTop α] + [InfConvergenceClass α] [Nonempty ι] (a : ι → α) (ha : BddBelow (range a)) : + Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := + tendsto_finset_sup_ciSup (α := αᵒᵈ) ha + +end ConditionallyCompleteLattice + end CiInf section iSup @@ -145,6 +176,11 @@ variable [CompleteLattice α] [SupConvergenceClass α] {f : ι → α} theorem tendsto_atTop_iSup (h_mono : Monotone f) : Tendsto f atTop (𝓝 (⨆ i, f i)) := tendsto_atTop_ciSup h_mono (OrderTop.bddAbove _) +theorem tendsto_finset_sup_iSup {ι} (a : ι → α) : + Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by + have hmono : Monotone (fun F : Finset ι => F.sup a) := fun F G hFG => Finset.sup_mono hFG + simpa [Finset.sup_eq_iSup, ← iSup_eq_iSup_finset a] using tendsto_atTop_iSup hmono + theorem tendsto_atBot_iSup (h_anti : Antitone f) : Tendsto f atBot (𝓝 (⨆ i, f i)) := tendsto_atBot_ciSup h_anti (OrderTop.bddAbove _) @@ -157,6 +193,10 @@ variable [CompleteLattice α] [InfConvergenceClass α] {f : ι → α} theorem tendsto_atBot_iInf (h_mono : Monotone f) : Tendsto f atBot (𝓝 (⨅ i, f i)) := tendsto_atBot_ciInf h_mono (OrderBot.bddBelow _) +theorem tendsto_finset_inf_iInf {ι} (a : ι → α) : + Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := + tendsto_finset_sup_iSup (α := αᵒᵈ) a + theorem tendsto_atTop_iInf (h_anti : Antitone f) : Tendsto f atTop (𝓝 (⨅ i, f i)) := tendsto_atTop_ciInf h_anti (OrderBot.bddBelow _) @@ -164,39 +204,6 @@ end iInf end -section FinsetSupInf - -variable {ι α : Type*} - -variable [TopologicalSpace α] - -theorem tendsto_finset_sup_ciSup [ConditionallyCompleteLattice α] [OrderBot α] - [SupConvergenceClass α] [Nonempty ι] {a : ι → α} (ha : BddAbove (range a)) : - Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by - have hmono : Monotone (fun F : Finset ι => F.sup a) := fun F G hFG => Finset.sup_mono hFG - have hbdd : BddAbove (Set.range fun F : Finset ι => F.sup a) := by - refine ⟨⨆ i, a i, ?_⟩ - rintro _ ⟨F, rfl⟩ - exact Finset.sup_le fun i _ => le_ciSup ha i - simpa [ciSup_eq_ciSup_finset ha] using tendsto_atTop_ciSup hmono hbdd - -theorem tendsto_finset_inf_ciInf [ConditionallyCompleteLattice α] [OrderTop α] - [InfConvergenceClass α] [Nonempty ι] (a : ι → α) (ha : BddBelow (range a)) : - Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := - tendsto_finset_sup_ciSup (α := αᵒᵈ) ha - -theorem tendsto_finset_sup_iSup [CompleteLattice α] [SupConvergenceClass α] (a : ι → α) : - Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by - have hmono : Monotone (fun F : Finset ι => F.sup a) := fun F G hFG => Finset.sup_mono hFG - simpa [Finset.sup_eq_iSup, ← iSup_eq_iSup_finset a] using tendsto_atTop_iSup hmono - -theorem tendsto_finset_inf_iInf [CompleteLattice α] [InfConvergenceClass α] (a : ι → α) : - Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) := by - have hanti : Antitone (fun F : Finset ι => F.inf a) := fun F G hFG => Finset.inf_mono hFG - simpa [Finset.inf_eq_iInf, ← iInf_eq_iInf_finset a] using tendsto_atTop_iInf hanti - -end FinsetSupInf - instance Prod.supConvergenceClass [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [SupConvergenceClass α] [SupConvergenceClass β] : SupConvergenceClass (α × β) := by From 8fa96c90eb6224406164e1882e032b3eb38457ec Mon Sep 17 00:00:00 2001 From: "Yongxi (Aaron) Lin" <97214596+CoolRmal@users.noreply.github.com> Date: Sat, 13 Jun 2026 21:32:09 -0700 Subject: [PATCH 21/24] trivial --- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean index 25fe2ab2403330..2836b4ae6b05aa 100644 --- a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean +++ b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean @@ -198,6 +198,7 @@ theorem ciSup_eq_ciSup_finset [OrderBot α] [Nonempty ι] {a : ι → α} · exact ciSup_le fun F => Finset.sup_le fun i _ => le_ciSup ha i end ConditionallyCompleteLattice + section CompleteLinearOrder variable {α : Type*} [CompleteLinearOrder α] {ι : Sort*} From 63d139d1c3ec90874fdcc14e7b0a261324cca0c1 Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sat, 13 Jun 2026 21:33:45 -0700 Subject: [PATCH 22/24] move section --- .../ConditionallyCompleteLattice/Finset.lean | 40 +++++++++---------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean index 2836b4ae6b05aa..525824db98d3d9 100644 --- a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean +++ b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean @@ -21,6 +21,26 @@ open Set variable {ι α β γ : Type*} +section ConditionallyCompleteLattice + +variable [ConditionallyCompleteLattice α] + +/-- Supremum of `a i`, `i : ι`, is equal to the supremum over finite suprema of `a`. -/ +@[to_dual +/-- Infimum of `a i`, `i : ι`, is equal to the infimum over finite infima of `a`. -/] +theorem ciSup_eq_ciSup_finset [OrderBot α] [Nonempty ι] {a : ι → α} + (ha : BddAbove (range a)) : + ⨆ i, a i = ⨆ F : Finset ι, F.sup a := by + have hbdd : BddAbove (Set.range fun F : Finset ι => F.sup a) := by + refine ⟨⨆ i, a i, ?_⟩ + rintro _ ⟨F, rfl⟩ + exact Finset.sup_le fun i _ => le_ciSup ha i + refine le_antisymm ?_ ?_ + · exact ciSup_le fun i => (Finset.le_sup (by simp)).trans (le_ciSup hbdd ({i} : Finset ι)) + · exact ciSup_le fun F => Finset.sup_le fun i _ => le_ciSup ha i + +end ConditionallyCompleteLattice + section ConditionallyCompleteLinearOrder variable [ConditionallyCompleteLinearOrder α] {s t : Set α} {a b : α} @@ -179,26 +199,6 @@ end ListMultiset end ConditionallyCompleteLinearOrder -section ConditionallyCompleteLattice - -variable [ConditionallyCompleteLattice α] - -/-- Supremum of `a i`, `i : ι`, is equal to the supremum over finite suprema of `a`. -/ -@[to_dual -/-- Infimum of `a i`, `i : ι`, is equal to the infimum over finite infima of `a`. -/] -theorem ciSup_eq_ciSup_finset [OrderBot α] [Nonempty ι] {a : ι → α} - (ha : BddAbove (range a)) : - ⨆ i, a i = ⨆ F : Finset ι, F.sup a := by - have hbdd : BddAbove (Set.range fun F : Finset ι => F.sup a) := by - refine ⟨⨆ i, a i, ?_⟩ - rintro _ ⟨F, rfl⟩ - exact Finset.sup_le fun i _ => le_ciSup ha i - refine le_antisymm ?_ ?_ - · exact ciSup_le fun i => (Finset.le_sup (by simp)).trans (le_ciSup hbdd ({i} : Finset ι)) - · exact ciSup_le fun F => Finset.sup_le fun i _ => le_ciSup ha i - -end ConditionallyCompleteLattice - section CompleteLinearOrder variable {α : Type*} [CompleteLinearOrder α] {ι : Sort*} From bf6f8bccc9ace85e38711a2cc0a10021b27c71dd Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sat, 13 Jun 2026 21:34:11 -0700 Subject: [PATCH 23/24] trivial --- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean index 525824db98d3d9..7d6f6da9bbd401 100644 --- a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean +++ b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean @@ -36,7 +36,7 @@ theorem ciSup_eq_ciSup_finset [OrderBot α] [Nonempty ι] {a : ι → α} rintro _ ⟨F, rfl⟩ exact Finset.sup_le fun i _ => le_ciSup ha i refine le_antisymm ?_ ?_ - · exact ciSup_le fun i => (Finset.le_sup (by simp)).trans (le_ciSup hbdd ({i} : Finset ι)) + · exact ciSup_le fun i => (Finset.le_sup (by simp)).trans (le_ciSup hbdd {i}) · exact ciSup_le fun F => Finset.sup_le fun i _ => le_ciSup ha i end ConditionallyCompleteLattice From 76021236640b1d116a5d6007245ef520601e502a Mon Sep 17 00:00:00 2001 From: Yongxi Lin Date: Sat, 13 Jun 2026 21:58:22 -0700 Subject: [PATCH 24/24] Fix generated ciInf theorem name --- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean index 558f50fc38df58..217a256864676b 100644 --- a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean +++ b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean @@ -324,7 +324,7 @@ theorem ciInf_inf_le {f g : ι → α} : (⨅ x, f x) ⊓ (⨅ x, g x) ≤ ⨅ x /-- Indexed version of `exists_lt_of_lt_csSup`. When `b < iSup f`, there is an element `i` such that `b < f i`. -/ -@[to_dual +@[to_dual exists_lt_of_ciInf_lt /-- Indexed version of `exists_lt_of_csInf_lt`. When `iInf f < a`, there is an element `i` such that `f i < a`. -/]