From 8b2dfa4e358ef9969cc5f519810315b205710e24 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 21 Feb 2024 03:47:55 +0000 Subject: [PATCH 01/20] =?UTF-8?q?feat:=20`StarAlgEquiv`'s=20on=20C?= =?UTF-8?q?=E2=8B=86-algebras=20are=20isometric=20(#10504)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Analysis/NormedSpace/Star/Spectrum.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Mathlib/Analysis/NormedSpace/Star/Spectrum.lean b/Mathlib/Analysis/NormedSpace/Star/Spectrum.lean index 1a67cda62dbde..17c0e1526a4fc 100644 --- a/Mathlib/Analysis/NormedSpace/Star/Spectrum.lean +++ b/Mathlib/Analysis/NormedSpace/Star/Spectrum.lean @@ -155,6 +155,24 @@ noncomputable instance (priority := 100) : ContinuousLinearMapClass F ℂ A B := end StarAlgHom +namespace StarAlgEquiv + +variable {F A B : Type*} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [StarRing A] + [CstarRing A] [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] [StarRing B] [CstarRing B] + [EquivLike F A B] [NonUnitalAlgEquivClass F ℂ A B] [StarAlgEquivClass F ℂ A B] + +lemma nnnorm_map (φ : F) (a : A) : ‖φ a‖₊ = ‖a‖₊ := + le_antisymm (StarAlgHom.nnnorm_apply_le φ a) <| by + simpa using StarAlgHom.nnnorm_apply_le (symm (φ : A ≃⋆ₐ[ℂ] B)) ((φ : A ≃⋆ₐ[ℂ] B) a) + +lemma norm_map (φ : F) (a : A) : ‖φ a‖ = ‖a‖ := + congr_arg NNReal.toReal (nnnorm_map φ a) + +lemma isometry (φ : F) : Isometry φ := + AddMonoidHomClass.isometry_of_norm φ (norm_map φ) + +end StarAlgEquiv + end namespace WeakDual From 1726adc5793ca3586d06f778d885e256c6259b18 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 21 Feb 2024 10:03:05 +0000 Subject: [PATCH 02/20] chore: bump to nightly-2024-02-21 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 0e72c49726644..423cb480096c4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-02-20 +leanprover/lean4:nightly-2024-02-21 From 88a36ee6447ba3cd2bb6f1c525079aa0b1268593 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 21 Feb 2024 13:31:21 +0000 Subject: [PATCH 03/20] feat: instances `CovariantAddLE` and `OrderBot` for kernel (#10802) --- Mathlib/Probability/Kernel/Basic.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Mathlib/Probability/Kernel/Basic.lean b/Mathlib/Probability/Kernel/Basic.lean index c05dad0306633..2cb4478f5b971 100644 --- a/Mathlib/Probability/Kernel/Basic.lean +++ b/Mathlib/Probability/Kernel/Basic.lean @@ -70,6 +70,16 @@ instance {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] : coe := Subtype.val coe_injective' := Subtype.val_injective +instance kernel.instCovariantAddLE {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] : + CovariantClass (kernel α β) (kernel α β) (· + ·) (· ≤ ·) := + ⟨fun _ _ _ hμ a ↦ add_le_add_left (hμ a) _⟩ + +noncomputable +instance kernel.instOrderBot {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] : + OrderBot (kernel α β) where + bot := 0 + bot_le κ a := by simp only [ZeroMemClass.coe_zero, Pi.zero_apply, Measure.zero_le] + variable {α β ι : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} namespace kernel From c63ddc259fc8177934b931d4934d9b20cad89cb0 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 21 Feb 2024 14:19:37 +0000 Subject: [PATCH 04/20] feat: unitary elements are normal (#10778) --- Mathlib/Algebra/Star/SelfAdjoint.lean | 5 +++++ Mathlib/Algebra/Star/Unitary.lean | 15 ++++++++++++--- 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Star/SelfAdjoint.lean b/Mathlib/Algebra/Star/SelfAdjoint.lean index f9c4d67aa8ce9..9cec401802ac2 100644 --- a/Mathlib/Algebra/Star/SelfAdjoint.lean +++ b/Mathlib/Algebra/Star/SelfAdjoint.lean @@ -596,6 +596,11 @@ protected instance IsStarNormal.neg [Ring R] [StarAddMonoid R] {x : R} [IsStarNo IsStarNormal (-x) := ⟨show star (-x) * -x = -x * star (-x) by simp_rw [star_neg, neg_mul_neg, star_comm_self']⟩ +protected instance IsStarNormal.map {F R S : Type*} [Mul R] [Star R] [Mul S] [Star S] + [FunLike F R S] [MulHomClass F R S] [StarHomClass F R S] (f : F) (r : R) [hr : IsStarNormal r] : + IsStarNormal (f r) where + star_comm_self := by simpa [map_star] using congr(f $(hr.star_comm_self)) + -- see Note [lower instance priority] instance (priority := 100) TrivialStar.isStarNormal [Mul R] [StarMul R] [TrivialStar R] {x : R} : IsStarNormal x := diff --git a/Mathlib/Algebra/Star/Unitary.lean b/Mathlib/Algebra/Star/Unitary.lean index 21cc9de379220..d3732e82a9689 100644 --- a/Mathlib/Algebra/Star/Unitary.lean +++ b/Mathlib/Algebra/Star/Unitary.lean @@ -3,7 +3,7 @@ Copyright (c) 2022 Frédéric Dupuis. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Shing Tak Lam, Frédéric Dupuis -/ -import Mathlib.Algebra.Star.Basic +import Mathlib.Algebra.Star.SelfAdjoint import Mathlib.GroupTheory.Submonoid.Operations #align_import algebra.star.unitary from "leanprover-community/mathlib"@"247a102b14f3cebfee126293341af5f6bed00237" @@ -135,9 +135,18 @@ def toUnits : unitary R →* Rˣ map_mul' _ _ := Units.ext rfl #align unitary.to_units unitary.toUnits -theorem to_units_injective : Function.Injective (toUnits : unitary R → Rˣ) := fun _ _ h => +theorem toUnits_injective : Function.Injective (toUnits : unitary R → Rˣ) := fun _ _ h => Subtype.ext <| Units.ext_iff.mp h -#align unitary.to_units_injective unitary.to_units_injective +#align unitary.to_units_injective unitary.toUnits_injective + +instance instIsStarNormal (u : unitary R) : IsStarNormal u where + star_comm_self := star_mul_self u |>.trans <| (mul_star_self u).symm + +instance coe_isStarNormal (u : unitary R) : IsStarNormal (u : R) where + star_comm_self := congr(Subtype.val $(star_comm_self' u)) + +lemma _root_.isStarNormal_of_mem_unitary {u : R} (hu : u ∈ unitary R) : IsStarNormal u := + coe_isStarNormal ⟨u, hu⟩ end Monoid From e6bc0f58c617b13224bb5030c0a448cc04732acd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 21 Feb 2024 14:19:37 +0000 Subject: [PATCH 05/20] feat: add `snorm_restrict_le` (#10788) --- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean index 4c441d6cf9b88..711842ca21de6 100644 --- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean +++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean @@ -621,6 +621,10 @@ theorem Memℒp.mono_measure {f : α → E} (hμν : ν ≤ μ) (hf : Memℒp f ⟨hf.1.mono_measure hμν, (snorm_mono_measure f hμν).trans_lt hf.2⟩ #align measure_theory.mem_ℒp.mono_measure MeasureTheory.Memℒp.mono_measure +lemma snorm_restrict_le (f : α → F) (p : ℝ≥0∞) (μ : Measure α) (s : Set α) : + snorm f p (μ.restrict s) ≤ snorm f p μ := + snorm_mono_measure f Measure.restrict_le_self + theorem Memℒp.restrict (s : Set α) {f : α → E} (hf : Memℒp f p μ) : Memℒp f p (μ.restrict s) := hf.mono_measure Measure.restrict_le_self #align measure_theory.mem_ℒp.restrict MeasureTheory.Memℒp.restrict From 79d097fa4a3758eb0433fe9937b112bab9715d4e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 21 Feb 2024 14:19:38 +0000 Subject: [PATCH 06/20] feat: MeasurableSpace.generateFrom lemmas (#10797) --- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Defs.lean b/Mathlib/MeasureTheory/MeasurableSpace/Defs.lean index 31b1db9d8045f..5a2240bfbbebd 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/Defs.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/Defs.lean @@ -453,6 +453,14 @@ theorem generateFrom_sup_generateFrom {s t : Set (Set α)} : (@giGenerateFrom α).gc.l_sup.symm #align measurable_space.generate_from_sup_generate_from MeasurableSpace.generateFrom_sup_generateFrom +lemma iSup_generateFrom (s : ι → Set (Set α)) : + ⨆ i, generateFrom (s i) = generateFrom (⋃ i, s i) := + (@MeasurableSpace.giGenerateFrom α).gc.l_iSup.symm + +@[simp] +lemma generateFrom_empty : generateFrom (∅ : Set (Set α)) = ⊥ := + le_bot_iff.mp (generateFrom_le (by simp)) + theorem generateFrom_singleton_empty : generateFrom {∅} = (⊥ : MeasurableSpace α) := bot_unique <| generateFrom_le <| by simp [@MeasurableSet.empty α ⊥] #align measurable_space.generate_from_singleton_empty MeasurableSpace.generateFrom_singleton_empty From 7d7cd8cfc73c3d934fd4b35ff65791921b93a1ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 21 Feb 2024 14:19:39 +0000 Subject: [PATCH 07/20] chore: add `@[simp]` to `limsup_const` and `liminf_const` (#10798) --- Mathlib/Order/LiminfLimsup.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Order/LiminfLimsup.lean b/Mathlib/Order/LiminfLimsup.lean index 74b135ea9525f..473baac089541 100644 --- a/Mathlib/Order/LiminfLimsup.lean +++ b/Mathlib/Order/LiminfLimsup.lean @@ -663,11 +663,13 @@ theorem liminf_congr {α : Type*} [ConditionallyCompleteLattice β] {f : Filter limsup_congr (β := βᵒᵈ) h #align filter.liminf_congr Filter.liminf_congr +@[simp] theorem limsup_const {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} [NeBot f] (b : β) : limsup (fun _ => b) f = b := by simpa only [limsup_eq, eventually_const] using csInf_Ici #align filter.limsup_const Filter.limsup_const +@[simp] theorem liminf_const {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} [NeBot f] (b : β) : liminf (fun _ => b) f = b := limsup_const (β := βᵒᵈ) b @@ -756,12 +758,14 @@ theorem bliminf_false {f : Filter β} {u : β → α} : (bliminf u f fun _ => Fa #align filter.bliminf_false Filter.bliminf_false /-- Same as limsup_const applied to `⊥` but without the `NeBot f` assumption -/ +@[simp] theorem limsup_const_bot {f : Filter β} : limsup (fun _ : β => (⊥ : α)) f = (⊥ : α) := by rw [limsup_eq, eq_bot_iff] exact sInf_le (eventually_of_forall fun _ => le_rfl) #align filter.limsup_const_bot Filter.limsup_const_bot /-- Same as limsup_const applied to `⊤` but without the `NeBot f` assumption -/ +@[simp] theorem liminf_const_top {f : Filter β} : liminf (fun _ : β => (⊤ : α)) f = (⊤ : α) := limsup_const_bot (α := αᵒᵈ) #align filter.liminf_const_top Filter.liminf_const_top From 24c9aaa1324fd7dcb9235ea365368b000f0a9e0e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 21 Feb 2024 14:19:40 +0000 Subject: [PATCH 08/20] feat: add `kernel.(co)map_id` (#10801) --- Mathlib/Probability/Kernel/Basic.lean | 4 ++++ Mathlib/Probability/Kernel/Composition.lean | 12 ++++++++++++ 2 files changed, 16 insertions(+) diff --git a/Mathlib/Probability/Kernel/Basic.lean b/Mathlib/Probability/Kernel/Basic.lean index 2cb4478f5b971..32c5f7edd7705 100644 --- a/Mathlib/Probability/Kernel/Basic.lean +++ b/Mathlib/Probability/Kernel/Basic.lean @@ -608,6 +608,10 @@ theorem comapRight_apply' (κ : kernel α β) (hf : MeasurableEmbedding f) (a : Measure.comap_apply _ hf.injective (fun s => hf.measurableSet_image.mpr) _ ht] #align probability_theory.kernel.comap_right_apply' ProbabilityTheory.kernel.comapRight_apply' +@[simp] +lemma comapRight_id (κ : kernel α β) : comapRight κ MeasurableEmbedding.id = κ := by + ext _ _ hs; rw [comapRight_apply' _ _ _ hs]; simp + theorem IsMarkovKernel.comapRight (κ : kernel α β) (hf : MeasurableEmbedding f) (hκ : ∀ a, κ a (Set.range f) = 1) : IsMarkovKernel (comapRight κ hf) := by refine' ⟨fun a => ⟨_⟩⟩ diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean index 03cfeed68e94b..0afa83e67c486 100644 --- a/Mathlib/Probability/Kernel/Composition.lean +++ b/Mathlib/Probability/Kernel/Composition.lean @@ -588,6 +588,12 @@ theorem map_apply' (κ : kernel α β) (hf : Measurable f) (a : α) {s : Set γ} lemma map_zero (hf : Measurable f) : kernel.map (0 : kernel α β) f hf = 0 := by ext; rw [kernel.map_apply]; simp +@[simp] +lemma map_id (κ : kernel α β) : map κ id measurable_id = κ := by ext a; rw [map_apply]; simp + +@[simp] +lemma map_id' (κ : kernel α β) : map κ (fun a ↦ a) measurable_id = κ := map_id κ + nonrec theorem lintegral_map (κ : kernel α β) (hf : Measurable f) (a : α) {g' : γ → ℝ≥0∞} (hg : Measurable g') : ∫⁻ b, g' b ∂map κ f hf a = ∫⁻ a, g' (f a) ∂κ a := by rw [map_apply _ hf, lintegral_map hg hf] @@ -646,6 +652,12 @@ theorem comap_apply' (κ : kernel α β) (hg : Measurable g) (c : γ) (s : Set lemma comap_zero (hg : Measurable g) : kernel.comap (0 : kernel α β) g hg = 0 := by ext; rw [kernel.comap_apply]; simp +@[simp] +lemma comap_id (κ : kernel α β) : comap κ id measurable_id = κ := by ext a; rw [comap_apply]; simp + +@[simp] +lemma comap_id' (κ : kernel α β) : comap κ (fun a ↦ a) measurable_id = κ := comap_id κ + theorem lintegral_comap (κ : kernel α β) (hg : Measurable g) (c : γ) (g' : β → ℝ≥0∞) : ∫⁻ b, g' b ∂comap κ g hg c = ∫⁻ b, g' b ∂κ (g c) := rfl From 359d4b984ae2b170505d30ae24fe81bdf220f916 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 21 Feb 2024 15:14:10 +0000 Subject: [PATCH 09/20] feat(UniformSpace): add `UniformSpace.isClosed_ball` (#10782) --- Mathlib/Topology/UniformSpace/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean index 62e80f9515f4d..1c7b2a81746e6 100644 --- a/Mathlib/Topology/UniformSpace/Basic.lean +++ b/Mathlib/Topology/UniformSpace/Basic.lean @@ -675,6 +675,10 @@ theorem UniformSpace.isOpen_ball (x : α) {V : Set (α × α)} (hV : IsOpen V) : hV.preimage <| continuous_const.prod_mk continuous_id #align uniform_space.is_open_ball UniformSpace.isOpen_ball +theorem UniformSpace.isClosed_ball (x : α) {V : Set (α × α)} (hV : IsClosed V) : + IsClosed (ball x V) := + hV.preimage <| continuous_const.prod_mk continuous_id + theorem mem_comp_comp {V W M : Set (β × β)} (hW' : SymmetricRel W) {p : β × β} : p ∈ V ○ M ○ W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty := by cases' p with x y From 807b7b42daa712c8f28a6c9dcac654202349abbe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 21 Feb 2024 15:14:11 +0000 Subject: [PATCH 10/20] feat: add `tendsto_nat_ceil_atTop` (#10786) --- Mathlib/Analysis/SpecificLimits/Basic.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index 26412ecbb362d..66986a544eab6 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -624,6 +624,11 @@ theorem tendsto_nat_floor_atTop {α : Type*} [LinearOrderedSemiring α] [FloorSe Nat.floor_mono.tendsto_atTop_atTop fun x ↦ ⟨max 0 (x + 1), by simp [Nat.le_floor_iff]⟩ #align tendsto_nat_floor_at_top tendsto_nat_floor_atTop +lemma tendsto_nat_ceil_atTop {α : Type*} [LinearOrderedSemiring α] [FloorSemiring α] : + Tendsto (fun x : α ↦ ⌈x⌉₊) atTop atTop := by + refine Nat.ceil_mono.tendsto_atTop_atTop (fun x ↦ ⟨x, ?_⟩) + simp only [Nat.ceil_natCast, le_refl] + lemma tendsto_nat_floor_mul_atTop {α : Type _} [LinearOrderedSemifield α] [FloorSemiring α] [Archimedean α] (a : α) (ha : 0 < a) : Tendsto (fun (x:ℕ) => ⌊a * x⌋₊) atTop atTop := Tendsto.comp tendsto_nat_floor_atTop From bafc1ac756ac723440367f5bbd20254ccf6e886a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 21 Feb 2024 15:14:12 +0000 Subject: [PATCH 11/20] feat: add `MeasurableEmbedding.comap_add` (#10795) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Also add a simp attribute to `AbsolutelyContinuous.zero`. Co-authored-by: Rémy Degenne --- Mathlib/MeasureTheory/Measure/MeasureSpace.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean index f8e9986170192..06c53526b7029 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean +++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean @@ -1617,6 +1617,7 @@ instance instIsRefl [MeasurableSpace α] : IsRefl (Measure α) (· ≪ ·) := ⟨fun _ => AbsolutelyContinuous.rfl⟩ #align measure_theory.measure.absolutely_continuous.is_refl MeasureTheory.Measure.AbsolutelyContinuous.instIsRefl +@[simp] protected lemma zero (μ : Measure α) : 0 ≪ μ := fun s _ ↦ by simp @[trans] @@ -2123,6 +2124,11 @@ nonrec theorem map_apply (μ : Measure α) (s : Set β) : μ.map f s = μ (f ⁻ _ = μ (f ⁻¹' s) := by rw [map_apply hf.measurable htm, hft, measure_toMeasurable] #align measurable_embedding.map_apply MeasurableEmbedding.map_apply +lemma comap_add (μ ν : Measure β) : (μ + ν).comap f = μ.comap f + ν.comap f := by + ext s hs + simp only [← comapₗ_eq_comap _ hf.injective (fun _ ↦ hf.measurableSet_image.mpr) _ hs, + _root_.map_add, add_apply] + end MeasurableEmbedding namespace MeasurableEquiv From dd9c1eb3dad6757ffbd65d6e5d5447e913527cd3 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 21 Feb 2024 15:14:13 +0000 Subject: [PATCH 12/20] feat: provide an instance of `Fintype (Fin2 n)` (#10805) This enables use of the `fin_cases` tactic on premises `i : Fin2 _` --- Mathlib/Data/Fin/Fin2.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/Data/Fin/Fin2.lean b/Mathlib/Data/Fin/Fin2.lean index e09451db0d4ed..3dd964d08e1a0 100644 --- a/Mathlib/Data/Fin/Fin2.lean +++ b/Mathlib/Data/Fin/Fin2.lean @@ -6,6 +6,7 @@ Authors: Mario Carneiro import Std.Tactic.NoMatch import Mathlib.Init.Data.Nat.Notation import Mathlib.Mathport.Rename +import Mathlib.Data.Fintype.Basic #align_import data.fin.fin2 from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23" @@ -131,4 +132,11 @@ def ofNat' : ∀ {n} (m) [IsLT m n], Fin2 n instance : Inhabited (Fin2 1) := ⟨fz⟩ +instance instFintype : ∀ n, Fintype (Fin2 n) + | 0 => ⟨∅, Fin2.elim0⟩ + | n+1 => + let ⟨elems, compl⟩ := instFintype n + { elems := elems.map ⟨Fin2.fs, @fs.inj _⟩ |>.cons .fz (by simp) + complete := by rintro (_|i) <;> simp [compl] } + end Fin2 From c0d05dba72aaaf12c72c62c4ab84e6e781acbfd5 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 21 Feb 2024 15:14:14 +0000 Subject: [PATCH 13/20] feat: transport an `MvQPF` instance along an equivalence (#10806) This is code ported from [alexkeizer/QpfTypes](https://github.com/alexkeizer/QpfTypes). It's primary use is to show that existing type functions which are equivalent to polynomial functors but not defined as such (e.g., `Sum`, `Prod`, etc.) are QPFs. --- Mathlib/Control/Functor/Multivariate.lean | 6 ++++++ Mathlib/Data/QPF/Multivariate/Basic.lean | 13 +++++++++++++ 2 files changed, 19 insertions(+) diff --git a/Mathlib/Control/Functor/Multivariate.lean b/Mathlib/Control/Functor/Multivariate.lean index e093beb4c4626..cedee8f75af3b 100644 --- a/Mathlib/Control/Functor/Multivariate.lean +++ b/Mathlib/Control/Functor/Multivariate.lean @@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Mario Carneiro, Simon Hudon -/ import Mathlib.Data.Fin.Fin2 import Mathlib.Data.TypeVec +import Mathlib.Logic.Equiv.Defs #align_import control.functor.multivariate from "leanprover-community/mathlib"@"008205aa645b3f194c1da47025c5f110c8406eab" @@ -242,4 +243,9 @@ theorem LiftR_RelLast_iff (x y : F (α ::: β)) : end LiftPLastPredIff +/-- Any type function that is (extensionally) equivalent to a functor, is itself a functor -/ +def ofEquiv {F F' : TypeVec.{u} n → Type*} [MvFunctor F'] (eqv : ∀ α, F α ≃ F' α) : + MvFunctor F where + map f x := (eqv _).symm <| f <$$> eqv _ x + end MvFunctor diff --git a/Mathlib/Data/QPF/Multivariate/Basic.lean b/Mathlib/Data/QPF/Multivariate/Basic.lean index 275ac121893bf..65bb4d46d5adc 100644 --- a/Mathlib/Data/QPF/Multivariate/Basic.lean +++ b/Mathlib/Data/QPF/Multivariate/Basic.lean @@ -283,4 +283,17 @@ theorem liftpPreservation_iff_uniform : q.LiftPPreservation ↔ q.IsUniform := b rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_isUniform] #align mvqpf.liftp_preservation_iff_uniform MvQPF.liftpPreservation_iff_uniform +/-- Any type function `F` that is (extensionally) equivalent to a QPF, is itself a QPF, +assuming that the functorial map of `F` behaves similar to `MvFunctor.ofEquiv eqv` -/ +def ofEquiv {F F' : TypeVec.{u} n → Type*} [MvFunctor F'] [q : MvQPF F'] [MvFunctor F] + (eqv : ∀ α, F α ≃ F' α) + (map_eq : ∀ (α β : TypeVec n) (f : α ⟹ β) (a : F α), + f <$$> a = ((eqv _).symm <| f <$$> eqv _ a) := by intros; rfl) : + MvQPF F where + P := q.P + abs α := (eqv _).symm <| q.abs α + repr α := q.repr <| eqv _ α + abs_repr := by simp [q.abs_repr] + abs_map := by simp [q.abs_map, map_eq] + end MvQPF From 5722a178bb23265969b68fe9b6f95606515860a1 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 21 Feb 2024 15:14:15 +0000 Subject: [PATCH 14/20] feat: show that every polynomial functor is a (trivial) QPF (#10807) Every polynomial functor `P` is trivially also a quotient of a polynomial functor, namely, it's a quotient of itself through equality. That is, `abs` and `repr` are just the identity. --- Mathlib/Data/QPF/Multivariate/Basic.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/Data/QPF/Multivariate/Basic.lean b/Mathlib/Data/QPF/Multivariate/Basic.lean index 65bb4d46d5adc..0706a84284b71 100644 --- a/Mathlib/Data/QPF/Multivariate/Basic.lean +++ b/Mathlib/Data/QPF/Multivariate/Basic.lean @@ -297,3 +297,11 @@ def ofEquiv {F F' : TypeVec.{u} n → Type*} [MvFunctor F'] [q : MvQPF F'] [MvFu abs_map := by simp [q.abs_map, map_eq] end MvQPF + +/-- Every polynomial functor is a (trivial) QPF -/ +instance MvPFunctor.instMvQPFObj {n} (P : MvPFunctor n) : MvQPF P where + P := P + abs := id + repr := id + abs_repr := by intros; rfl + abs_map := by intros; rfl From b06068c3595d2afad6662600de0e3a8ec837198b Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 21 Feb 2024 16:46:12 +0000 Subject: [PATCH 15/20] chore: classify `added to ease automation` porting notes (#10689) - [x] Classifies by adding issue number (#10688) to porting notes claiming anything semantically equivalent to `added to ease automation`. - [x] Enforce singular convention converting "porting notes" to "porting note". --- Mathlib/Algebra/PUnitInstances.lean | 4 ++-- Mathlib/AlgebraicGeometry/Scheme.lean | 2 +- Mathlib/AlgebraicTopology/SimplicialObject.lean | 8 ++++---- Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean | 2 +- Mathlib/CategoryTheory/Comma/Arrow.lean | 4 ++-- Mathlib/CategoryTheory/FintypeCat.lean | 2 +- Mathlib/CategoryTheory/GradedObject.lean | 2 +- Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean | 2 +- Mathlib/CategoryTheory/Limits/Shapes/Products.lean | 2 +- Mathlib/CategoryTheory/Monad/Basic.lean | 4 ++-- Mathlib/CategoryTheory/Monoidal/CommMon_.lean | 5 +++-- Mathlib/CategoryTheory/Preadditive/Mat.lean | 2 +- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean | 4 ++-- Mathlib/Data/List/Defs.lean | 4 ++-- Mathlib/RepresentationTheory/Action/Limits.lean | 2 +- Mathlib/SetTheory/Lists.lean | 2 +- 16 files changed, 26 insertions(+), 25 deletions(-) diff --git a/Mathlib/Algebra/PUnitInstances.lean b/Mathlib/Algebra/PUnitInstances.lean index 45c2303e5112d..d404d90c91d51 100644 --- a/Mathlib/Algebra/PUnitInstances.lean +++ b/Mathlib/Algebra/PUnitInstances.lean @@ -97,12 +97,12 @@ instance normalizedGCDMonoid : NormalizedGCDMonoid PUnit where normalize_gcd := by intros; rfl normalize_lcm := by intros; rfl --- Porting notes (#10618): simpNF lint: simp can prove this @[simp] +-- Porting note (#10618): simpNF lint: simp can prove this @[simp] theorem gcd_eq : gcd x y = unit := rfl #align punit.gcd_eq PUnit.gcd_eq --- Porting notes (#10618): simpNF lint: simp can prove this @[simp] +-- Porting note (#10618): simpNF lint: simp can prove this @[simp] theorem lcm_eq : lcm x y = unit := rfl #align punit.lcm_eq PUnit.lcm_eq diff --git a/Mathlib/AlgebraicGeometry/Scheme.lean b/Mathlib/AlgebraicGeometry/Scheme.lean index 47d718eb557f2..a57aa37927172 100644 --- a/Mathlib/AlgebraicGeometry/Scheme.lean +++ b/Mathlib/AlgebraicGeometry/Scheme.lean @@ -59,7 +59,7 @@ def Hom (X Y : Scheme) : Type* := instance : Category Scheme := { InducedCategory.category Scheme.toLocallyRingedSpace with Hom := Hom } --- porting note: added to ease automation +-- porting note (#10688): added to ease automation @[continuity] lemma Hom.continuous {X Y : Scheme} (f : X ⟶ Y) : Continuous f.1.base := f.1.base.2 diff --git a/Mathlib/AlgebraicTopology/SimplicialObject.lean b/Mathlib/AlgebraicTopology/SimplicialObject.lean index a63a776e3d4a6..88296fcbd5df2 100644 --- a/Mathlib/AlgebraicTopology/SimplicialObject.lean +++ b/Mathlib/AlgebraicTopology/SimplicialObject.lean @@ -76,7 +76,7 @@ instance [HasColimits C] : HasColimits (SimplicialObject C) := variable {C} --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[ext] lemma hom_ext {X Y : SimplicialObject C} (f g : X ⟶ Y) (h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n) : f = g := @@ -300,7 +300,7 @@ variable {C} namespace Augmented --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[ext] lemma hom_ext {X Y : Augmented C} (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) : f = g := @@ -446,7 +446,7 @@ instance [HasColimits C] : HasColimits (CosimplicialObject C) := variable {C} --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[ext] lemma hom_ext {X Y : CosimplicialObject C} (f g : X ⟶ Y) (h : ∀ (n : SimplexCategory), f.app n = g.app n) : f = g := @@ -672,7 +672,7 @@ variable {C} namespace Augmented --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[ext] lemma hom_ext {X Y : Augmented C} (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) : f = g := diff --git a/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean b/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean index 052edebda5b78..24a0c92c72ea5 100644 --- a/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean +++ b/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean @@ -67,7 +67,7 @@ instance toAddMonoidHomClass {V W : SemiNormedGroupCat} : AddMonoidHomClass (V map_add f := f.map_add' map_zero f := (AddMonoidHom.mk' f.toFun f.map_add').map_zero --- Porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[ext] lemma ext {M N : SemiNormedGroupCat} {f₁ f₂ : M ⟶ N} (h : ∀ (x : M), f₁ x = f₂ x) : f₁ = f₂ := DFunLike.ext _ _ h diff --git a/Mathlib/CategoryTheory/Comma/Arrow.lean b/Mathlib/CategoryTheory/Comma/Arrow.lean index d7db57b59180b..f5214a34fe2a4 100644 --- a/Mathlib/CategoryTheory/Comma/Arrow.lean +++ b/Mathlib/CategoryTheory/Comma/Arrow.lean @@ -64,12 +64,12 @@ theorem id_right (f : Arrow T) : CommaMorphism.right (𝟙 f) = 𝟙 f.right := rfl #align category_theory.arrow.id_right CategoryTheory.Arrow.id_right --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[simp, reassoc] theorem comp_left {X Y Z : Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).left = f.left ≫ g.left := rfl --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[simp, reassoc] theorem comp_right {X Y Z : Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).right = f.right ≫ g.right := rfl diff --git a/Mathlib/CategoryTheory/FintypeCat.lean b/Mathlib/CategoryTheory/FintypeCat.lean index 32fcb3ed4d865..987ae42acd2e4 100644 --- a/Mathlib/CategoryTheory/FintypeCat.lean +++ b/Mathlib/CategoryTheory/FintypeCat.lean @@ -92,7 +92,7 @@ lemma hom_inv_id_apply {X Y : FintypeCat} (f : X ≅ Y) (x : X) : f.inv (f.hom x lemma inv_hom_id_apply {X Y : FintypeCat} (f : X ≅ Y) (y : Y) : f.hom (f.inv y) = y := congr_fun f.inv_hom_id y --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[ext] lemma hom_ext {X Y : FintypeCat} (f g : X ⟶ Y) (h : ∀ x, f x = g x) : f = g := by funext diff --git a/Mathlib/CategoryTheory/GradedObject.lean b/Mathlib/CategoryTheory/GradedObject.lean index 0f88b78c8f8c3..4840cab046488 100644 --- a/Mathlib/CategoryTheory/GradedObject.lean +++ b/Mathlib/CategoryTheory/GradedObject.lean @@ -70,7 +70,7 @@ instance categoryOfGradedObjects (β : Type w) : Category.{max w v} (GradedObjec CategoryTheory.pi fun _ => C #align category_theory.graded_object.category_of_graded_objects CategoryTheory.GradedObject.categoryOfGradedObjects --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[ext] lemma hom_ext {X Y : GradedObject β C} (f g : X ⟶ Y) (h : ∀ x, f x = g x) : f = g := by funext diff --git a/Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean b/Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean index 2dac954477938..685738f48f6c0 100644 --- a/Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean +++ b/Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean @@ -28,7 +28,7 @@ namespace KaroubiKaroubi variable (C : Type*) [Category C] --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[reassoc (attr := simp)] lemma idem_f (P : Karoubi (Karoubi C)) : P.p.f ≫ P.p.f = P.p.f := by simpa only [hom_ext_iff, comp_f] using P.idem diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean index 5abf4b610c83a..54b0237a7b97e 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean @@ -203,7 +203,7 @@ abbrev Sigma.ι (f : β → C) [HasCoproduct f] (b : β) : f b ⟶ ∐ f := colimit.ι (Discrete.functor f) (Discrete.mk b) #align category_theory.limits.sigma.ι CategoryTheory.Limits.Sigma.ι --- porting note: added the next two lemmas to ease automation; without these lemmas, +-- porting note (#10688): added the next two lemmas to ease automation; without these lemmas, -- `limit.hom_ext` would be applied, but the goal would involve terms -- in `Discrete β` rather than `β` itself @[ext 1050] diff --git a/Mathlib/CategoryTheory/Monad/Basic.lean b/Mathlib/CategoryTheory/Monad/Basic.lean index fb0bc259ca4c3..95d578b8d13f4 100644 --- a/Mathlib/CategoryTheory/Monad/Basic.lean +++ b/Mathlib/CategoryTheory/Monad/Basic.lean @@ -203,12 +203,12 @@ instance : Quiver (Monad C) where instance : Quiver (Comonad C) where Hom := ComonadHom --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[ext] lemma MonadHom.ext' {T₁ T₂ : Monad C} (f g : T₁ ⟶ T₂) (h : f.app = g.app) : f = g := MonadHom.ext f g h --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[ext] lemma ComonadHom.ext' {T₁ T₂ : Comonad C} (f g : T₁ ⟶ T₂) (h : f.app = g.app) : f = g := ComonadHom.ext f g h diff --git a/Mathlib/CategoryTheory/Monoidal/CommMon_.lean b/Mathlib/CategoryTheory/Monoidal/CommMon_.lean index 4abc94fdb8686..a28683acd4a95 100644 --- a/Mathlib/CategoryTheory/Monoidal/CommMon_.lean +++ b/Mathlib/CategoryTheory/Monoidal/CommMon_.lean @@ -67,7 +67,8 @@ set_option linter.uppercaseLean3 false in lemma hom_ext {A B : CommMon_ C} (f g : A ⟶ B) (h : f.hom = g.hom) : f = g := Mon_.Hom.ext _ _ h --- porting note: the following two lemmas `id'` and `comp'` have been added to ease automation; +-- Porting note (#10688): the following two lemmas `id'` and `comp'` +-- have been added to ease automation; @[simp] lemma id' (A : CommMon_ C) : (𝟙 A : A.toMon_ ⟶ A.toMon_) = 𝟙 (A.toMon_) := rfl @@ -144,7 +145,7 @@ set_option linter.uppercaseLean3 false in variable (C) (D) --- porting note: added @[simps] to ease automation +-- Porting note (#10688): added @[simps] to ease automation /-- `mapCommMon` is functorial in the lax braided functor. -/ @[simps] def mapCommMonFunctor : LaxBraidedFunctor C D ⥤ CommMon_ C ⥤ CommMon_ D where diff --git a/Mathlib/CategoryTheory/Preadditive/Mat.lean b/Mathlib/CategoryTheory/Preadditive/Mat.lean index fec2909e9bfae..f92c81f4f5a58 100644 --- a/Mathlib/CategoryTheory/Preadditive/Mat.lean +++ b/Mathlib/CategoryTheory/Preadditive/Mat.lean @@ -666,7 +666,7 @@ instance (X Y : Mat R) : AddCommGroup (X ⟶ Y) := by variable {R} --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[simp] theorem add_apply {M N : Mat R} (f g : M ⟶ N) (i j) : (f + g) i j = f i j + g i j := rfl diff --git a/Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean b/Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean index aa2899c7a0e9a..1ee11ac7a0f39 100644 --- a/Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean +++ b/Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean @@ -55,7 +55,7 @@ def FirstObj : Type max v u := variable {P R} --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[ext] lemma FirstObj.ext (z₁ z₂ : FirstObj P R) (h : ∀ (Y : C) (f : Y ⟶ X) (hf : R f), (Pi.π _ ⟨Y, f, hf⟩ : FirstObj P R ⟶ _) z₁ = @@ -105,7 +105,7 @@ def SecondObj : Type max v u := variable {P S} --- porting note: added to ease automation +-- Porting note (#10688): added to ease automation @[ext] lemma SecondObj.ext (z₁ z₂ : SecondObj P S) (h : ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f), (Pi.π _ ⟨Y, Z, g, f, hf⟩ : SecondObj P S ⟶ _) z₁ = diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean index 4f839bac6c23a..b871d21ffbd05 100644 --- a/Mathlib/Data/List/Defs.lean +++ b/Mathlib/Data/List/Defs.lean @@ -21,7 +21,7 @@ proofs about these definitions, those are contained in other files in `Data.List set_option autoImplicit true --- Porting notes +-- Porting note -- Many of the definitions in `Data.List.Defs` were already defined upstream in `Std4` -- These have been annotated with `#align`s -- To make this easier for review, the `#align`s have been placed in order of occurrence @@ -500,7 +500,7 @@ def map₂Right (f : Option α → β → γ) (as : List α) (bs : List β) : Li #align list.to_chunks_aux List.toChunksAux #align list.to_chunks List.toChunks --- porting notes -- was `unsafe` but removed for Lean 4 port +-- porting note -- was `unsafe` but removed for Lean 4 port -- TODO: naming is awkward... /-- Asynchronous version of `List.map`. -/ diff --git a/Mathlib/RepresentationTheory/Action/Limits.lean b/Mathlib/RepresentationTheory/Action/Limits.lean index bbf777859af2b..3325a23460568 100644 --- a/Mathlib/RepresentationTheory/Action/Limits.lean +++ b/Mathlib/RepresentationTheory/Action/Limits.lean @@ -205,7 +205,7 @@ section HasZeroMorphisms variable [HasZeroMorphisms V] --- porting note: in order to ease automation, the `Zero` instance is introduced separately, +-- porting note (#10688): in order to ease automation, the `Zero` instance is introduced separately, -- and the lemma `zero_hom` was moved just below instance {X Y : Action V G} : Zero (X ⟶ Y) := ⟨0, by aesop_cat⟩ diff --git a/Mathlib/SetTheory/Lists.lean b/Mathlib/SetTheory/Lists.lean index ec012e522154d..fbea5c08c40cd 100644 --- a/Mathlib/SetTheory/Lists.lean +++ b/Mathlib/SetTheory/Lists.lean @@ -83,7 +83,7 @@ def toList : ∀ {b}, Lists' α b → List (Lists α) | _, cons' a l => ⟨_, a⟩ :: l.toList #align lists'.to_list Lists'.toList --- Porting notes (#10618): removed @[simp] +-- Porting note (#10618): removed @[simp] -- simp can prove this: by simp only [@Lists'.toList, @Sigma.eta] theorem toList_cons (a : Lists α) (l) : toList (cons a l) = a :: l.toList := by simp #align lists'.to_list_cons Lists'.toList_cons From f17e232420d02eefb6b737b71f5dbb02385a3436 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 21 Feb 2024 16:46:13 +0000 Subject: [PATCH 16/20] =?UTF-8?q?refactor(MeasureTheory):=20redefine=20`?= =?UTF-8?q?=E2=89=A4`=20on=20measures=20(#10714)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Redefine `≤` on `MeasureTheory.Measure` so that `μ ≤ ν ↔ ∀ s, μ s ≤ ν s` by definition instead of `∀ s, MeasurableSet s → μ s ≤ ν s`. ### Reasons - this way it is defeq to `≤` on outer measures; - if we decide to introduce an order on all `DFunLike` types **and** migrate measures to `FunLike`, then this is unavoidable; - the reasoning for the old definition was "it's slightly easier to prove `μ ≤ ν` this way"; the counter-argument is "it's slightly harder to apply `μ ≤ ν` this way". ### Other changes - golf some proofs broken by this change; - add `@[gcongr]` tags to some `ENNReal` lemmas; - fix the name `ENNReal.coe_lt_coe_of_le` -> `ENNReal.ENNReal.coe_lt_coe_of_lt`; - drop an unneeded `MeasurableSet` assumption in `set_lintegral_pdf_le_map` --- Mathlib/Data/ENNReal/Basic.lean | 4 +- Mathlib/Data/ENNReal/Real.lean | 4 ++ .../MeasureTheory/Decomposition/Lebesgue.lean | 8 +-- .../Decomposition/RadonNikodym.lean | 14 ++--- .../MeasureTheory/Function/SimpleFunc.lean | 5 +- .../MeasureTheory/Integral/IntegrableOn.lean | 9 +-- Mathlib/MeasureTheory/Integral/Layercake.lean | 2 +- Mathlib/MeasureTheory/Integral/SetToL1.lean | 15 +++-- .../MeasureTheory/Measure/AEMeasurable.lean | 4 +- Mathlib/MeasureTheory/Measure/Hausdorff.lean | 3 +- .../MeasureTheory/Measure/MeasureSpace.lean | 61 ++++++++----------- Mathlib/MeasureTheory/Measure/Restrict.lean | 23 +++---- Mathlib/MeasureTheory/Measure/Sub.lean | 15 ++--- .../MeasureTheory/Measure/Typeclasses.lean | 4 +- .../MeasureTheory/Measure/WithDensity.lean | 2 +- Mathlib/Probability/Density.lean | 4 +- Mathlib/Probability/Kernel/CondCdf.lean | 9 ++- 17 files changed, 86 insertions(+), 100 deletions(-) diff --git a/Mathlib/Data/ENNReal/Basic.lean b/Mathlib/Data/ENNReal/Basic.lean index 7991777cbd090..3d70e7926194b 100644 --- a/Mathlib/Data/ENNReal/Basic.lean +++ b/Mathlib/Data/ENNReal/Basic.lean @@ -384,8 +384,8 @@ alias ⟨_, coe_le_coe_of_le⟩ := coe_le_coe attribute [gcongr] ENNReal.coe_le_coe_of_le -- Needed until `@[gcongr]` accepts iff statements -alias ⟨_, coe_lt_coe_of_le⟩ := coe_lt_coe -attribute [gcongr] ENNReal.coe_lt_coe_of_le +alias ⟨_, coe_lt_coe_of_lt⟩ := coe_lt_coe +attribute [gcongr] ENNReal.coe_lt_coe_of_lt theorem coe_mono : Monotone ofNNReal := fun _ _ => coe_le_coe.2 #align ennreal.coe_mono ENNReal.coe_mono diff --git a/Mathlib/Data/ENNReal/Real.lean b/Mathlib/Data/ENNReal/Real.lean index d04ffdb2eaf1b..fd7b149e9ad78 100644 --- a/Mathlib/Data/ENNReal/Real.lean +++ b/Mathlib/Data/ENNReal/Real.lean @@ -79,6 +79,7 @@ theorem toReal_le_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal ≤ b.toRe norm_cast #align ennreal.to_real_le_to_real ENNReal.toReal_le_toReal +@[gcongr] theorem toReal_mono (hb : b ≠ ∞) (h : a ≤ b) : a.toReal ≤ b.toReal := (toReal_le_toReal (ne_top_of_le_ne_top hb h) hb).2 h #align ennreal.to_real_mono ENNReal.toReal_mono @@ -96,10 +97,12 @@ theorem toReal_lt_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal < b.toReal norm_cast #align ennreal.to_real_lt_to_real ENNReal.toReal_lt_toReal +@[gcongr] theorem toReal_strict_mono (hb : b ≠ ∞) (h : a < b) : a.toReal < b.toReal := (toReal_lt_toReal h.ne_top hb).2 h #align ennreal.to_real_strict_mono ENNReal.toReal_strict_mono +@[gcongr] theorem toNNReal_mono (hb : b ≠ ∞) (h : a ≤ b) : a.toNNReal ≤ b.toNNReal := toReal_mono hb h #align ennreal.to_nnreal_mono ENNReal.toNNReal_mono @@ -172,6 +175,7 @@ theorem toReal_pos {a : ℝ≥0∞} (ha₀ : a ≠ 0) (ha_top : a ≠ ∞) : 0 < toReal_pos_iff.mpr ⟨bot_lt_iff_ne_bot.mpr ha₀, lt_top_iff_ne_top.mpr ha_top⟩ #align ennreal.to_real_pos ENNReal.toReal_pos +@[gcongr] theorem ofReal_le_ofReal {p q : ℝ} (h : p ≤ q) : ENNReal.ofReal p ≤ ENNReal.ofReal q := by simp [ENNReal.ofReal, Real.toNNReal_le_toNNReal h] #align ennreal.of_real_le_of_real ENNReal.ofReal_le_ofReal diff --git a/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean b/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean index 76e7517ced7a8..defdf792be89a 100644 --- a/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean @@ -791,14 +791,14 @@ theorem haveLebesgueDecomposition_of_finiteMeasure [IsFiniteMeasure μ] [IsFinit -- since we need `μ₁ + ν.withDensity ξ = μ` set μ₁ := μ - ν.withDensity ξ with hμ₁ have hle : ν.withDensity ξ ≤ μ := by - intro B hB + refine le_iff.2 fun B hB ↦ ?_ rw [hξ, withDensity_apply _ hB] simp_rw [iSup_apply] rw [lintegral_iSup (fun i => (iSup_mem_measurableLE _ hf₁ i).1) (iSup_monotone _)] exact iSup_le fun i => (iSup_mem_measurableLE _ hf₁ i).2 B hB have : IsFiniteMeasure (ν.withDensity ξ) := by refine' isFiniteMeasure_withDensity _ - have hle' := hle univ MeasurableSet.univ + have hle' := hle univ rw [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ] at hle' exact ne_top_of_le_ne_top (measure_ne_top _ _) hle' refine' ⟨⟨μ₁, ξ⟩, hξm, _, _⟩ @@ -854,7 +854,7 @@ theorem haveLebesgueDecomposition_of_finiteMeasure [IsFiniteMeasure μ] [IsFinit -- since `ν.withDensity ξ ≤ μ`, it is clear that `μ = μ₁ + ν.withDensity ξ` · rw [hμ₁]; ext1 A hA rw [Measure.coe_add, Pi.add_apply, Measure.sub_apply hA hle, add_comm, - add_tsub_cancel_of_le (hle A hA)]⟩ + add_tsub_cancel_of_le (hle A)]⟩ #align measure_theory.measure.have_lebesgue_decomposition_of_finite_measure MeasureTheory.Measure.haveLebesgueDecomposition_of_finiteMeasure attribute [local instance] haveLebesgueDecomposition_of_finiteMeasure @@ -913,7 +913,7 @@ instance (priority := 100) haveLebesgueDecomposition_of_sigmaFinite (μ ν : Mea intro i; rw [sum_apply _ ((S.set_mem i).inter (hA₁ i)), tsum_eq_single i] · intro j hij rw [hμn, ← nonpos_iff_eq_zero] - refine' le_trans ((singularPart_le _ _) _ ((S.set_mem i).inter (hA₁ i))) (le_of_eq _) + refine (singularPart_le _ _ _).trans_eq ?_ rw [restrict_apply ((S.set_mem i).inter (hA₁ i)), inter_comm, ← inter_assoc] have : Disjoint (S.set j) (S.set i) := h₂ hij rw [disjoint_iff_inter_eq_empty] at this diff --git a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean b/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean index df77778d4dec2..bc4d421bafd1c 100644 --- a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean +++ b/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean @@ -62,9 +62,8 @@ theorem withDensity_rnDeriv_eq (μ ν : Measure α) [HaveLebesgueDecomposition rw [← measure_add_measure_compl h_sing.measurableSet_nullSet] simp only [MutuallySingular.measure_nullSet, zero_add] refine le_antisymm ?_ (zero_le _) - refine (singularPart_le μ ν ?_ ?_).trans_eq ?_ - · exact h_sing.measurableSet_nullSet.compl - · exact h h_sing.measure_compl_nullSet + refine (singularPart_le μ ν ?_ ).trans_eq ?_ + exact h h_sing.measure_compl_nullSet #align measure_theory.measure.with_density_rn_deriv_eq MeasureTheory.Measure.withDensity_rnDeriv_eq variable {μ ν : Measure α} @@ -367,11 +366,12 @@ lemma set_integral_toReal_rnDeriv_le [SigmaFinite μ] {s : Set α} (hμs : μ s refine set_integral_mono_set ?_ ?_ (HasSubset.Subset.eventuallyLE (subset_toMeasurable _ _)) · exact integrableOn_toReal_rnDeriv hμt · exact ae_of_all _ (by simp) + _ = (withDensity ν (rnDeriv μ ν) t).toReal := set_integral_toReal_rnDeriv_eq_withDensity' ht_m _ ≤ (μ t).toReal := by - rw [set_integral_toReal_rnDeriv_eq_withDensity' ht_m, ENNReal.toReal_le_toReal _ hμt] - · exact withDensity_rnDeriv_le _ _ _ ht_m - · exact ((withDensity_rnDeriv_le _ _ _ ht_m).trans_lt hμt.lt_top).ne - _ = (μ s).toReal := by rw [← measure_toMeasurable s] + gcongr + · exact hμt + · apply withDensity_rnDeriv_le + _ = (μ s).toReal := by rw [measure_toMeasurable s] lemma set_integral_toReal_rnDeriv' [SigmaFinite μ] [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) {s : Set α} (hs : MeasurableSet s) : diff --git a/Mathlib/MeasureTheory/Function/SimpleFunc.lean b/Mathlib/MeasureTheory/Function/SimpleFunc.lean index 645a95fe034fa..2aa18b90a64f4 100644 --- a/Mathlib/MeasureTheory/Function/SimpleFunc.lean +++ b/Mathlib/MeasureTheory/Function/SimpleFunc.lean @@ -1112,10 +1112,9 @@ theorem lintegral_mono {f g : α →ₛ ℝ≥0∞} (hfg : f ≤ g) (hμν : μ f.lintegral μ ≤ g.lintegral ν := calc f.lintegral μ ≤ f.lintegral μ ⊔ g.lintegral μ := le_sup_left - _ ≤ (f ⊔ g).lintegral μ := (le_sup_lintegral _ _) + _ ≤ (f ⊔ g).lintegral μ := le_sup_lintegral _ _ _ = g.lintegral μ := by rw [sup_of_le_right hfg] - _ ≤ g.lintegral ν := - Finset.sum_le_sum fun y _ => ENNReal.mul_left_mono <| hμν _ (g.measurableSet_preimage _) + _ ≤ g.lintegral ν := Finset.sum_le_sum fun y _ => ENNReal.mul_left_mono <| hμν _ #align measure_theory.simple_func.lintegral_mono MeasureTheory.SimpleFunc.lintegral_mono /-- `SimpleFunc.lintegral` depends only on the measures of `f ⁻¹' {y}`. -/ diff --git a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean index 5329fddc0836b..1cef0da233f8d 100644 --- a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean +++ b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean @@ -482,13 +482,10 @@ theorem IntegrableAtFilter.inf_of_right (hl : IntegrableAtFilter f l μ) : @[simp] theorem IntegrableAtFilter.inf_ae_iff {l : Filter α} : IntegrableAtFilter f (l ⊓ μ.ae) μ ↔ IntegrableAtFilter f l μ := by - refine' ⟨_, fun h => h.filter_mono inf_le_left⟩ + refine ⟨?_, fun h ↦ h.filter_mono inf_le_left⟩ rintro ⟨s, ⟨t, ht, u, hu, rfl⟩, hf⟩ - refine' ⟨t, ht, _⟩ - refine' hf.integrable.mono_measure fun v hv => _ - simp only [Measure.restrict_apply hv] - refine' measure_mono_ae (mem_of_superset hu fun x hx => _) - exact fun ⟨hv, ht⟩ => ⟨hv, ⟨ht, hx⟩⟩ + refine ⟨t, ht, hf.congr_set_ae <| eventuallyEq_set.2 ?_⟩ + filter_upwards [hu] with x hx using (and_iff_left hx).symm #align measure_theory.integrable_at_filter.inf_ae_iff MeasureTheory.IntegrableAtFilter.inf_ae_iff alias ⟨IntegrableAtFilter.of_inf_ae, _⟩ := IntegrableAtFilter.inf_ae_iff diff --git a/Mathlib/MeasureTheory/Integral/Layercake.lean b/Mathlib/MeasureTheory/Integral/Layercake.lean index 2f4f36fff22a7..e627f0c7af04b 100644 --- a/Mathlib/MeasureTheory/Integral/Layercake.lean +++ b/Mathlib/MeasureTheory/Integral/Layercake.lean @@ -331,7 +331,7 @@ theorem lintegral_comp_eq_lintegral_meas_le_mul_of_measurable (μ : Measure α) refine lt_of_le_of_lt (measure_union_le _ _) ?_ rw [I, zero_add] apply lt_of_le_of_lt _ J - exact restrict_le_self _ (measurableSet_lt measurable_const f_mble) + exact restrict_le_self _ spanning := by apply eq_univ_iff_forall.2 (fun a ↦ ?_) rcases le_or_lt (f a) M with ha|ha diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean index 08e54d9527788..15bf4dfcabb33 100644 --- a/Mathlib/MeasureTheory/Integral/SetToL1.lean +++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean @@ -231,13 +231,12 @@ theorem smul [NormedField 𝕜] [NormedSpace 𝕜 β] (hT : DominatedFinMeasAddi theorem of_measure_le {μ' : Measure α} (h : μ ≤ μ') (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) : DominatedFinMeasAdditive μ' T C := by - have h' : ∀ s, MeasurableSet s → μ s = ∞ → μ' s = ∞ := by - intro s hs hμs; rw [eq_top_iff, ← hμs]; exact h s hs - refine' ⟨hT.1.of_eq_top_imp_eq_top h', fun s hs hμ's => _⟩ - have hμs : μ s < ∞ := (h s hs).trans_lt hμ's - refine' (hT.2 s hs hμs).trans (mul_le_mul le_rfl _ ENNReal.toReal_nonneg hC) - rw [toReal_le_toReal hμs.ne hμ's.ne] - exact h s hs + have h' : ∀ s, μ s = ∞ → μ' s = ∞ := fun s hs ↦ top_unique <| hs.symm.trans_le (h _) + refine ⟨hT.1.of_eq_top_imp_eq_top fun s _ ↦ h' s, fun s hs hμ's ↦ ?_⟩ + have hμs : μ s < ∞ := (h s).trans_lt hμ's + calc + ‖T s‖ ≤ C * (μ s).toReal := hT.2 s hs hμs + _ ≤ C * (μ' s).toReal := by gcongr; exacts [hμ's.ne, h _] #align measure_theory.dominated_fin_meas_additive.of_measure_le MeasureTheory.DominatedFinMeasAdditive.of_measure_le theorem add_measure_right {_ : MeasurableSpace α} (μ ν : Measure α) @@ -1610,7 +1609,7 @@ theorem setToFun_congr_measure_of_integrable {μ' : Measure α} (c' : ℝ≥0∞ apply hfμ.induction (P := fun f => setToFun μ T hT f = setToFun μ' T hT' f) · intro c s hs hμs have hμ's : μ' s ≠ ∞ := by - refine' ((hμ'_le s hs).trans_lt _).ne + refine ((hμ'_le s).trans_lt ?_).ne rw [Measure.smul_apply, smul_eq_mul] exact ENNReal.mul_lt_top hc' hμs.ne rw [setToFun_indicator_const hT hs hμs.ne, setToFun_indicator_const hT' hs hμ's] diff --git a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean index c9a6443c7078b..147b07c63e53d 100644 --- a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean +++ b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean @@ -387,8 +387,8 @@ theorem MeasureTheory.Measure.restrict_map_of_aemeasurable {f : α → δ} (hf : #align measure_theory.measure.restrict_map_of_ae_measurable MeasureTheory.Measure.restrict_map_of_aemeasurable theorem MeasureTheory.Measure.map_mono_of_aemeasurable {f : α → δ} (h : μ ≤ ν) - (hf : AEMeasurable f ν) : μ.map f ≤ ν.map f := fun s hs => by - simpa [hf, hs, hf.mono_measure h] using Measure.le_iff'.1 h (f ⁻¹' s) + (hf : AEMeasurable f ν) : μ.map f ≤ ν.map f := + le_iff.2 fun s hs ↦ by simpa [hf, hs, hf.mono_measure h] using h (f ⁻¹' s) #align measure_theory.measure.map_mono_of_ae_measurable MeasureTheory.Measure.map_mono_of_aemeasurable /-- If the `σ`-algebra of the codomain of a null measurable function is countably generated, diff --git a/Mathlib/MeasureTheory/Measure/Hausdorff.lean b/Mathlib/MeasureTheory/Measure/Hausdorff.lean index adbf011aa44e6..f115568e67953 100644 --- a/Mathlib/MeasureTheory/Measure/Hausdorff.lean +++ b/Mathlib/MeasureTheory/Measure/Hausdorff.lean @@ -478,8 +478,7 @@ variable [MeasurableSpace X] [BorelSpace X] /-- If `c ∉ {0, ∞}` and `m₁ d ≤ c * m₂ d` for `d < ε` for some `ε > 0` (we use `≤ᶠ[𝓝[≥] 0]` to state this), then `mkMetric m₁ hm₁ ≤ c • mkMetric m₂ hm₂`. -/ theorem mkMetric_mono_smul {m₁ m₂ : ℝ≥0∞ → ℝ≥0∞} {c : ℝ≥0∞} (hc : c ≠ ∞) (h0 : c ≠ 0) - (hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂) : (mkMetric m₁ : Measure X) ≤ c • mkMetric m₂ := by - intro s _ + (hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂) : (mkMetric m₁ : Measure X) ≤ c • mkMetric m₂ := fun s ↦ by rw [← OuterMeasure.coe_mkMetric, coe_smul, ← OuterMeasure.coe_mkMetric] exact OuterMeasure.mkMetric_mono_smul hc h0 hle s #align measure_theory.measure.mk_metric_mono_smul MeasureTheory.Measure.mkMetric_mono_smul diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean index 06c53526b7029..c77832dc1b49c 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean +++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean @@ -967,29 +967,25 @@ theorem measure_toMeasurable_add_inter_right {s t : Set α} (hs : MeasurableSet /-! ### The complete lattice of measures -/ -/-- Measures are partially ordered. - -The definition of less equal here is equivalent to the definition without the -measurable set condition, and this is shown by `Measure.le_iff'`. It is defined -this way since, to prove `μ ≤ ν`, we may simply `intros s hs` instead of rewriting followed -by `intros s hs`. -/ +/-- Measures are partially ordered. -/ instance instPartialOrder [MeasurableSpace α] : PartialOrder (Measure α) where - le m₁ m₂ := ∀ s, MeasurableSet s → m₁ s ≤ m₂ s - le_refl m s _hs := le_rfl - le_trans m₁ m₂ m₃ h₁ h₂ s hs := le_trans (h₁ s hs) (h₂ s hs) - le_antisymm m₁ m₂ h₁ h₂ := ext fun s hs => le_antisymm (h₁ s hs) (h₂ s hs) + le m₁ m₂ := ∀ s, m₁ s ≤ m₂ s + le_refl m s := le_rfl + le_trans m₁ m₂ m₃ h₁ h₂ s := le_trans (h₁ s) (h₂ s) + le_antisymm m₁ m₂ h₁ h₂ := ext fun s _ => le_antisymm (h₁ s) (h₂ s) #align measure_theory.measure.partial_order MeasureTheory.Measure.instPartialOrder -theorem le_iff : μ₁ ≤ μ₂ ↔ ∀ s, MeasurableSet s → μ₁ s ≤ μ₂ s := - Iff.rfl +theorem toOuterMeasure_le : μ₁.toOuterMeasure ≤ μ₂.toOuterMeasure ↔ μ₁ ≤ μ₂ := .rfl +#align measure_theory.measure.to_outer_measure_le MeasureTheory.Measure.toOuterMeasure_le + +theorem le_iff : μ₁ ≤ μ₂ ↔ ∀ s, MeasurableSet s → μ₁ s ≤ μ₂ s := by + rw [← toOuterMeasure_le, ← OuterMeasure.le_trim_iff, μ₂.trimmed] #align measure_theory.measure.le_iff MeasureTheory.Measure.le_iff -theorem toOuterMeasure_le : μ₁.toOuterMeasure ≤ μ₂.toOuterMeasure ↔ μ₁ ≤ μ₂ := by - rw [← μ₂.trimmed, OuterMeasure.le_trim_iff]; rfl -#align measure_theory.measure.to_outer_measure_le MeasureTheory.Measure.toOuterMeasure_le +theorem le_intro (h : ∀ s, MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s) : μ₁ ≤ μ₂ := + le_iff.2 fun s hs ↦ s.eq_empty_or_nonempty.elim (by rintro rfl; simp) (h s hs) -theorem le_iff' : μ₁ ≤ μ₂ ↔ ∀ s, μ₁ s ≤ μ₂ s := - toOuterMeasure_le.symm +theorem le_iff' : μ₁ ≤ μ₂ ↔ ∀ s, μ₁ s ≤ μ₂ s := .rfl #align measure_theory.measure.le_iff' MeasureTheory.Measure.le_iff' theorem lt_iff : μ < ν ↔ μ ≤ ν ∧ ∃ s, MeasurableSet s ∧ μ s < ν s := @@ -1003,13 +999,13 @@ theorem lt_iff' : μ < ν ↔ μ ≤ ν ∧ ∃ s, μ s < ν s := instance covariantAddLE [MeasurableSpace α] : CovariantClass (Measure α) (Measure α) (· + ·) (· ≤ ·) := - ⟨fun _ν _μ₁ _μ₂ hμ s hs => add_le_add_left (hμ s hs) _⟩ + ⟨fun _ν _μ₁ _μ₂ hμ s => add_le_add_left (hμ s) _⟩ #align measure_theory.measure.covariant_add_le MeasureTheory.Measure.covariantAddLE -protected theorem le_add_left (h : μ ≤ ν) : μ ≤ ν' + ν := fun s hs => le_add_left (h s hs) +protected theorem le_add_left (h : μ ≤ ν) : μ ≤ ν' + ν := fun s => le_add_left (h s) #align measure_theory.measure.le_add_left MeasureTheory.Measure.le_add_left -protected theorem le_add_right (h : μ ≤ ν) : μ ≤ ν + ν' := fun s hs => le_add_right (h s hs) +protected theorem le_add_right (h : μ ≤ ν) : μ ≤ ν + ν' := fun s => le_add_right (h s) #align measure_theory.measure.le_add_right MeasureTheory.Measure.le_add_right section sInf @@ -1041,17 +1037,16 @@ theorem sInf_apply (hs : MeasurableSet s) : sInf m s = sInf (toOuterMeasure '' m private theorem measure_sInf_le (h : μ ∈ m) : sInf m ≤ μ := have : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure := sInf_le (mem_image_of_mem _ h) - fun s hs => by rw [sInf_apply hs]; exact this s + le_iff.2 fun s hs => by rw [sInf_apply hs]; exact this s private theorem measure_le_sInf (h : ∀ μ' ∈ m, μ ≤ μ') : μ ≤ sInf m := have : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m) := le_sInf <| ball_image_of_ball fun μ hμ => toOuterMeasure_le.2 <| h _ hμ - fun s hs => by rw [sInf_apply hs]; exact this s + le_iff.2 fun s hs => by rw [sInf_apply hs]; exact this s instance instCompleteSemilatticeInf [MeasurableSpace α] : CompleteSemilatticeInf (Measure α) := { (by infer_instance : PartialOrder (Measure α)), - (by infer_instance : - InfSet (Measure α)) with + (by infer_instance : InfSet (Measure α)) with sInf_le := fun _s _a => measure_sInf_le le_sInf := fun _s _a => measure_le_sInf } #align measure_theory.measure.complete_semilattice_Inf MeasureTheory.Measure.instCompleteSemilatticeInf @@ -1069,7 +1064,7 @@ instance instCompleteLattice [MeasurableSpace α] : CompleteLattice (Measure α) -/ completeLatticeOfCompleteSemilatticeInf (Measure α) with bot := 0 - bot_le := fun _a _s _hs => bot_le } + bot_le := fun _a _s => bot_le } #align measure_theory.measure.complete_lattice MeasureTheory.Measure.instCompleteLattice end sInf @@ -1078,9 +1073,8 @@ end sInf theorem _root_.MeasureTheory.OuterMeasure.toMeasure_top [MeasurableSpace α] : (⊤ : OuterMeasure α).toMeasure (by rw [OuterMeasure.top_caratheodory]; exact le_top) = (⊤ : Measure α) := - top_unique fun s hs => by - rcases s.eq_empty_or_nonempty with h | h <;> - simp [h, toMeasure_apply ⊤ _ hs, OuterMeasure.top_apply] + top_unique <| le_intro fun s hs hne => by + simp [hne, toMeasure_apply ⊤ _ hs, OuterMeasure.top_apply] #align measure_theory.outer_measure.to_measure_top MeasureTheory.OuterMeasure.toMeasure_top @[simp] @@ -1109,7 +1103,7 @@ theorem nonpos_iff_eq_zero' : μ ≤ 0 ↔ μ = 0 := @[simp] theorem measure_univ_eq_zero : μ univ = 0 ↔ μ = 0 := - ⟨fun h => bot_unique fun s _ => (h ▸ measure_mono (subset_univ s) : μ s ≤ 0), fun h => + ⟨fun h => bot_unique fun s => (h ▸ measure_mono (subset_univ s) : μ s ≤ 0), fun h => h.symm ▸ rfl⟩ #align measure_theory.measure.measure_univ_eq_zero MeasureTheory.Measure.measure_univ_eq_zero @@ -1292,8 +1286,8 @@ theorem map_map {g : β → γ} {f : α → β} (hg : Measurable g) (hf : Measur #align measure_theory.measure.map_map MeasureTheory.Measure.map_map @[mono] -theorem map_mono {f : α → β} (h : μ ≤ ν) (hf : Measurable f) : μ.map f ≤ ν.map f := fun s hs => by - simp [hf.aemeasurable, hs, h _ (hf hs)] +theorem map_mono {f : α → β} (h : μ ≤ ν) (hf : Measurable f) : μ.map f ≤ ν.map f := + le_iff.2 fun s hs ↦ by simp [hf.aemeasurable, hs, h _] #align measure_theory.measure.map_mono MeasureTheory.Measure.map_mono /-- Even if `s` is not measurable, we can bound `map f μ s` from below. @@ -1467,8 +1461,8 @@ theorem sum_apply_of_countable [Countable ι] (f : ι → Measure α) (s : Set _ = ∑' i, f i t := sum_apply _ htm _ = ∑' i, f i s := by simp [ht] -theorem le_sum (μ : ι → Measure α) (i : ι) : μ i ≤ sum μ := fun s hs => by - simpa only [sum_apply μ hs] using ENNReal.le_tsum i +theorem le_sum (μ : ι → Measure α) (i : ι) : μ i ≤ sum μ := + le_iff.2 fun s hs ↦ by simpa only [sum_apply μ hs] using ENNReal.le_tsum i #align measure_theory.measure.le_sum MeasureTheory.Measure.le_sum @[simp] @@ -1481,7 +1475,6 @@ theorem sum_apply_eq_zero [Countable ι] {μ : ι → Measure α} {s : Set α} : calc sum μ s ≤ sum μ t := measure_mono hst _ = 0 := by simp [*] - #align measure_theory.measure.sum_apply_eq_zero MeasureTheory.Measure.sum_apply_eq_zero theorem sum_apply_eq_zero' {μ : ι → Measure α} {s : Set α} (hs : MeasurableSet s) : diff --git a/Mathlib/MeasureTheory/Measure/Restrict.lean b/Mathlib/MeasureTheory/Measure/Restrict.lean index 99bfdf8a59f9b..8e8b073a76f6e 100644 --- a/Mathlib/MeasureTheory/Measure/Restrict.lean +++ b/Mathlib/MeasureTheory/Measure/Restrict.lean @@ -78,13 +78,12 @@ theorem restrict_apply (ht : MeasurableSet t) : μ.restrict s t = μ (t ∩ s) : /-- Restriction of a measure to a subset is monotone both in set and in measure. -/ theorem restrict_mono' {_m0 : MeasurableSpace α} ⦃s s' : Set α⦄ ⦃μ ν : Measure α⦄ (hs : s ≤ᵐ[μ] s') - (hμν : μ ≤ ν) : μ.restrict s ≤ ν.restrict s' := fun t ht => - calc + (hμν : μ ≤ ν) : μ.restrict s ≤ ν.restrict s' := + Measure.le_iff.2 fun t ht => calc μ.restrict s t = μ (t ∩ s) := restrict_apply ht _ ≤ μ (t ∩ s') := (measure_mono_ae <| hs.mono fun _x hx ⟨hxt, hxs⟩ => ⟨hxt, hx hxs⟩) _ ≤ ν (t ∩ s') := (le_iff'.1 hμν (t ∩ s')) _ = ν.restrict s' t := (restrict_apply ht).symm - #align measure_theory.measure.restrict_mono' MeasureTheory.Measure.restrict_mono' /-- Restriction of a measure to a subset is monotone both in set and in measure. -/ @@ -117,8 +116,8 @@ theorem restrict_apply₀' (hs : NullMeasurableSet s μ) : μ.restrict s t = μ measure_congr ((ae_eq_refl t).inter hs.toMeasurable_ae_eq)] #align measure_theory.measure.restrict_apply₀' MeasureTheory.Measure.restrict_apply₀' -theorem restrict_le_self : μ.restrict s ≤ μ := fun t ht => - calc +theorem restrict_le_self : μ.restrict s ≤ μ := + Measure.le_iff.2 fun t ht => calc μ.restrict s t = μ (t ∩ s) := restrict_apply ht _ ≤ μ t := measure_mono <| inter_subset_left t s #align measure_theory.measure.restrict_le_self MeasureTheory.Measure.restrict_le_self @@ -299,10 +298,9 @@ theorem restrict_compl_add_restrict (hs : MeasurableSet s) : μ.restrict sᶜ + by rw [add_comm, restrict_add_restrict_compl hs] #align measure_theory.measure.restrict_compl_add_restrict MeasureTheory.Measure.restrict_compl_add_restrict -theorem restrict_union_le (s s' : Set α) : μ.restrict (s ∪ s') ≤ μ.restrict s + μ.restrict s' := by - intro t ht - suffices μ (t ∩ s ∪ t ∩ s') ≤ μ (t ∩ s) + μ (t ∩ s') by simpa [ht, inter_union_distrib_left] - apply measure_union_le +theorem restrict_union_le (s s' : Set α) : μ.restrict (s ∪ s') ≤ μ.restrict s + μ.restrict s' := + le_iff.2 fun t ht ↦ by + simpa [ht, inter_union_distrib_left] using measure_union_le (t ∩ s) (t ∩ s') #align measure_theory.measure.restrict_union_le MeasureTheory.Measure.restrict_union_le theorem restrict_iUnion_apply_ae [Countable ι] {s : ι → Set α} (hd : Pairwise (AEDisjoint μ on s)) @@ -385,7 +383,6 @@ theorem restrict_union_congr : simp only [restrict_apply, hu, hu.diff hm, hν, ← inter_comm t, inter_diff_assoc] _ = ν (US ∪ u ∩ t) := (measure_add_diff hm _) _ = ν (u ∩ s ∪ u ∩ t) := Eq.symm <| measure_union_congr_of_subset hsub hν.le Subset.rfl le_rfl - #align measure_theory.measure.restrict_union_congr MeasureTheory.Measure.restrict_union_congr theorem restrict_finset_biUnion_congr {s : Finset ι} {t : ι → Set α} : @@ -541,10 +538,8 @@ theorem restrict_iUnion [Countable ι] {s : ι → Set α} (hd : Pairwise (Disjo #align measure_theory.measure.restrict_Union MeasureTheory.Measure.restrict_iUnion theorem restrict_iUnion_le [Countable ι] {s : ι → Set α} : - μ.restrict (⋃ i, s i) ≤ sum fun i => μ.restrict (s i) := by - intro t ht - suffices μ (⋃ i, t ∩ s i) ≤ ∑' i, μ (t ∩ s i) by simpa [ht, inter_iUnion] - apply measure_iUnion_le + μ.restrict (⋃ i, s i) ≤ sum fun i => μ.restrict (s i) := + le_iff.2 fun t ht ↦ by simpa [ht, inter_iUnion] using measure_iUnion_le (t ∩ s ·) #align measure_theory.measure.restrict_Union_le MeasureTheory.Measure.restrict_iUnion_le end Measure diff --git a/Mathlib/MeasureTheory/Measure/Sub.lean b/Mathlib/MeasureTheory/Measure/Sub.lean index 7ba7df117e76d..1414f2b5f4213 100644 --- a/Mathlib/MeasureTheory/Measure/Sub.lean +++ b/Mathlib/MeasureTheory/Measure/Sub.lean @@ -73,16 +73,17 @@ theorem sub_apply [IsFiniteMeasure ν] (h₁ : MeasurableSet s) (h₂ : ν ≤ -- We begin by defining `measure_sub`, which will be equal to `(μ - ν)`. let measure_sub : Measure α := MeasureTheory.Measure.ofMeasurable (fun (t : Set α) (_ : MeasurableSet t) => μ t - ν t) (by simp) - (by - intro g h_meas h_disj; simp only; rw [ENNReal.tsum_sub] - repeat' rw [← MeasureTheory.measure_iUnion h_disj h_meas] - exacts [MeasureTheory.measure_ne_top _ _, fun i => h₂ _ (h_meas _)]) + (fun g h_meas h_disj ↦ by + simp only [measure_iUnion h_disj h_meas] + rw [ENNReal.tsum_sub _ (h₂ <| g ·)] + rw [← measure_iUnion h_disj h_meas] + apply measure_ne_top) -- Now, we demonstrate `μ - ν = measure_sub`, and apply it. have h_measure_sub_add : ν + measure_sub = μ := by ext1 t h_t_measurable_set simp only [Pi.add_apply, coe_add] rw [MeasureTheory.Measure.ofMeasurable_apply _ h_t_measurable_set, add_comm, - tsub_add_cancel_of_le (h₂ t h_t_measurable_set)] + tsub_add_cancel_of_le (h₂ t)] have h_measure_sub_eq : μ - ν = measure_sub := by rw [MeasureTheory.Measure.sub_def] apply le_antisymm @@ -98,7 +99,7 @@ theorem sub_apply [IsFiniteMeasure ν] (h₁ : MeasurableSet s) (h₂ : ν ≤ theorem sub_add_cancel_of_le [IsFiniteMeasure ν] (h₁ : ν ≤ μ) : μ - ν + ν = μ := by ext1 s h_s_meas - rw [add_apply, sub_apply h_s_meas h₁, tsub_add_cancel_of_le (h₁ s h_s_meas)] + rw [add_apply, sub_apply h_s_meas h₁, tsub_add_cancel_of_le (h₁ s)] #align measure_theory.measure.sub_add_cancel_of_le MeasureTheory.Measure.sub_add_cancel_of_le theorem restrict_sub_eq_restrict_sub_restrict (h_meas_s : MeasurableSet s) : @@ -120,7 +121,7 @@ theorem restrict_sub_eq_restrict_sub_restrict (h_meas_s : MeasurableSet s) : apply le_add_right _ rw [← restrict_eq_self μ (inter_subset_right _ _), ← restrict_eq_self ν (inter_subset_right _ _)] - apply h_ν'_in _ (h_meas_t.inter h_meas_s) + apply h_ν'_in · rw [add_apply, restrict_apply (h_meas_t.diff h_meas_s), diff_eq, inter_assoc, inter_self, ← add_apply] have h_mu_le_add_top : μ ≤ ν' + ν + ⊤ := by simp only [add_top, le_top] diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/Mathlib/MeasureTheory/Measure/Typeclasses.lean index e3c8255bb933a..265bf41c4b65e 100644 --- a/Mathlib/MeasureTheory/Measure/Typeclasses.lean +++ b/Mathlib/MeasureTheory/Measure/Typeclasses.lean @@ -126,7 +126,7 @@ instance isFiniteMeasureSMulOfNNRealTower {R} [SMul R ℝ≥0] [SMul R ℝ≥0 #align measure_theory.is_finite_measure_smul_of_nnreal_tower MeasureTheory.isFiniteMeasureSMulOfNNRealTower theorem isFiniteMeasure_of_le (μ : Measure α) [IsFiniteMeasure μ] (h : ν ≤ μ) : IsFiniteMeasure ν := - { measure_univ_lt_top := lt_of_le_of_lt (h Set.univ MeasurableSet.univ) (measure_lt_top _ _) } + { measure_univ_lt_top := (h Set.univ).trans_lt (measure_lt_top _ _) } #align measure_theory.is_finite_measure_of_le MeasureTheory.isFiniteMeasure_of_le @[instance] @@ -154,7 +154,7 @@ theorem measureUnivNNReal_pos [IsFiniteMeasure μ] (hμ : μ ≠ 0) : 0 < measur /-- `le_of_add_le_add_left` is normally applicable to `OrderedCancelAddCommMonoid`, but it holds for measures with the additional assumption that μ is finite. -/ theorem Measure.le_of_add_le_add_left [IsFiniteMeasure μ] (A2 : μ + ν₁ ≤ μ + ν₂) : ν₁ ≤ ν₂ := - fun S B1 => ENNReal.le_of_add_le_add_left (MeasureTheory.measure_ne_top μ S) (A2 S B1) + fun S => ENNReal.le_of_add_le_add_left (MeasureTheory.measure_ne_top μ S) (A2 S) #align measure_theory.measure.le_of_add_le_add_left MeasureTheory.Measure.le_of_add_le_add_left theorem summable_measure_toReal [hμ : IsFiniteMeasure μ] {f : ℕ → Set α} diff --git a/Mathlib/MeasureTheory/Measure/WithDensity.lean b/Mathlib/MeasureTheory/Measure/WithDensity.lean index b924e68e0b56e..7cec4f50fb32a 100644 --- a/Mathlib/MeasureTheory/Measure/WithDensity.lean +++ b/Mathlib/MeasureTheory/Measure/WithDensity.lean @@ -89,7 +89,7 @@ theorem withDensity_congr_ae {f g : α → ℝ≥0∞} (h : f =ᵐ[μ] g) : lemma withDensity_mono {f g : α → ℝ≥0∞} (hfg : f ≤ᵐ[μ] g) : μ.withDensity f ≤ μ.withDensity g := by - intro s hs + refine le_iff.2 fun s hs ↦ ?_ rw [withDensity_apply _ hs, withDensity_apply _ hs] refine set_lintegral_mono_ae' hs ?_ filter_upwards [hfg] with x h_le using fun _ ↦ h_le diff --git a/Mathlib/Probability/Density.lean b/Mathlib/Probability/Density.lean index 8e9b600c5301b..1a49c05de6d13 100644 --- a/Mathlib/Probability/Density.lean +++ b/Mathlib/Probability/Density.lean @@ -175,10 +175,10 @@ theorem withDensity_pdf_le_map {_ : MeasurableSpace Ω} (X : Ω → E) (ℙ : Me withDensity_rnDeriv_le _ _ theorem set_lintegral_pdf_le_map {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) - (μ : Measure E := by volume_tac) {s : Set E} (hs : MeasurableSet s) : + (μ : Measure E := by volume_tac) (s : Set E) : ∫⁻ x in s, pdf X ℙ μ x ∂μ ≤ map X ℙ s := by apply (withDensity_apply_le _ s).trans - exact withDensity_pdf_le_map _ _ _ s hs + exact withDensity_pdf_le_map _ _ _ s theorem map_eq_withDensity_pdf {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) [hX : HasPDF X ℙ μ] : diff --git a/Mathlib/Probability/Kernel/CondCdf.lean b/Mathlib/Probability/Kernel/CondCdf.lean index ab86bf1556065..4777d3807b596 100644 --- a/Mathlib/Probability/Kernel/CondCdf.lean +++ b/Mathlib/Probability/Kernel/CondCdf.lean @@ -89,14 +89,14 @@ theorem IicSnd_univ (r : ℝ) : ρ.IicSnd r univ = ρ (univ ×ˢ Iic r) := #align measure_theory.measure.Iic_snd_univ MeasureTheory.Measure.IicSnd_univ theorem IicSnd_mono {r r' : ℝ} (h_le : r ≤ r') : ρ.IicSnd r ≤ ρ.IicSnd r' := by - intro s hs + refine Measure.le_iff.2 fun s hs ↦ ?_ simp_rw [IicSnd_apply ρ _ hs] refine' measure_mono (prod_subset_prod_iff.mpr (Or.inl ⟨subset_rfl, Iic_subset_Iic.mpr _⟩)) exact mod_cast h_le #align measure_theory.measure.Iic_snd_mono MeasureTheory.Measure.IicSnd_mono theorem IicSnd_le_fst (r : ℝ) : ρ.IicSnd r ≤ ρ.fst := by - intro s hs + refine Measure.le_iff.2 fun s hs ↦ ?_ simp_rw [fst_apply hs, IicSnd_apply ρ r hs] exact measure_mono (prod_subset_preimage_fst _ _) #align measure_theory.measure.Iic_snd_le_fst MeasureTheory.Measure.IicSnd_le_fst @@ -219,8 +219,7 @@ theorem monotone_preCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] : ae_le_of_forall_set_lintegral_le_of_sigmaFinite measurable_preCDF measurable_preCDF fun s hs _ => _ rw [set_lintegral_preCDF_fst ρ r hs, set_lintegral_preCDF_fst ρ r' hs] - refine' Measure.IicSnd_mono ρ _ s hs - exact mod_cast hrr' + exact Measure.IicSnd_mono ρ (mod_cast hrr') s #align probability_theory.monotone_pre_cdf ProbabilityTheory.monotone_preCDF theorem set_lintegral_iInf_gt_preCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (t : ℚ) {s : Set α} @@ -251,7 +250,7 @@ theorem preCDF_le_one (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] : fun s hs _ => _ rw [set_lintegral_preCDF_fst ρ r hs] simp only [Pi.one_apply, lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter] - exact Measure.IicSnd_le_fst ρ r s hs + exact Measure.IicSnd_le_fst ρ r s #align probability_theory.pre_cdf_le_one ProbabilityTheory.preCDF_le_one theorem tendsto_lintegral_preCDF_atTop (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] : From 7a17e9debe6c7b8a494caada80faa5781fb73d2a Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 21 Feb 2024 16:46:14 +0000 Subject: [PATCH 17/20] chore: add some `fun_prop` attributes for continuity (#10769) --- Mathlib/Topology/Algebra/Monoid.lean | 2 +- Mathlib/Topology/Algebra/Polynomial.lean | 16 +++++++++++----- Mathlib/Topology/ContinuousOn.lean | 7 +++++++ 3 files changed, 19 insertions(+), 6 deletions(-) diff --git a/Mathlib/Topology/Algebra/Monoid.lean b/Mathlib/Topology/Algebra/Monoid.lean index 2c2a7971adeb7..d4c94464391d1 100644 --- a/Mathlib/Topology/Algebra/Monoid.lean +++ b/Mathlib/Topology/Algebra/Monoid.lean @@ -28,7 +28,7 @@ open Classical Topology BigOperators Pointwise variable {ι α M N X : Type*} [TopologicalSpace X] -@[to_additive (attr := continuity)] +@[to_additive (attr := continuity, fun_prop)] theorem continuous_one [TopologicalSpace M] [One M] : Continuous (1 : X → M) := @continuous_const _ _ _ _ 1 #align continuous_one continuous_one diff --git a/Mathlib/Topology/Algebra/Polynomial.lean b/Mathlib/Topology/Algebra/Polynomial.lean index 9d5a18d39ddd9..36e76fdc7d47c 100644 --- a/Mathlib/Topology/Algebra/Polynomial.lean +++ b/Mathlib/Topology/Algebra/Polynomial.lean @@ -23,8 +23,8 @@ In this file we prove the following lemmas. * `Polynomial.continuous`: `Polynomial.eval` defines a continuous functions; we also prove convenience lemmas `Polynomial.continuousAt`, `Polynomial.continuousWithinAt`, `Polynomial.continuousOn`. -* `Polynomial.tendsto_norm_atTop`: `fun x ↦‖Polynomial.eval (z x) p‖` tends to infinity - provided that `fun x ↦ ‖z x‖` tends to infinity and `0 < degree p`; +* `Polynomial.tendsto_norm_atTop`: `fun x ↦ ‖Polynomial.eval (z x) p‖` tends to infinity provided + that `fun x ↦ ‖z x‖` tends to infinity and `0 < degree p`; * `Polynomial.tendsto_abv_eval₂_atTop`, `Polynomial.tendsto_abv_atTop`, `Polynomial.tendsto_abv_aeval_atTop`: a few versions of the previous statement for `IsAbsoluteValue abv` instead of norm. @@ -45,26 +45,29 @@ section TopologicalSemiring variable {R S : Type*} [Semiring R] [TopologicalSpace R] [TopologicalSemiring R] (p : R[X]) -@[continuity] +@[continuity, fun_prop] protected theorem continuous_eval₂ [Semiring S] (p : S[X]) (f : S →+* R) : Continuous fun x => p.eval₂ f x := by simp only [eval₂_eq_sum, Finsupp.sum] exact continuous_finset_sum _ fun c _ => continuous_const.mul (continuous_pow _) #align polynomial.continuous_eval₂ Polynomial.continuous_eval₂ -@[continuity] +@[continuity, fun_prop] protected theorem continuous : Continuous fun x => p.eval x := p.continuous_eval₂ _ #align polynomial.continuous Polynomial.continuous +@[fun_prop] protected theorem continuousAt {a : R} : ContinuousAt (fun x => p.eval x) a := p.continuous.continuousAt #align polynomial.continuous_at Polynomial.continuousAt +@[fun_prop] protected theorem continuousWithinAt {s a} : ContinuousWithinAt (fun x => p.eval x) s a := p.continuous.continuousWithinAt #align polynomial.continuous_within_at Polynomial.continuousWithinAt +@[fun_prop] protected theorem continuousOn {s} : ContinuousOn (fun x => p.eval x) s := p.continuous.continuousOn #align polynomial.continuous_on Polynomial.continuousOn @@ -76,20 +79,23 @@ section TopologicalAlgebra variable {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] [TopologicalSemiring A] (p : R[X]) -@[continuity] +@[continuity, fun_prop] protected theorem continuous_aeval : Continuous fun x : A => aeval x p := p.continuous_eval₂ _ #align polynomial.continuous_aeval Polynomial.continuous_aeval +@[fun_prop] protected theorem continuousAt_aeval {a : A} : ContinuousAt (fun x : A => aeval x p) a := p.continuous_aeval.continuousAt #align polynomial.continuous_at_aeval Polynomial.continuousAt_aeval +@[fun_prop] protected theorem continuousWithinAt_aeval {s a} : ContinuousWithinAt (fun x : A => aeval x p) s a := p.continuous_aeval.continuousWithinAt #align polynomial.continuous_within_at_aeval Polynomial.continuousWithinAt_aeval +@[fun_prop] protected theorem continuousOn_aeval {s} : ContinuousOn (fun x : A => aeval x p) s := p.continuous_aeval.continuousOn #align polynomial.continuous_on_aeval Polynomial.continuousOn_aeval diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean index 2cec92fe0d0e4..d518acb4bff2d 100644 --- a/Mathlib/Topology/ContinuousOn.lean +++ b/Mathlib/Topology/ContinuousOn.lean @@ -978,6 +978,13 @@ theorem Continuous.comp_continuousOn {g : β → γ} {f : α → β} {s : Set α hg.continuousOn.comp hf (mapsTo_univ _ _) #align continuous.comp_continuous_on Continuous.comp_continuousOn +@[fun_prop] +theorem Continuous.comp_continuousOn' + {α β γ : Type*} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} + {f : α → β} {s : Set α} (hg : Continuous g) (hf : ContinuousOn f s) : + ContinuousOn (fun x ↦ g (f x)) s := + hg.comp_continuousOn hf + theorem ContinuousOn.comp_continuous {g : β → γ} {f : α → β} {s : Set β} (hg : ContinuousOn g s) (hf : Continuous f) (hs : ∀ x, f x ∈ s) : Continuous (g ∘ f) := by rw [continuous_iff_continuousOn_univ] at * From ba55c689b2a339601a15bfd0e38207b446f8ef15 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 21 Feb 2024 16:46:15 +0000 Subject: [PATCH 18/20] chore: classify `previously simp` porting notes (#10789) Classifies by adding issue number (#10745) to porting note claiming anything semantically equivalent to `was simp`. Related merged PR: #10746. --- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean index 1b49b14ceb28d..bbd25a4174499 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean @@ -500,7 +500,7 @@ protected def unit' : 𝟭 (ModuleCat S) ⟶ restrictScalars f ⋙ coextendScala app Y := app' f Y naturality Y Y' g := LinearMap.ext fun y : Y => LinearMap.ext fun s : S => by - -- Porting note: previously simp [CoextendScalars.map_apply] + -- Porting note (#10745): previously simp [CoextendScalars.map_apply] simp only [ModuleCat.coe_comp, Functor.id_map, Functor.id_obj, Functor.comp_obj, Functor.comp_map] rw [coe_comp, coe_comp, Function.comp, Function.comp] @@ -545,12 +545,12 @@ def restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] { toFun := RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁,u₂,v} f invFun := RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁,u₂,v} f left_inv := fun g => LinearMap.ext fun x : X => by - -- Porting note: once just simp + -- Porting note (#10745): once just simp rw [RestrictionCoextensionAdj.HomEquiv.toRestriction_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, RestrictionCoextensionAdj.HomEquiv.fromRestriction_apply_apply, one_smul] right_inv := fun g => LinearMap.ext fun x => LinearMap.ext fun s : S => by - -- Porting note: once just simp + -- Porting note (#10745): once just simp rw [RestrictionCoextensionAdj.HomEquiv.fromRestriction_apply_apply, RestrictionCoextensionAdj.HomEquiv.toRestriction_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.map_smulₛₗ, RingHom.id_apply, @@ -559,7 +559,7 @@ def restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] counit := RestrictionCoextensionAdj.counit'.{u₁,u₂,v} f homEquiv_unit := LinearMap.ext fun y => rfl homEquiv_counit := fun {X Y g} => LinearMap.ext <| by - -- Porting note: previously simp [RestrictionCoextensionAdj.counit'] + -- Porting note (#10745): previously simp [RestrictionCoextensionAdj.counit'] intro x; dsimp rw [coe_comp, Function.comp] change _ = (((restrictScalars f).map g) x).toFun (1 : S) From 10e929a254938156c046ce223d819cb07d0f5faf Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 21 Feb 2024 16:46:16 +0000 Subject: [PATCH 19/20] chore: classify `added lemma` porting notes (#10791) Classifies by adding number (#10756) to porting notes claiming `added lemma`. --- Mathlib/Algebra/Category/GroupCat/Basic.lean | 12 ++++++------ Mathlib/Algebra/Category/GroupWithZeroCat.lean | 2 +- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 2 +- Mathlib/Algebra/Category/MonCat/Basic.lean | 12 ++++++------ Mathlib/Algebra/Category/Ring/Basic.lean | 8 ++++---- 5 files changed, 18 insertions(+), 18 deletions(-) diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean index 9fa9129b32d38..fa38ddc536cd4 100644 --- a/Mathlib/Algebra/Category/GroupCat/Basic.lean +++ b/Mathlib/Algebra/Category/GroupCat/Basic.lean @@ -68,18 +68,18 @@ instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where instance instFunLike (X Y : GroupCat) : FunLike (X ⟶ Y) X Y := show FunLike (X →* Y) X Y from inferInstance --- porting note: added +-- porting note (#10756): added lemma @[to_additive (attr := simp)] lemma coe_id {X : GroupCat} : (𝟙 X : X → X) = id := rfl --- porting note: added +-- porting note (#10756): added lemma @[to_additive (attr := simp)] lemma coe_comp {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl @[to_additive] lemma comp_def {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : f ≫ g = g.comp f := rfl --- porting note: added +-- porting note (#10756): added lemma @[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupCat).map f = (f : X → Y) := rfl @[to_additive (attr := ext)] @@ -217,18 +217,18 @@ instance {X Y : CommGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where instance instFunLike (X Y : CommGroupCat) : FunLike (X ⟶ Y) X Y := show FunLike (X →* Y) X Y from inferInstance --- porting note: added +-- porting note (#10756): added lemma @[to_additive (attr := simp)] lemma coe_id {X : CommGroupCat} : (𝟙 X : X → X) = id := rfl --- porting note: added +-- porting note (#10756): added lemma @[to_additive (attr := simp)] lemma coe_comp {X Y Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl @[to_additive] lemma comp_def {X Y Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : f ≫ g = g.comp f := rfl --- porting note: added +-- porting note (#10756): added lemma @[to_additive (attr := simp)] lemma forget_map {X Y : CommGroupCat} (f : X ⟶ Y) : (forget CommGroupCat).map f = (f : X → Y) := diff --git a/Mathlib/Algebra/Category/GroupWithZeroCat.lean b/Mathlib/Algebra/Category/GroupWithZeroCat.lean index 0bd4d7f3d4d1f..58d13d3af3dde 100644 --- a/Mathlib/Algebra/Category/GroupWithZeroCat.lean +++ b/Mathlib/Algebra/Category/GroupWithZeroCat.lean @@ -72,7 +72,7 @@ instance groupWithZeroConcreteCategory : ConcreteCategory GroupWithZeroCat where map := fun f => f.toFun } forget_faithful := ⟨fun h => DFunLike.coe_injective h⟩ --- porting note: added +-- porting note (#10756): added lemma @[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupWithZeroCat).map f = f := rfl instance hasForgetToBipointed : HasForget₂ GroupWithZeroCat Bipointed where forget₂ := diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index 8bec016448dfc..a44fa1e103163 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -227,7 +227,7 @@ theorem comp_def (f : M ⟶ N) (g : N ⟶ U) : f ≫ g = g.comp f := rfl #align Module.comp_def ModuleCat.comp_def --- porting note: added +-- porting note (#10756): added lemma @[simp] lemma forget_map (f : M ⟶ N) : (forget (ModuleCat R)).map f = (f : M → N) := rfl end ModuleCat diff --git a/Mathlib/Algebra/Category/MonCat/Basic.lean b/Mathlib/Algebra/Category/MonCat/Basic.lean index 57728f7d8c7dd..74d109cc7f3aa 100644 --- a/Mathlib/Algebra/Category/MonCat/Basic.lean +++ b/Mathlib/Algebra/Category/MonCat/Basic.lean @@ -93,15 +93,15 @@ instance instFunLike (X Y : MonCat) : FunLike (X ⟶ Y) X Y := instance instMonoidHomClass (X Y : MonCat) : MonoidHomClass (X ⟶ Y) X Y := inferInstanceAs <| MonoidHomClass (X →* Y) X Y --- porting note: added +-- porting note (#10756): added lemma @[to_additive (attr := simp)] lemma coe_id {X : MonCat} : (𝟙 X : X → X) = id := rfl --- porting note: added +-- porting note (#10756): added lemma @[to_additive (attr := simp)] lemma coe_comp {X Y Z : MonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl --- porting note: added +-- porting note (#10756): added lemma @[to_additive (attr := simp)] lemma forget_map (f : X ⟶ Y) : (forget MonCat).map f = f := rfl @[to_additive (attr := ext)] @@ -215,15 +215,15 @@ instance {X Y : CommMonCat} : CoeFun (X ⟶ Y) fun _ => X → Y where instance instFunLike (X Y : CommMonCat) : FunLike (X ⟶ Y) X Y := show FunLike (X →* Y) X Y by infer_instance --- porting note: added +-- porting note (#10756): added lemma @[to_additive (attr := simp)] lemma coe_id {X : CommMonCat} : (𝟙 X : X → X) = id := rfl --- porting note: added +-- porting note (#10756): added lemma @[to_additive (attr := simp)] lemma coe_comp {X Y Z : CommMonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl --- porting note: added +-- porting note (#10756): added lemma @[to_additive (attr := simp)] lemma forget_map {X Y : CommMonCat} (f : X ⟶ Y) : (forget CommMonCat).map f = (f : X → Y) := diff --git a/Mathlib/Algebra/Category/Ring/Basic.lean b/Mathlib/Algebra/Category/Ring/Basic.lean index db4eef560cf50..bdf043b5ae9e7 100644 --- a/Mathlib/Algebra/Category/Ring/Basic.lean +++ b/Mathlib/Algebra/Category/Ring/Basic.lean @@ -91,7 +91,7 @@ lemma coe_id {X : SemiRingCat} : (𝟙 X : X → X) = id := rfl -- Porting note (#10756): added lemma lemma coe_comp {X Y Z : SemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl --- porting note: added +-- porting note (#10756): added lemma @[simp] lemma forget_map (f : X ⟶ Y) : (forget SemiRingCat).map f = (f : X → Y) := rfl lemma ext {X Y : SemiRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := @@ -215,7 +215,7 @@ lemma coe_id {X : RingCat} : (𝟙 X : X → X) = id := rfl -- Porting note (#10756): added lemma lemma coe_comp {X Y Z : RingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl --- porting note: added +-- porting note (#10756): added lemma @[simp] lemma forget_map (f : X ⟶ Y) : (forget RingCat).map f = (f : X → Y) := rfl lemma ext {X Y : RingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := @@ -321,7 +321,7 @@ lemma coe_id {X : CommSemiRingCat} : (𝟙 X : X → X) = id := rfl -- Porting note (#10756): added lemma lemma coe_comp {X Y Z : CommSemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl --- porting note: added +-- porting note (#10756): added lemma @[simp] lemma forget_map (f : X ⟶ Y) : (forget CommSemiRingCat).map f = (f : X → Y) := rfl lemma ext {X Y : CommSemiRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := @@ -441,7 +441,7 @@ lemma coe_id {X : CommRingCat} : (𝟙 X : X → X) = id := rfl -- Porting note (#10756): added lemma lemma coe_comp {X Y Z : CommRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl --- porting note: added +-- porting note (#10756): added lemma @[simp] lemma forget_map (f : X ⟶ Y) : (forget CommRingCat).map f = (f : X → Y) := rfl lemma ext {X Y : CommRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g := From 65d9c6c4d7f2bad2aac31291c2a7dccee4ea8a35 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 21 Feb 2024 16:46:17 +0000 Subject: [PATCH 20/20] feat: add `tendsto_atBot_atTop_of_antitone` (#10794) --- Mathlib/Order/Filter/AtTopBot.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Mathlib/Order/Filter/AtTopBot.lean b/Mathlib/Order/Filter/AtTopBot.lean index 8814f430c52d2..b1192943448af 100644 --- a/Mathlib/Order/Filter/AtTopBot.lean +++ b/Mathlib/Order/Filter/AtTopBot.lean @@ -1371,24 +1371,40 @@ theorem tendsto_atTop_atTop_of_monotone [Preorder α] [Preorder β] {f : α → mem_of_superset (mem_atTop a) fun _a' ha' => le_trans ha (hf ha') #align filter.tendsto_at_top_at_top_of_monotone Filter.tendsto_atTop_atTop_of_monotone +theorem tendsto_atTop_atBot_of_antitone [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) + (h : ∀ b, ∃ a, f a ≤ b) : Tendsto f atTop atBot := + @tendsto_atTop_atTop_of_monotone _ βᵒᵈ _ _ _ hf h + theorem tendsto_atBot_atBot_of_monotone [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (h : ∀ b, ∃ a, f a ≤ b) : Tendsto f atBot atBot := tendsto_iInf.2 fun b => tendsto_principal.2 <| let ⟨a, ha⟩ := h b; mem_of_superset (mem_atBot a) fun _a' ha' => le_trans (hf ha') ha #align filter.tendsto_at_bot_at_bot_of_monotone Filter.tendsto_atBot_atBot_of_monotone +theorem tendsto_atBot_atTop_of_antitone [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) + (h : ∀ b, ∃ a, b ≤ f a) : Tendsto f atBot atTop := + @tendsto_atBot_atBot_of_monotone _ βᵒᵈ _ _ _ hf h + theorem tendsto_atTop_atTop_iff_of_monotone [Nonempty α] [SemilatticeSup α] [Preorder β] {f : α → β} (hf : Monotone f) : Tendsto f atTop atTop ↔ ∀ b : β, ∃ a : α, b ≤ f a := tendsto_atTop_atTop.trans <| forall_congr' fun _ => exists_congr fun a => ⟨fun h => h a (le_refl a), fun h _a' ha' => le_trans h <| hf ha'⟩ #align filter.tendsto_at_top_at_top_iff_of_monotone Filter.tendsto_atTop_atTop_iff_of_monotone +theorem tendsto_atTop_atBot_iff_of_antitone [Nonempty α] [SemilatticeSup α] [Preorder β] {f : α → β} + (hf : Antitone f) : Tendsto f atTop atBot ↔ ∀ b : β, ∃ a : α, f a ≤ b := + @tendsto_atTop_atTop_iff_of_monotone _ βᵒᵈ _ _ _ _ hf + theorem tendsto_atBot_atBot_iff_of_monotone [Nonempty α] [SemilatticeInf α] [Preorder β] {f : α → β} (hf : Monotone f) : Tendsto f atBot atBot ↔ ∀ b : β, ∃ a : α, f a ≤ b := tendsto_atBot_atBot.trans <| forall_congr' fun _ => exists_congr fun a => ⟨fun h => h a (le_refl a), fun h _a' ha' => le_trans (hf ha') h⟩ #align filter.tendsto_at_bot_at_bot_iff_of_monotone Filter.tendsto_atBot_atBot_iff_of_monotone +theorem tendsto_atBot_atTop_iff_of_antitone [Nonempty α] [SemilatticeInf α] [Preorder β] {f : α → β} + (hf : Antitone f) : Tendsto f atBot atTop ↔ ∀ b : β, ∃ a : α, b ≤ f a := + @tendsto_atBot_atBot_iff_of_monotone _ βᵒᵈ _ _ _ _ hf + alias _root_.Monotone.tendsto_atTop_atTop := tendsto_atTop_atTop_of_monotone #align monotone.tendsto_at_top_at_top Monotone.tendsto_atTop_atTop