From b5440da9ef438cddc9912f2552504106a46d1124 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 9 Aug 2024 00:58:22 +0000 Subject: [PATCH] chore: backports for leanprover/lean4#4814 (part 33) (#15605) --- .../Algebra/Homology/DerivedCategory/Ext.lean | 23 +++-- Mathlib/Algebra/Lie/CartanExists.lean | 6 +- Mathlib/Algebra/Lie/Killing.lean | 9 +- Mathlib/Algebra/Lie/Weights/Linear.lean | 9 +- .../ContinuousFunctionalCalculus/Unitary.lean | 4 +- .../Analysis/Calculus/FDeriv/Measurable.lean | 5 +- Mathlib/Analysis/Fourier/AddCircle.lean | 2 +- .../NormedSpace/HahnBanach/Separation.lean | 13 ++- .../Combinatorics/SimpleGraph/LapMatrix.lean | 14 +-- .../Manifold/ContMDiff/NormedSpace.lean | 92 ++++++++++--------- .../Geometry/Manifold/ContMDiff/Product.lean | 16 +--- .../LinearAlgebra/Matrix/SchurComplement.lean | 4 +- .../Constructions/BorelSpace/Real.lean | 3 +- .../Constructions/Polish/Basic.lean | 10 +- .../Function/ContinuousMapDense.lean | 19 ++-- Mathlib/MeasureTheory/Group/Integral.lean | 2 +- Mathlib/MeasureTheory/Integral/Bochner.lean | 5 +- .../Integral/BoundedContinuousFunction.lean | 18 ++-- .../Measure/Haar/InnerProductSpace.lean | 44 +++++---- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 15 +-- .../DedekindDomain/IntegralClosure.lean | 7 +- Mathlib/RingTheory/Discriminant.lean | 2 +- Mathlib/RingTheory/Kaehler/Basic.lean | 5 + Mathlib/RingTheory/WittVector/MulCoeff.lean | 3 +- Mathlib/Topology/Algebra/Algebra.lean | 3 + 25 files changed, 182 insertions(+), 151 deletions(-) diff --git a/Mathlib/Algebra/Homology/DerivedCategory/Ext.lean b/Mathlib/Algebra/Homology/DerivedCategory/Ext.lean index 6245ca808b6f0..15e28dcd178de 100644 --- a/Mathlib/Algebra/Homology/DerivedCategory/Ext.lean +++ b/Mathlib/Algebra/Homology/DerivedCategory/Ext.lean @@ -238,18 +238,7 @@ lemma mk₀_zero : mk₀ (0 : X ⟶ Y) = 0 := by section -variable [HasDerivedCategory.{w'} C] - -variable (X Y n) in -@[simp] -lemma zero_hom : (0 : Ext X Y n).hom = 0 := by - let β : Ext 0 Y n := 0 - have hβ : β.hom = 0 := by apply (Functor.map_isZero _ (isZero_zero C)).eq_of_src - have : (0 : Ext X Y n) = (0 : Ext X 0 0).comp β (zero_add n) := by simp [β] - rw [this, comp_hom, hβ, ShiftedHom.comp_zero] - -attribute [local instance] preservesBinaryBiproductsOfPreservesBiproducts - +attribute [local instance] preservesBinaryBiproductsOfPreservesBiproducts in lemma biprod_ext {X₁ X₂ : C} {α β : Ext (X₁ ⊞ X₂) Y n} (h₁ : (mk₀ biprod.inl).comp α (zero_add n) = (mk₀ biprod.inl).comp β (zero_add n)) (h₂ : (mk₀ biprod.inr).comp α (zero_add n) = (mk₀ biprod.inr).comp β (zero_add n)) : @@ -262,6 +251,16 @@ lemma biprod_ext {X₁ X₂ : C} {α β : Ext (X₁ ⊞ X₂) Y n} (BinaryBiproduct.isBilimit X₁ X₂)).isColimit all_goals assumption +variable [HasDerivedCategory.{w'} C] + +variable (X Y n) in +@[simp] +lemma zero_hom : (0 : Ext X Y n).hom = 0 := by + let β : Ext 0 Y n := 0 + have hβ : β.hom = 0 := by apply (Functor.map_isZero _ (isZero_zero C)).eq_of_src + have : (0 : Ext X Y n) = (0 : Ext X 0 0).comp β (zero_add n) := by simp [β] + rw [this, comp_hom, hβ, ShiftedHom.comp_zero] + @[simp] lemma add_hom (α β : Ext X Y n) : (α + β).hom = α.hom + β.hom := by let α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α (zero_add n) diff --git a/Mathlib/Algebra/Lie/CartanExists.lean b/Mathlib/Algebra/Lie/CartanExists.lean index 77a85c041d18b..25735e2642f2f 100644 --- a/Mathlib/Algebra/Lie/CartanExists.lean +++ b/Mathlib/Algebra/Lie/CartanExists.lean @@ -32,7 +32,7 @@ namespace LieAlgebra section CommRing variable {K R L M : Type*} -variable [Field K] [CommRing R] [Nontrivial R] +variable [Field K] [CommRing R] variable [LieRing L] [LieAlgebra K L] [LieAlgebra R L] variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] variable [Module.Finite K L] @@ -83,7 +83,7 @@ def lieCharpoly : Polynomial R[X] := lemma lieCharpoly_monic : (lieCharpoly R M x y).Monic := (polyCharpoly_monic _ _).map _ -lemma lieCharpoly_natDegree : (lieCharpoly R M x y).natDegree = finrank R M := by +lemma lieCharpoly_natDegree [Nontrivial R] : (lieCharpoly R M x y).natDegree = finrank R M := by rw [lieCharpoly, (polyCharpoly_monic _ _).natDegree_map, polyCharpoly_natDegree] variable {R} in @@ -97,7 +97,7 @@ lemma lieCharpoly_map_eval (r : R) : map_add, map_mul, aeval_C, Algebra.id.map_eq_id, RingHom.id_apply, aeval_X, aux, MvPolynomial.coe_aeval_eq_eval, polyCharpoly_map_eq_charpoly, LieHom.coe_toLinearMap] -lemma lieCharpoly_coeff_natDegree (i j : ℕ) (hij : i + j = finrank R M) : +lemma lieCharpoly_coeff_natDegree [Nontrivial R] (i j : ℕ) (hij : i + j = finrank R M) : ((lieCharpoly R M x y).coeff i).natDegree ≤ j := by classical rw [← mul_one j, lieCharpoly, coeff_map] diff --git a/Mathlib/Algebra/Lie/Killing.lean b/Mathlib/Algebra/Lie/Killing.lean index 72cb8a63122ad..45f1f3365045c 100644 --- a/Mathlib/Algebra/Lie/Killing.lean +++ b/Mathlib/Algebra/Lie/Killing.lean @@ -54,7 +54,7 @@ attribute [simp] IsKilling.killingCompl_top_eq_bot namespace IsKilling -variable [Module.Free R L] [Module.Finite R L] [IsKilling R L] +variable [IsKilling R L] @[simp] lemma ker_killingForm_eq_bot : LinearMap.ker (killingForm R L) = ⊥ := by @@ -65,7 +65,8 @@ lemma killingForm_nondegenerate : simp [LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot] variable {R L} in -lemma ideal_eq_bot_of_isLieAbelian [IsDomain R] [IsPrincipalIdealRing R] +lemma ideal_eq_bot_of_isLieAbelian + [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] (I : LieIdeal R L) [IsLieAbelian I] : I = ⊥ := by rw [eq_bot_iff, ← killingCompl_top_eq_bot] exact I.le_killingCompl_top_of_isLieAbelian @@ -83,7 +84,9 @@ over fields with positive characteristic. Note that when the coefficients are a field this instance is redundant since we have `LieAlgebra.IsKilling.instSemisimple` and `LieAlgebra.IsSemisimple.instHasTrivialRadical`. -/ -instance instHasTrivialRadical [IsDomain R] [IsPrincipalIdealRing R] : HasTrivialRadical R L := +instance instHasTrivialRadical + [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] : + HasTrivialRadical R L := (hasTrivialRadical_iff_no_abelian_ideals R L).mpr IsKilling.ideal_eq_bot_of_isLieAbelian end IsKilling diff --git a/Mathlib/Algebra/Lie/Weights/Linear.lean b/Mathlib/Algebra/Lie/Weights/Linear.lean index bcd07bf9df39c..39d847bba73c0 100644 --- a/Mathlib/Algebra/Lie/Weights/Linear.lean +++ b/Mathlib/Algebra/Lie/Weights/Linear.lean @@ -55,8 +55,7 @@ class LinearWeights [LieAlgebra.IsNilpotent R L] : Prop := namespace Weight -variable [LieAlgebra.IsNilpotent R L] [LinearWeights R L M] - [NoZeroSMulDivisors R M] [IsNoetherian R M] (χ : Weight R L M) +variable [LieAlgebra.IsNilpotent R L] [LinearWeights R L M] (χ : Weight R L M) /-- A weight of a Lie module, bundled as a linear map. -/ @[simps] @@ -155,7 +154,7 @@ instance instLinearWeightsOfCharZero [CharZero R] : end FiniteDimensional -variable [LieAlgebra.IsNilpotent R L] [LinearWeights R L M] (χ : L → R) +variable [LieAlgebra.IsNilpotent R L] (χ : L → R) /-- A type synonym for the `χ`-weight space but with the action of `x : L` on `m : weightSpace M χ`, shifted to act as `⁅x, m⁆ - χ x • m`. -/ @@ -166,6 +165,8 @@ namespace shiftedWeightSpace private lemma aux [h : Nontrivial (shiftedWeightSpace R L M χ)] : weightSpace M χ ≠ ⊥ := (LieSubmodule.nontrivial_iff_ne_bot _ _ _).mp h +variable [LinearWeights R L M] + instance : LieRingModule L (shiftedWeightSpace R L M χ) where bracket x m := ⁅x, m⁆ - χ x • m add_lie x y m := by @@ -217,7 +218,7 @@ end shiftedWeightSpace /-- Given a Lie module `M` of a Lie algebra `L` with coefficients in `R`, if a function `χ : L → R` has a simultaneous generalized eigenvector for the action of `L` then it has a simultaneous true eigenvector, provided `M` is Noetherian and has linear weights. -/ -lemma exists_forall_lie_eq_smul [IsNoetherian R M] (χ : Weight R L M) : +lemma exists_forall_lie_eq_smul [LinearWeights R L M] [IsNoetherian R M] (χ : Weight R L M) : ∃ m : M, m ≠ 0 ∧ ∀ x : L, ⁅x, m⁆ = χ x • m := by replace hχ : Nontrivial (shiftedWeightSpace R L M χ) := (LieSubmodule.nontrivial_iff_ne_bot R L M).mpr χ.weightSpace_ne_bot diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unitary.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unitary.lean index bda712cdab3b1..d39bee3d59145 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unitary.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unitary.lean @@ -20,7 +20,7 @@ section Generic variable {R A : Type*} {p : A → Prop} [CommRing R] [StarRing R] [MetricSpace R] variable [TopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] -variable [Algebra R A] [StarModule R A] [ContinuousFunctionalCalculus R p] +variable [Algebra R A] [ContinuousFunctionalCalculus R p] lemma cfc_unitary_iff (f : R → R) (a : A) (ha : p a := by cfc_tac) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) : @@ -35,7 +35,7 @@ end Generic section Complex variable {A : Type*} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] - [StarModule ℂ A] [ContinuousFunctionalCalculus ℂ (IsStarNormal : A → Prop)] + [ContinuousFunctionalCalculus ℂ (IsStarNormal : A → Prop)] lemma unitary_iff_isStarNormal_and_spectrum_subset_unitary {u : A} : u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ unitary ℂ := by diff --git a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean index b02054cbd951d..d201d59948dd7 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean @@ -787,8 +787,7 @@ that the differentiability set `D` is measurable. -/ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] - {α : Type*} [TopologicalSpace α] [MeasurableSpace α] [MeasurableSpace E] - [OpensMeasurableSpace α] [OpensMeasurableSpace E] + {α : Type*} [TopologicalSpace α] {f : α → E → F} (K : Set (E →L[𝕜] F)) namespace FDerivMeasurableAux @@ -873,6 +872,8 @@ end FDerivMeasurableAux open FDerivMeasurableAux +variable [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace E] [OpensMeasurableSpace E] + theorem measurableSet_of_differentiableAt_of_isComplete_with_param (hf : Continuous f.uncurry) {K : Set (E →L[𝕜] F)} (hK : IsComplete K) : MeasurableSet {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} := by diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean index 732c088472bb7..7ddc90e99180e 100644 --- a/Mathlib/Analysis/Fourier/AddCircle.lean +++ b/Mathlib/Analysis/Fourier/AddCircle.lean @@ -243,7 +243,7 @@ theorem coeFn_fourierLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (n : ℤ) : theorem span_fourierLp_closure_eq_top {p : ℝ≥0∞} [Fact (1 ≤ p)] (hp : p ≠ ∞) : (span ℂ (range (@fourierLp T _ p _))).topologicalClosure = ⊤ := by convert - (ContinuousMap.toLp_denseRange ℂ (@haarAddCircle T hT) hp ℂ).topologicalClosure_map_submodule + (ContinuousMap.toLp_denseRange ℂ (@haarAddCircle T hT) ℂ hp).topologicalClosure_map_submodule span_fourier_closure_eq_top erw [map_span, range_comp] simp only [ContinuousLinearMap.coe_coe] diff --git a/Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean b/Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean index e35d4c0f03deb..a054142703272 100644 --- a/Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean +++ b/Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean @@ -75,8 +75,11 @@ theorem separate_convex_open_set [TopologicalSpace E] [AddCommGroup E] [Topologi one_le_gauge_of_not_mem (hs₁.starConvex hs₀) (absorbent_nhds_zero <| hs₂.mem_nhds hs₀).absorbs hx₀ -variable [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module ℝ E] - [ContinuousSMul ℝ E] {s t : Set E} {x y : E} +variable [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] + {s t : Set E} {x y : E} +section + +variable [TopologicalAddGroup E] [ContinuousSMul ℝ E] /-- A version of the **Hahn-Banach theorem**: given disjoint convex sets `s`, `t` where `s` is open, there is a continuous linear functional which separates them. -/ @@ -203,6 +206,8 @@ theorem iInter_halfspaces_eq (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) : obtain ⟨y, hy, hxy⟩ := hx l exact ((hxy.trans_lt (hlA y hy)).trans hl).not_le le_rfl +end + namespace RCLike variable [RCLike 𝕜] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [IsScalarTower ℝ 𝕜 E] @@ -218,12 +223,12 @@ noncomputable def extendTo𝕜'ₗ : (E →L[ℝ] ℝ) →ₗ[ℝ] (E →L[𝕜] map_smul' := by intros; ext; simp [h, real_smul_eq_coe_mul]; ring } @[simp] -lemma re_extendTo𝕜'ₗ (g : E →L[ℝ] ℝ) (x : E) : re ((extendTo𝕜'ₗ g) x : 𝕜) = g x := by +lemma re_extendTo𝕜'ₗ (g : E →L[ℝ] ℝ) (x : E) : re ((extendTo𝕜'ₗ g) x : 𝕜) = g x := by have h g (x : E) : extendTo𝕜'ₗ g x = ((g x : 𝕜) - (I : 𝕜) * (g ((I : 𝕜) • x) : 𝕜)) := rfl simp only [h , map_sub, ofReal_re, mul_re, I_re, zero_mul, ofReal_im, mul_zero, sub_self, sub_zero] -variable [ContinuousSMul ℝ E] +variable [TopologicalAddGroup E] [ContinuousSMul ℝ E] theorem separate_convex_open_set {s : Set E} (hs₀ : (0 : E) ∈ s) (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) {x₀ : E} (hx₀ : x₀ ∉ s) : diff --git a/Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean index d8515484fe143..570e89aa491e2 100644 --- a/Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean +++ b/Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean @@ -28,7 +28,14 @@ open Finset Matrix namespace SimpleGraph variable {V : Type*} (R : Type*) -variable [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] +variable [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] + +theorem degree_eq_sum_if_adj {R : Type*} [AddCommMonoidWithOne R] (i : V) : + (G.degree i : R) = ∑ j : V, if G.Adj i j then 1 else 0 := by + unfold degree neighborFinset neighborSet + rw [sum_boole, Set.toFinset_setOf] + +variable [DecidableEq V] /-- The diagonal matrix consisting of the degrees of the vertices in the graph. -/ def degMatrix [AddMonoidWithOne R] : Matrix V V R := Matrix.diagonal (G.degree ·) @@ -64,11 +71,6 @@ theorem dotProduct_mulVec_degMatrix [CommRing R] (x : V → R) : variable (R) -theorem degree_eq_sum_if_adj [AddCommMonoidWithOne R] (i : V) : - (G.degree i : R) = ∑ j : V, if G.Adj i j then 1 else 0 := by - unfold degree neighborFinset neighborSet - rw [sum_boole, Set.toFinset_setOf] - /-- Let $L$ be the graph Laplacian and let $x \in \mathbb{R}$, then $$x^{\top} L x = \sum_{i \sim j} (x_{i}-x_{j})^{2}$$, where $\sim$ denotes the adjacency relation -/ diff --git a/Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean b/Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean index 8fb7c52d6bcbf..97804c5a82769 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean @@ -19,11 +19,10 @@ open Set ChartedSpace SmoothManifoldWithCorners open scoped Topology Manifold variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] - -- declare a smooth manifold `M` over the pair `(E, H)`. + -- declare a charted space `M` over the pair `(E, H)`. {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M] - [SmoothManifoldWithCorners I M] -- declare a smooth manifold `M'` over the pair `(E', H')`. {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] @@ -120,49 +119,6 @@ theorem ContinuousLinearMap.contMDiffOn (L : E →L[𝕜] F) {s} : ContMDiffOn theorem ContinuousLinearMap.smooth (L : E →L[𝕜] F) : Smooth 𝓘(𝕜, E) 𝓘(𝕜, F) L := L.contMDiff -theorem ContMDiffWithinAt.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M} {x : M} - (hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s x) - (hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s x) : - ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) s x := - ContDiff.comp_contMDiffWithinAt (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₁) => x.1.comp x.2) - (f := fun x => (g x, f x)) (contDiff_fst.clm_comp contDiff_snd) (hg.prod_mk_space hf) - -theorem ContMDiffAt.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {x : M} - (hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g x) (hf : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f x) : - ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) x := - (hg.contMDiffWithinAt.clm_comp hf.contMDiffWithinAt).contMDiffAt Filter.univ_mem - -theorem ContMDiffOn.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M} - (hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s) (hf : ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s) : - ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) s := fun x hx => - (hg x hx).clm_comp (hf x hx) - -theorem ContMDiff.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} - (hg : ContMDiff I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g) (hf : ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f) : - ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₃) n fun x => (g x).comp (f x) := fun x => (hg x).clm_comp (hf x) - -theorem ContMDiffWithinAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M} - (hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x) - (hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x) : - ContMDiffWithinAt I 𝓘(𝕜, F₂) n (fun x => g x (f x)) s x := - @ContDiffWithinAt.comp_contMDiffWithinAt _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - (fun x : (F₁ →L[𝕜] F₂) × F₁ => x.1 x.2) (fun x => (g x, f x)) s _ x - (by apply ContDiff.contDiffAt; exact contDiff_fst.clm_apply contDiff_snd) (hg.prod_mk_space hf) - (by simp_rw [preimage_univ, subset_univ]) - -nonrec theorem ContMDiffAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M} - (hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g x) (hf : ContMDiffAt I 𝓘(𝕜, F₁) n f x) : - ContMDiffAt I 𝓘(𝕜, F₂) n (fun x => g x (f x)) x := - hg.clm_apply hf - -theorem ContMDiffOn.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} - (hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s) (hf : ContMDiffOn I 𝓘(𝕜, F₁) n f s) : - ContMDiffOn I 𝓘(𝕜, F₂) n (fun x => g x (f x)) s := fun x hx => (hg x hx).clm_apply (hf x hx) - -theorem ContMDiff.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} - (hg : ContMDiff I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g) (hf : ContMDiff I 𝓘(𝕜, F₁) n f) : - ContMDiff I 𝓘(𝕜, F₂) n fun x => g x (f x) := fun x => (hg x).clm_apply (hf x) - theorem ContMDiffWithinAt.clm_precomp {f : M → F₁ →L[𝕜] F₂} {s : Set M} {x : M} (hf : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n f s x) : ContMDiffWithinAt I 𝓘(𝕜, (F₂ →L[𝕜] F₃) →L[𝕜] (F₁ →L[𝕜] F₃)) n @@ -211,6 +167,52 @@ theorem ContMDiff.clm_postcomp {f : M → F₂ →L[𝕜] F₃} (hf : ContMDiff (fun y ↦ (f y).postcomp F₁ : M → (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃)) := fun x ↦ (hf x).clm_postcomp +-- Now make `M` a smooth manifold. +variable [SmoothManifoldWithCorners I M] + +theorem ContMDiffWithinAt.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M} {x : M} + (hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s x) + (hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s x) : + ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) s x := + ContDiff.comp_contMDiffWithinAt (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₁) => x.1.comp x.2) + (f := fun x => (g x, f x)) (contDiff_fst.clm_comp contDiff_snd) (hg.prod_mk_space hf) + +theorem ContMDiffAt.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {x : M} + (hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g x) (hf : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f x) : + ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) x := + (hg.contMDiffWithinAt.clm_comp hf.contMDiffWithinAt).contMDiffAt Filter.univ_mem + +theorem ContMDiffOn.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M} + (hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s) (hf : ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s) : + ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) s := fun x hx => + (hg x hx).clm_comp (hf x hx) + +theorem ContMDiff.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} + (hg : ContMDiff I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g) (hf : ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f) : + ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₃) n fun x => (g x).comp (f x) := fun x => (hg x).clm_comp (hf x) + +theorem ContMDiffWithinAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M} + (hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x) + (hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x) : + ContMDiffWithinAt I 𝓘(𝕜, F₂) n (fun x => g x (f x)) s x := + ContDiffWithinAt.comp_contMDiffWithinAt + (g := fun x : (F₁ →L[𝕜] F₂) × F₁ => x.1 x.2) + (by apply ContDiff.contDiffAt; exact contDiff_fst.clm_apply contDiff_snd) (hg.prod_mk_space hf) + (by simp_rw [preimage_univ, subset_univ]) + +nonrec theorem ContMDiffAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M} + (hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g x) (hf : ContMDiffAt I 𝓘(𝕜, F₁) n f x) : + ContMDiffAt I 𝓘(𝕜, F₂) n (fun x => g x (f x)) x := + hg.clm_apply hf + +theorem ContMDiffOn.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} + (hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s) (hf : ContMDiffOn I 𝓘(𝕜, F₁) n f s) : + ContMDiffOn I 𝓘(𝕜, F₂) n (fun x => g x (f x)) s := fun x hx => (hg x hx).clm_apply (hf x hx) + +theorem ContMDiff.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} + (hg : ContMDiff I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g) (hf : ContMDiff I 𝓘(𝕜, F₁) n f) : + ContMDiff I 𝓘(𝕜, F₂) n fun x => g x (f x) := fun x => (hg x).clm_apply (hf x) + theorem ContMDiffWithinAt.cle_arrowCongr {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} {s : Set M} {x : M} (hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n (fun x ↦ ((f x).symm : F₂ →L[𝕜] F₁)) s x) diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Product.lean b/Mathlib/Geometry/Manifold/ContMDiff/Product.lean index 6ef4a2c6de4d0..6cd5c2919d09b 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Product.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Product.lean @@ -20,30 +20,22 @@ open Set Function Filter ChartedSpace SmoothManifoldWithCorners open scoped Topology Manifold variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] - -- declare a smooth manifold `M` over the pair `(E, H)`. + -- declare a charted space `M` over the pair `(E, H)`. {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M] - [SmoothManifoldWithCorners I M] - -- declare a smooth manifold `M'` over the pair `(E', H')`. + -- declare a charted space `M'` over the pair `(E', H')`. {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] - [SmoothManifoldWithCorners I' M'] - -- declare a manifold `M''` over the pair `(E'', H'')`. - {E'' : Type*} - [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type*} [TopologicalSpace H''] - {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type*} [TopologicalSpace M''] [ChartedSpace H'' M''] - -- declare a smooth manifold `N` over the pair `(F, G)`. + -- declare a charted space `N` over the pair `(F, G)`. {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type*} [TopologicalSpace N] [ChartedSpace G N] - [SmoothManifoldWithCorners J N] - -- declare a smooth manifold `N'` over the pair `(F', G')`. + -- declare a charted space `N'` over the pair `(F', G')`. {F' : Type*} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type*} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type*} [TopologicalSpace N'] [ChartedSpace G' N'] - [SmoothManifoldWithCorners J' N'] -- F₁, F₂, F₃, F₄ are normed spaces {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type*} [NormedAddCommGroup F₂] diff --git a/Mathlib/LinearAlgebra/Matrix/SchurComplement.lean b/Mathlib/LinearAlgebra/Matrix/SchurComplement.lean index 3dc06c9196321..e233de0d891e6 100644 --- a/Mathlib/LinearAlgebra/Matrix/SchurComplement.lean +++ b/Mathlib/LinearAlgebra/Matrix/SchurComplement.lean @@ -443,7 +443,7 @@ end CommRing section StarOrderedRing -variable {𝕜 : Type*} [CommRing 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] +variable {𝕜 : Type*} [CommRing 𝕜] [StarRing 𝕜] scoped infixl:65 " ⊕ᵥ " => Sum.elim @@ -491,6 +491,8 @@ theorem IsHermitian.fromBlocks₂₂ [Fintype n] [DecidableEq n] (A : Matrix m m fromBlocks_submatrix_sum_swap_sum_swap] convert IsHermitian.fromBlocks₁₁ _ _ hD <;> simp +variable [PartialOrder 𝕜] [StarOrderedRing 𝕜] + theorem PosSemidef.fromBlocks₁₁ [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m m 𝕜} (B : Matrix m n 𝕜) (D : Matrix n n 𝕜) (hA : A.PosDef) [Invertible A] : (fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef := by diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean index e47b7dd06d224..9e03eae8ea344 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean @@ -470,7 +470,8 @@ end NNReal spanning measurable sets with finite measure on which `f` is bounded. See also `StronglyMeasurable.exists_spanning_measurableSet_norm_le` for functions into normed groups. -/ -theorem exists_spanning_measurableSet_le {m : MeasurableSpace α} {f : α → ℝ≥0} +-- We redeclare `α` to temporarily avoid the `[MeasurableSpace α]` instance. +theorem exists_spanning_measurableSet_le {α : Type*} {m : MeasurableSpace α} {f : α → ℝ≥0} (hf : Measurable f) (μ : Measure α) [SigmaFinite μ] : ∃ s : ℕ → Set α, (∀ n, MeasurableSet (s n) ∧ μ (s n) < ∞ ∧ ∀ x ∈ s n, f x ≤ n) ∧ diff --git a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean index 75e4a6fbdd0a2..be0467e7351a6 100644 --- a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean @@ -793,9 +793,9 @@ theorem _root_.IsClosed.measurableSet_image_of_continuousOn_injOn · rwa [continuousOn_iff_continuous_restrict] at f_cont · rwa [injOn_iff_injective] at f_inj -variable {α β : Type*} [tβ : TopologicalSpace β] [T2Space β] [MeasurableSpace β] - [MeasurableSpace α] - {s : Set γ} {f : γ → β} +variable {α β : Type*} [MeasurableSpace β] +section +variable [tβ : TopologicalSpace β] [T2Space β] [MeasurableSpace α] {s : Set γ} {f : γ → β} /-- The Lusin-Souslin theorem: if `s` is Borel-measurable in a Polish space, then its image under a continuous injective map is also Borel-measurable. -/ @@ -879,7 +879,7 @@ theorem borel_eq_borel_of_le {t t' : TopologicalSpace γ} refine le_antisymm ?_ (borel_anti hle) intro s hs have e := @Continuous.measurableEmbedding - _ _ t' _ (@borel _ t') _ (@BorelSpace.mk _ _ (borel γ) rfl) + _ _ (@borel _ t') t' _ _ (@BorelSpace.mk _ _ (borel γ) rfl) t _ (@borel _ t) (@BorelSpace.mk _ t (@borel _ t) rfl) (continuous_id_of_le hle) injective_id convert e.measurableSet_image.2 hs simp only [id_eq, image_id'] @@ -898,6 +898,8 @@ theorem isClopenable_iff_measurableSet · exact MeasurableSpace.measurableSet_generateFrom s_open infer_instance +end + /-- The set of points for which a sequence of measurable functions converges to a given function is measurable. -/ @[measurability] diff --git a/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean b/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean index bfe6a02c9efa5..d16ec22981a70 100644 --- a/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean +++ b/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean @@ -61,7 +61,7 @@ open scoped ENNReal NNReal Topology BoundedContinuousFunction open MeasureTheory TopologicalSpace ContinuousMap Set Bornology -variable {α : Type*} [TopologicalSpace α] [NormalSpace α] [R1Space α] +variable {α : Type*} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] variable {E : Type*} [NormedAddCommGroup E] {μ : Measure α} {p : ℝ≥0∞} @@ -137,7 +137,8 @@ alias exists_continuous_snorm_sub_le_of_closed := exists_continuous_eLpNorm_sub_ /-- In a locally compact space, any function in `ℒp` can be approximated by compactly supported continuous functions when `p < ∞`, version in terms of `eLpNorm`. -/ -theorem Memℒp.exists_hasCompactSupport_eLpNorm_sub_le [WeaklyLocallyCompactSpace α] [μ.Regular] +theorem Memℒp.exists_hasCompactSupport_eLpNorm_sub_le + [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] (hp : p ≠ ∞) {f : α → E} (hf : Memℒp f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) : ∃ g : α → E, HasCompactSupport g ∧ eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ := by suffices H : @@ -194,7 +195,7 @@ alias Memℒp.exists_hasCompactSupport_snorm_sub_le := Memℒp.exists_hasCompact /-- In a locally compact space, any function in `ℒp` can be approximated by compactly supported continuous functions when `0 < p < ∞`, version in terms of `∫`. -/ theorem Memℒp.exists_hasCompactSupport_integral_rpow_sub_le - [WeaklyLocallyCompactSpace α] [μ.Regular] + [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {p : ℝ} (hp : 0 < p) {f : α → E} (hf : Memℒp f (ENNReal.ofReal p) μ) {ε : ℝ} (hε : 0 < ε) : ∃ g : α → E, HasCompactSupport g ∧ @@ -215,7 +216,7 @@ theorem Memℒp.exists_hasCompactSupport_integral_rpow_sub_le /-- In a locally compact space, any integrable function can be approximated by compactly supported continuous functions, version in terms of `∫⁻`. -/ theorem Integrable.exists_hasCompactSupport_lintegral_sub_le - [WeaklyLocallyCompactSpace α] [μ.Regular] + [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E} (hf : Integrable f μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) : ∃ g : α → E, HasCompactSupport g ∧ (∫⁻ x, ‖f x - g x‖₊ ∂μ) ≤ ε ∧ Continuous g ∧ Integrable g μ := by @@ -225,7 +226,7 @@ theorem Integrable.exists_hasCompactSupport_lintegral_sub_le /-- In a locally compact space, any integrable function can be approximated by compactly supported continuous functions, version in terms of `∫`. -/ theorem Integrable.exists_hasCompactSupport_integral_sub_le - [WeaklyLocallyCompactSpace α] [μ.Regular] + [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E} (hf : Integrable f μ) {ε : ℝ} (hε : 0 < ε) : ∃ g : α → E, HasCompactSupport g ∧ (∫ x, ‖f x - g x‖ ∂μ) ≤ ε ∧ Continuous g ∧ Integrable g μ := by @@ -347,13 +348,13 @@ end Lp end MeasureTheory -variable [SecondCountableTopologyEither α E] [_i : Fact (1 ≤ p)] (hp : p ≠ ∞) +variable [SecondCountableTopologyEither α E] [_i : Fact (1 ≤ p)] variable (𝕜 : Type*) [NormedField 𝕜] [NormedAlgebra ℝ 𝕜] [NormedSpace 𝕜 E] variable (E) (μ) namespace BoundedContinuousFunction -theorem toLp_denseRange [μ.WeaklyRegular] [IsFiniteMeasure μ] : +theorem toLp_denseRange [μ.WeaklyRegular] [IsFiniteMeasure μ] (hp : p ≠ ∞) : DenseRange (toLp p μ 𝕜 : (α →ᵇ E) →L[𝕜] Lp E p μ) := by haveI : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E simpa only [← range_toLp p μ (𝕜 := 𝕜)] @@ -366,9 +367,9 @@ namespace ContinuousMap /-- Continuous functions are dense in `MeasureTheory.Lp`, `1 ≤ p < ∞`. This theorem assumes that the domain is a compact space because otherwise `ContinuousMap.toLp` is undefined. Use `BoundedContinuousFunction.toLp_denseRange` if the domain is not a compact space. -/ -theorem toLp_denseRange [CompactSpace α] [μ.WeaklyRegular] [IsFiniteMeasure μ] : +theorem toLp_denseRange [CompactSpace α] [μ.WeaklyRegular] [IsFiniteMeasure μ] (hp : p ≠ ∞) : DenseRange (toLp p μ 𝕜 : C(α, E) →L[𝕜] Lp E p μ) := by - refine (BoundedContinuousFunction.toLp_denseRange _ _ hp 𝕜).mono ?_ + refine (BoundedContinuousFunction.toLp_denseRange _ _ 𝕜 hp).mono ?_ refine range_subset_iff.2 fun f ↦ ?_ exact ⟨f.toContinuousMap, rfl⟩ diff --git a/Mathlib/MeasureTheory/Group/Integral.lean b/Mathlib/MeasureTheory/Group/Integral.lean index aed3991da1182..665790505f3cd 100644 --- a/Mathlib/MeasureTheory/Group/Integral.lean +++ b/Mathlib/MeasureTheory/Group/Integral.lean @@ -20,7 +20,7 @@ open Measure TopologicalSpace open scoped ENNReal variable {𝕜 M α G E F : Type*} [MeasurableSpace G] -variable [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] +variable [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] variable {μ : Measure G} {f : G → E} {g : G} section MeasurableInv diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean index 0e02937ac68d2..7bc444ca0b8c6 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner.lean @@ -699,8 +699,8 @@ Define the Bochner integral on functions generally to be the `L1` Bochner integr functions, and 0 otherwise; prove its basic properties. -/ -variable [NormedAddCommGroup E] [NormedSpace ℝ E] [hE : CompleteSpace E] [NontriviallyNormedField 𝕜] - [NormedSpace 𝕜 E] [SMulCommClass ℝ 𝕜 E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] +variable [NormedAddCommGroup E] [hE : CompleteSpace E] [NontriviallyNormedField 𝕜] + [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] open Classical in @@ -730,6 +730,7 @@ section Properties open ContinuousLinearMap MeasureTheory.SimpleFunc +variable [NormedSpace ℝ E] [SMulCommClass ℝ 𝕜 E] variable {f g : α → E} {m : MeasurableSpace α} {μ : Measure α} theorem integral_eq (f : α → E) (hf : Integrable f μ) : ∫ a, f a ∂μ = L1.integral (hf.toL1 f) := by diff --git a/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean b/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean index a07c2b8aa6b73..1a10dec86151f 100644 --- a/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean +++ b/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean @@ -26,13 +26,13 @@ lemma apply_le_nndist_zero {X : Type*} [TopologicalSpace X] (f : X →ᵇ ℝ≥ convert nndist_coe_le_nndist x simp only [coe_zero, Pi.zero_apply, NNReal.nndist_zero_eq_val] -variable {X : Type*} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] +variable {X : Type*} [MeasurableSpace X] [TopologicalSpace X] lemma lintegral_le_edist_mul (f : X →ᵇ ℝ≥0) (μ : Measure X) : (∫⁻ x, f x ∂μ) ≤ edist 0 f * (μ Set.univ) := le_trans (lintegral_mono (fun x ↦ ENNReal.coe_le_coe.mpr (f.apply_le_nndist_zero x))) (by simp) -theorem measurable_coe_ennreal_comp (f : X →ᵇ ℝ≥0) : +theorem measurable_coe_ennreal_comp [OpensMeasurableSpace X] (f : X →ᵇ ℝ≥0) : Measurable fun x ↦ (f x : ℝ≥0∞) := measurable_coe_nnreal_ennreal.comp f.continuous.measurable @@ -44,12 +44,13 @@ theorem lintegral_lt_top_of_nnreal (f : X →ᵇ ℝ≥0) : ∫⁻ x, f x ∂μ have key := BoundedContinuousFunction.NNReal.upper_bound f x rwa [ENNReal.coe_le_coe] -theorem integrable_of_nnreal (f : X →ᵇ ℝ≥0) : Integrable (((↑) : ℝ≥0 → ℝ) ∘ ⇑f) μ := by +theorem integrable_of_nnreal [OpensMeasurableSpace X] (f : X →ᵇ ℝ≥0) : + Integrable (((↑) : ℝ≥0 → ℝ) ∘ ⇑f) μ := by refine ⟨(NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable, ?_⟩ simp only [HasFiniteIntegral, Function.comp_apply, NNReal.nnnorm_eq] exact lintegral_lt_top_of_nnreal _ f -theorem integral_eq_integral_nnrealPart_sub (f : X →ᵇ ℝ) : +theorem integral_eq_integral_nnrealPart_sub [OpensMeasurableSpace X] (f : X →ᵇ ℝ) : ∫ x, f x ∂μ = (∫ x, (f.nnrealPart x : ℝ) ∂μ) - ∫ x, ((-f).nnrealPart x : ℝ) ∂μ := by simp only [f.self_eq_nnrealPart_sub_nnrealPart_neg, Pi.sub_apply, integral_sub, integrable_of_nnreal] @@ -58,7 +59,7 @@ theorem integral_eq_integral_nnrealPart_sub (f : X →ᵇ ℝ) : theorem lintegral_of_real_lt_top (f : X →ᵇ ℝ) : ∫⁻ x, ENNReal.ofReal (f x) ∂μ < ∞ := lintegral_lt_top_of_nnreal _ f.nnrealPart -theorem toReal_lintegral_coe_eq_integral (f : X →ᵇ ℝ≥0) (μ : Measure X) : +theorem toReal_lintegral_coe_eq_integral [OpensMeasurableSpace X] (f : X →ᵇ ℝ≥0) (μ : Measure X) : (∫⁻ x, (f x : ℝ≥0∞) ∂μ).toReal = ∫ x, (f x : ℝ) ∂μ := by rw [integral_eq_lintegral_of_nonneg_ae _ (by simpa [Function.comp_apply] using (NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable)] @@ -69,10 +70,9 @@ end NNRealValued section BochnerIntegral -variable {X : Type*} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] +variable {X : Type*} [MeasurableSpace X] [TopologicalSpace X] variable (μ : Measure X) -variable {E : Type*} [NormedAddCommGroup E] [SecondCountableTopology E] -variable [MeasurableSpace E] [BorelSpace E] +variable {E : Type*} [NormedAddCommGroup E] lemma lintegral_nnnorm_le (f : X →ᵇ E) : ∫⁻ x, ‖f x‖₊ ∂μ ≤ ‖f‖₊ * (μ Set.univ) := by @@ -80,6 +80,8 @@ lemma lintegral_nnnorm_le (f : X →ᵇ E) : _ ≤ ∫⁻ _, ‖f‖₊ ∂μ := by gcongr; apply nnnorm_coe_le_nnnorm _ = ‖f‖₊ * (μ Set.univ) := by rw [lintegral_const] +variable [OpensMeasurableSpace X] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] + lemma integrable [IsFiniteMeasure μ] (f : X →ᵇ E) : Integrable f μ := by refine ⟨f.continuous.measurable.aestronglyMeasurable, (hasFiniteIntegral_def _ _).mp ?_⟩ diff --git a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean index cf60664ba60af..cc3daa531971b 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean @@ -19,11 +19,31 @@ the canonical `volume` from the `MeasureSpace` instance. open FiniteDimensional MeasureTheory MeasureTheory.Measure Set variable {ι E F : Type*} -variable [Fintype ι] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] - [MeasurableSpace F] [BorelSpace F] -section +variable [NormedAddCommGroup F] [InnerProductSpace ℝ F] + [NormedAddCommGroup E] [InnerProductSpace ℝ E] + [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] + +namespace LinearIsometryEquiv + +variable (f : E ≃ₗᵢ[ℝ] F) + +/-- Every linear isometry equivalence is a measurable equivalence. -/ +def toMeasureEquiv : E ≃ᵐ F where + toEquiv := f + measurable_toFun := f.continuous.measurable + measurable_invFun := f.symm.continuous.measurable + +@[simp] theorem coe_toMeasureEquiv : (f.toMeasureEquiv : E → F) = f := rfl + +theorem toMeasureEquiv_symm : f.toMeasureEquiv.symm = f.symm.toMeasureEquiv := rfl + +end LinearIsometryEquiv + +variable [Fintype ι] +variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] +section variable {m n : ℕ} [_i : Fact (finrank ℝ F = n)] /-- The volume form coming from an orientation in an inner product space gives measure `1` to the @@ -122,27 +142,13 @@ end PiLp namespace LinearIsometryEquiv -variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] - [MeasurableSpace E] [BorelSpace E] - -variable (f : E ≃ₗᵢ[ℝ] F) - /-- Every linear isometry on a real finite dimensional Hilbert space is measure-preserving. -/ -theorem measurePreserving : MeasurePreserving f := by +theorem measurePreserving (f : E ≃ₗᵢ[ℝ] F) : + MeasurePreserving f := by refine ⟨f.continuous.measurable, ?_⟩ rcases exists_orthonormalBasis ℝ E with ⟨w, b, _hw⟩ erw [← OrthonormalBasis.addHaar_eq_volume b, ← OrthonormalBasis.addHaar_eq_volume (b.map f), Basis.map_addHaar _ f.toContinuousLinearEquiv] congr -/-- Every linear isometry equivalence is a measurable equivalence. -/ -def toMeasureEquiv : E ≃ᵐ F where - toEquiv := f - measurable_toFun := f.continuous.measurable - measurable_invFun := f.symm.continuous.measurable - -@[simp] theorem coe_toMeasureEquiv : (f.toMeasureEquiv : E → F) = f := rfl - -theorem toMeasureEquiv_symm : f.toMeasureEquiv.symm = f.symm.toMeasureEquiv := rfl - end LinearIsometryEquiv diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index 4027bbcc9a884..e066e17c51f07 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -521,7 +521,7 @@ end CyclotomicField section IsDomain -variable [Algebra A K] [IsFractionRing A K] +variable [Algebra A K] section CyclotomicRing @@ -541,7 +541,8 @@ instance CyclotomicField.algebra' {R : Type*} [CommRing R] [Algebra R K] : instance {R : Type*} [CommRing R] [Algebra R K] : IsScalarTower R K (CyclotomicField n K) := SplittingField.isScalarTower _ -instance CyclotomicField.noZeroSMulDivisors : NoZeroSMulDivisors A (CyclotomicField n K) := by +instance CyclotomicField.noZeroSMulDivisors [IsFractionRing A K] : + NoZeroSMulDivisors A (CyclotomicField n K) := by refine NoZeroSMulDivisors.of_algebraMap_injective ?_ rw [IsScalarTower.algebraMap_eq A K (CyclotomicField n K)] exact @@ -578,10 +579,12 @@ instance algebraBase : Algebra A (CyclotomicRing n A K) := -- but there is at `reducible_and_instances` #10906 example {n : ℕ+} : CyclotomicRing.algebraBase n ℤ ℚ = Ring.toIntAlgebra _ := rfl -instance : NoZeroSMulDivisors A (CyclotomicRing n A K) := +instance [IsFractionRing A K] : + NoZeroSMulDivisors A (CyclotomicRing n A K) := (adjoin A _).noZeroSMulDivisors_bot -theorem algebraBase_injective : Function.Injective <| algebraMap A (CyclotomicRing n A K) := +theorem algebraBase_injective [IsFractionRing A K] : + Function.Injective <| algebraMap A (CyclotomicRing n A K) := NoZeroSMulDivisors.algebraMap_injective _ _ instance : Algebra (CyclotomicRing n A K) (CyclotomicField n K) := @@ -597,7 +600,7 @@ instance : NoZeroSMulDivisors (CyclotomicRing n A K) (CyclotomicField n K) := instance : IsScalarTower A (CyclotomicRing n A K) (CyclotomicField n K) := IsScalarTower.subalgebra' _ _ _ _ -instance isCyclotomicExtension [NeZero ((n : ℕ) : A)] : +instance isCyclotomicExtension [IsFractionRing A K] [NeZero ((n : ℕ) : A)] : IsCyclotomicExtension {n} A (CyclotomicRing n A K) where exists_prim_root := @fun a han => by rw [mem_singleton_iff] at han @@ -620,7 +623,7 @@ instance isCyclotomicExtension [NeZero ((n : ℕ) : A)] : · exact Subalgebra.add_mem _ hy hz · exact Subalgebra.mul_mem _ hy hz -instance [IsDomain A] [NeZero ((n : ℕ) : A)] : +instance [IsFractionRing A K] [IsDomain A] [NeZero ((n : ℕ) : A)] : IsFractionRing (CyclotomicRing n A K) (CyclotomicField n K) where map_units' := fun ⟨x, hx⟩ => by rw [isUnit_iff_ne_zero] diff --git a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean index 9fe35d4f6f364..a570a392aa683 100644 --- a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean +++ b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean @@ -40,8 +40,6 @@ variable (R A K : Type*) [CommRing R] [CommRing A] [Field K] open scoped nonZeroDivisors Polynomial -variable [IsDomain A] - section IsIntegralClosure /-! ### `IsIntegralClosure` section @@ -60,7 +58,7 @@ variable [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A /-- If `L` is an algebraic extension of `K = Frac(A)` and `L` has no zero smul divisors by `A`, then `L` is the localization of the integral closure `C` of `A` in `L` at `A⁰`. -/ -theorem IsIntegralClosure.isLocalization [Algebra.IsAlgebraic K L] : +theorem IsIntegralClosure.isLocalization [IsDomain A] [Algebra.IsAlgebraic K L] : IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L := by haveI : IsDomain C := (IsIntegralClosure.equiv A C L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L) @@ -80,7 +78,7 @@ theorem IsIntegralClosure.isLocalization [Algebra.IsAlgebraic K L] : smul_def] · simp only [IsIntegralClosure.algebraMap_injective C A L h] -theorem IsIntegralClosure.isLocalization_of_isSeparable [Algebra.IsSeparable K L] : +theorem IsIntegralClosure.isLocalization_of_isSeparable [IsDomain A] [Algebra.IsSeparable K L] : IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L := IsIntegralClosure.isLocalization A K L C @@ -107,6 +105,7 @@ theorem integralClosure_le_span_dualBasis [Algebra.IsSeparable K L] {ι : Type*} intro x hx exact ⟨⟨x, hx⟩, rfl⟩ +variable [IsDomain A] variable (A K) /-- Send a set of `x`s in a finite extension `L` of the fraction field of `R` diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean index 7aa87440e0881..f6285f4b7aa27 100644 --- a/Mathlib/RingTheory/Discriminant.lean +++ b/Mathlib/RingTheory/Discriminant.lean @@ -301,7 +301,7 @@ end Field section Int /-- Two (finite) ℤ-bases have the same discriminant. -/ -theorem discr_eq_discr [Fintype ι] (b : Basis ι ℤ A) (b' : Basis ι ℤ A) : +theorem discr_eq_discr (b : Basis ι ℤ A) (b' : Basis ι ℤ A) : Algebra.discr ℤ b = Algebra.discr ℤ b' := by convert Algebra.discr_of_matrix_vecMul b' (b'.toMatrix b) · rw [Basis.toMatrix_map_vecMul] diff --git a/Mathlib/RingTheory/Kaehler/Basic.lean b/Mathlib/RingTheory/Kaehler/Basic.lean index d5a828b146a26..c57b401f8224a 100644 --- a/Mathlib/RingTheory/Kaehler/Basic.lean +++ b/Mathlib/RingTheory/Kaehler/Basic.lean @@ -675,6 +675,7 @@ theorem KaehlerDifferential.kerTotal_map' [Algebra R B] refine congr_arg Set.range ?_ ext; simp [IsScalarTower.algebraMap_eq R A B] +section variable [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] /-- The map `Ω[A⁄R] →ₗ[A] Ω[B⁄S]` given a square @@ -786,6 +787,8 @@ lemma KaehlerDifferential.exact_mapBaseChange_map : Function.Exact (mapBaseChange R A B) (map R A B B) := SetLike.ext_iff.mp (range_mapBaseChange R A B).symm +end + /-- The map `I → B ⊗[A] B ⊗[A] Ω[A⁄R]` where `I = ker(A → B)`. -/ @[simps] noncomputable @@ -813,6 +816,8 @@ def KaehlerDifferential.kerCotangentToTensor : lemma KaehlerDifferential.kerCotangentToTensor_toCotangent (x) : kerCotangentToTensor R A B (Ideal.toCotangent _ x) = 1 ⊗ₜ D _ _ x.1 := rfl +variable [Algebra R B] [IsScalarTower R A B] + theorem KaehlerDifferential.range_kerCotangentToTensor (h : Function.Surjective (algebraMap A B)) : LinearMap.range (kerCotangentToTensor R A B) = diff --git a/Mathlib/RingTheory/WittVector/MulCoeff.lean b/Mathlib/RingTheory/WittVector/MulCoeff.lean index f5b7c0ecd8979..edb4720376f65 100644 --- a/Mathlib/RingTheory/WittVector/MulCoeff.lean +++ b/Mathlib/RingTheory/WittVector/MulCoeff.lean @@ -131,7 +131,8 @@ theorem mul_polyOfInterest_aux2 (n : ℕ) : rw [sum_range_succ, add_comm, Nat.sub_self, pow_zero, pow_one] rfl -theorem mul_polyOfInterest_aux3 (n : ℕ) : wittPolyProd p (n + 1) = +-- We redeclare `p` here to locally discard the unneeded `p.Prime` hypothesis. +theorem mul_polyOfInterest_aux3 (p n : ℕ) : wittPolyProd p (n + 1) = -((p : 𝕄) ^ (n + 1) * X (0, n + 1)) * ((p : 𝕄) ^ (n + 1) * X (1, n + 1)) + (p : 𝕄) ^ (n + 1) * X (0, n + 1) * rename (Prod.mk (1 : Fin 2)) (wittPolynomial p ℤ (n + 1)) + (p : 𝕄) ^ (n + 1) * X (1, n + 1) * rename (Prod.mk (0 : Fin 2)) (wittPolynomial p ℤ (n + 1)) + diff --git a/Mathlib/Topology/Algebra/Algebra.lean b/Mathlib/Topology/Algebra/Algebra.lean index 5eff70c7f4cc8..c229209194995 100644 --- a/Mathlib/Topology/Algebra/Algebra.lean +++ b/Mathlib/Topology/Algebra/Algebra.lean @@ -52,6 +52,7 @@ theorem continuousSMul_of_algebraMap [TopologicalSemiring A] (h : Continuous (al ContinuousSMul R A := ⟨(continuous_algebraMap_iff_smul R A).1 h⟩ +section variable [ContinuousSMul R A] /-- The inclusion of the base ring in a topological algebra as a continuous linear map. -/ @@ -67,6 +68,8 @@ theorem algebraMapCLM_coe : ⇑(algebraMapCLM R A) = algebraMap R A := theorem algebraMapCLM_toLinearMap : (algebraMapCLM R A).toLinearMap = Algebra.linearMap R A := rfl +end + /-- If `R` is a discrete topological ring, then any topological ring `S` which is an `R`-algebra is also a topological `R`-algebra.