diff --git a/Counterexamples/Pseudoelement.lean b/Counterexamples/Pseudoelement.lean index fa640e6f0a..2bc8b8fc8a 100644 --- a/Counterexamples/Pseudoelement.lean +++ b/Counterexamples/Pseudoelement.lean @@ -65,8 +65,6 @@ theorem snd_x_pseudo_eq_snd_y : PseudoEqual _ (app biprod.snd x) (app biprod.snd simp_rw [biprod.lift_snd]; rfl set_option backward.isDefEq.respectTransparency false in --- Porting note: locally disable instance to avoid inferred/synthesized clash -attribute [-instance] AddCommGroup.toIntModule in /-- `x` is not pseudoequal to `y`. -/ theorem x_not_pseudo_eq : ¬PseudoEqual _ x y := by intro h diff --git a/Mathlib.lean b/Mathlib.lean index 624f35d65f..9d18364412 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2046,6 +2046,7 @@ public import Mathlib.Analysis.InnerProductSpace.Convex public import Mathlib.Analysis.InnerProductSpace.Defs public import Mathlib.Analysis.InnerProductSpace.Dual public import Mathlib.Analysis.InnerProductSpace.EuclideanDist +public import Mathlib.Analysis.InnerProductSpace.ExteriorPower public import Mathlib.Analysis.InnerProductSpace.GramMatrix public import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho public import Mathlib.Analysis.InnerProductSpace.Harmonic.Basic @@ -4597,6 +4598,7 @@ public import Mathlib.Geometry.Convex.Cone.Face.Basic public import Mathlib.Geometry.Convex.Cone.Pointed public import Mathlib.Geometry.Convex.Cone.Simplicial public import Mathlib.Geometry.Convex.Cone.TensorProduct +public import Mathlib.Geometry.Convex.ConvexSpace.AffineMap public import Mathlib.Geometry.Convex.ConvexSpace.AffineSpace public import Mathlib.Geometry.Convex.ConvexSpace.Defs public import Mathlib.Geometry.Convex.ConvexSpace.Module @@ -4903,6 +4905,7 @@ public import Mathlib.InformationTheory.Coding.UniquelyDecodable public import Mathlib.InformationTheory.Hamming public import Mathlib.InformationTheory.KullbackLeibler.Basic public import Mathlib.InformationTheory.KullbackLeibler.ChainRule +public import Mathlib.InformationTheory.KullbackLeibler.DataProcessing public import Mathlib.InformationTheory.KullbackLeibler.KLFun public import Mathlib.Init public import Mathlib.Lean.ContextInfo @@ -6133,6 +6136,7 @@ public import Mathlib.Order.Interval.Finset.Box public import Mathlib.Order.Interval.Finset.Defs public import Mathlib.Order.Interval.Finset.DenselyOrdered public import Mathlib.Order.Interval.Finset.Fin +public import Mathlib.Order.Interval.Finset.Floor public import Mathlib.Order.Interval.Finset.Gaps public import Mathlib.Order.Interval.Finset.Nat public import Mathlib.Order.Interval.Finset.SuccPred diff --git a/Mathlib/Algebra/Algebra/Equiv.lean b/Mathlib/Algebra/Algebra/Equiv.lean index 5ad24a529a..f423163bc8 100644 --- a/Mathlib/Algebra/Algebra/Equiv.lean +++ b/Mathlib/Algebra/Algebra/Equiv.lean @@ -777,6 +777,68 @@ end Semiring end AlgEquiv +namespace RingEquiv + +variable {R S : Type*} + +/-- Reinterpret a `RingEquiv` as an `ℕ`-algebra isomorphism. -/ +@[simps! -isSimp apply] +def toNatAlgEquiv [Semiring R] [Semiring S] (f : R ≃+* S) : R ≃ₐ[ℕ] S where + toEquiv := f + __ := f.toRingHom.toNatAlgHom + +@[simp] +lemma coe_toNatAlgEquiv [Semiring R] [Semiring S] (f : R ≃+* S) : + ⇑f.toNatAlgEquiv = ⇑f := rfl + +lemma toAlgHom_toNatAlgEquiv [Semiring R] [Semiring S] (f : R ≃+* S) : + f.toNatAlgEquiv.toAlgHom = (f : R →+* S).toNatAlgHom := rfl + +@[simp] +lemma symm_toNatAlgEquiv [Semiring R] [Semiring S] (f : R ≃+* S) : + f.toNatAlgEquiv.symm = f.symm.toNatAlgEquiv := rfl + +variable (R) (S) in +/-- The equivalence between `RingEquiv` and `ℕ`-algebra isomorphisms. -/ +@[simps apply symm_apply] +def equivNatAlgEquiv [Semiring R] [Semiring S] : (R ≃+* S) ≃ (R ≃ₐ[ℕ] S) where + toFun := toNatAlgEquiv + invFun := AlgEquiv.toRingEquiv + +lemma toNatAlgEquiv_injective [Semiring R] [Semiring S] : + Function.Injective (RingEquiv.toNatAlgEquiv : (R ≃+* S) → _) := + (equivNatAlgEquiv R S).injective + +/-- Reinterpret a `RingEquiv` as a `ℤ`-algebra isomorphism. -/ +@[simps! -isSimp apply] +def toIntAlgEquiv [Ring R] [Ring S] (f : R ≃+* S) : R ≃ₐ[ℤ] S where + toEquiv := f + __ := f.toRingHom.toIntAlgHom + +@[simp] +lemma coe_toIntAlgEquiv [Ring R] [Ring S] (f : R ≃+* S) : + ⇑f.toIntAlgEquiv = ⇑f := rfl + +lemma toAlgHom_toIntAlgEquiv [Ring R] [Ring S] (f : R ≃+* S) : + f.toIntAlgEquiv.toAlgHom = (f : R →+* S).toIntAlgHom := rfl + +@[simp] +lemma symm_toIntAlgEquiv [Ring R] [Ring S] (f : R ≃+* S) : + f.toIntAlgEquiv.symm = f.symm.toIntAlgEquiv := rfl + +variable (R) (S) in +/-- The equivalence between `RingEquiv` and `ℤ`-algebra isomorphisms. -/ +@[simps apply symm_apply] +def equivIntAlgEquiv [Ring R] [Ring S] : (R ≃+* S) ≃ (R ≃ₐ[ℤ] S) where + toFun := toIntAlgEquiv + invFun := AlgEquiv.toRingEquiv + +lemma toIntAlgEquiv_injective [Ring R] [Ring S] : + Function.Injective (RingEquiv.toIntAlgEquiv : (R ≃+* S) → _) := + (equivIntAlgEquiv R S).injective + +end RingEquiv + namespace MulSemiringAction variable {M G : Type*} (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] diff --git a/Mathlib/Algebra/Algebra/Hom/Rat.lean b/Mathlib/Algebra/Algebra/Hom/Rat.lean index 41fcb31b9d..cef17b3769 100644 --- a/Mathlib/Algebra/Algebra/Hom/Rat.lean +++ b/Mathlib/Algebra/Algebra/Hom/Rat.lean @@ -5,6 +5,7 @@ Authors: Kenny Lau, Yury Kudryashov -/ module +public import Mathlib.Algebra.Algebra.Equiv public import Mathlib.Algebra.Algebra.Hom public import Mathlib.Algebra.Algebra.Rat @@ -15,43 +16,77 @@ public import Mathlib.Algebra.Algebra.Rat @[expose] public section +variable {R S : Type*} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] namespace RingHom -variable {R S : Type*} - /-- Reinterpret a `RingHom` as a `ℚ`-algebra homomorphism. This actually yields an equivalence, see `RingHom.equivRatAlgHom`. -/ -def toRatAlgHom [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) : R →ₐ[ℚ] S := +def toRatAlgHom (f : R →+* S) : R →ₐ[ℚ] S := { f with commutes' := f.map_rat_algebraMap } @[simp] -theorem toRatAlgHom_toRingHom [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) : +theorem toRatAlgHom_toRingHom (f : R →+* S) : ↑f.toRatAlgHom = f := RingHom.ext fun _x => rfl @[simp] -theorem toRatAlgHom_apply [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) (x : R) : +theorem toRatAlgHom_apply (f : R →+* S) (x : R) : f.toRatAlgHom x = f x := rfl end RingHom -section - -variable {R S : Type*} - @[simp] -theorem AlgHom.toRingHom_toRatAlgHom [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] - (f : R →ₐ[ℚ] S) : (f : R →+* S).toRatAlgHom = f := +theorem AlgHom.toRingHom_toRatAlgHom (f : R →ₐ[ℚ] S) : (f : R →+* S).toRatAlgHom = f := AlgHom.ext fun _x => rfl variable (R) (S) in /-- The equivalence between `RingHom` and `ℚ`-algebra homomorphisms. -/ @[simps] -def RingHom.equivRatAlgHom [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] : - (R →+* S) ≃ (R →ₐ[ℚ] S) where +def RingHom.equivRatAlgHom : (R →+* S) ≃ (R →ₐ[ℚ] S) where toFun := RingHom.toRatAlgHom invFun := AlgHom.toRingHom -end +namespace RingEquiv + +/-- Reinterpret a `RingEquiv` as a `ℚ`-algebra isomorphism. This actually yields an +equivalence, see `RingEquiv.equivRatAlgEquiv`. -/ +@[simps! -isSimp apply] +def toRatAlgEquiv (f : R ≃+* S) : R ≃ₐ[ℚ] S where + toEquiv := f + __ := f.toRingHom.toRatAlgHom + +@[simp] +theorem coe_toRatAlgEquiv (f : R ≃+* S) : ⇑f.toRatAlgEquiv = ⇑f := rfl + +@[simp] +theorem toRingEquiv_toRatAlgEquiv (f : R ≃+* S) : + f.toRatAlgEquiv = f := + rfl + +theorem toAlgHom_toRatAlgEquiv (f : R ≃+* S) : + f.toRatAlgEquiv.toAlgHom = (f : R →+* S).toRatAlgHom := + rfl + +@[simp] +theorem symm_toRatAlgEquiv (f : R ≃+* S) : + f.toRatAlgEquiv.symm = f.symm.toRatAlgEquiv := + rfl + +end RingEquiv + +@[simp] +theorem AlgEquiv.toRatAlgEquiv_toRingEquiv (f : R ≃ₐ[ℚ] S) : (f : R ≃+* S).toRatAlgEquiv = f := + rfl + +variable (R) (S) in +/-- The equivalence between `RingEquiv` and `ℚ`-algebra isomorphisms. -/ +@[simps apply symm_apply] +def RingEquiv.equivRatAlgEquiv : (R ≃+* S) ≃ (R ≃ₐ[ℚ] S) where + toFun := RingEquiv.toRatAlgEquiv + invFun := AlgEquiv.toRingEquiv + +lemma RingEquiv.toRatAlgEquiv_injective : + Function.Injective (RingEquiv.toRatAlgEquiv : (R ≃+* S) → _) := + (RingEquiv.equivRatAlgEquiv R S).injective diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean index 18a69ab25d..5fa1fa1e91 100644 --- a/Mathlib/Algebra/Group/Subgroup/Basic.lean +++ b/Mathlib/Algebra/Group/Subgroup/Basic.lean @@ -316,6 +316,46 @@ instance botCharacteristic : Characteristic (⊥ : Subgroup G) := instance topCharacteristic : Characteristic (⊤ : Subgroup G) := characteristic_iff_map_le.mpr fun _ϕ => le_top +@[to_additive] +instance characteristic_sup [H.Characteristic] [K.Characteristic] : + (H ⊔ K).Characteristic := by + simp_all [characteristic_iff_map_eq, map_sup] + +@[to_additive] +instance characteristic_iSup {ι : Sort*} {H : ι → Subgroup G} [∀ i, (H i).Characteristic] : + (⨆ i, H i).Characteristic := by + simp_all [characteristic_iff_map_eq, map_iSup] + +@[to_additive] +theorem characteristic_biSup {ι : Type*} {s : Set ι} {H : ι → Subgroup G} + (h : ∀ i ∈ s, (H i).Characteristic) : (⨆ i ∈ s, H i).Characteristic := by + simp [← iSup_subtype'', characteristic_iSup, h] + +@[to_additive] +theorem characteristic_sSup {Hs : Set (Subgroup G)} (h : ∀ H ∈ Hs, H.Characteristic) : + (sSup Hs).Characteristic := by + simp [sSup_eq_iSup', characteristic_iSup, h] + +@[to_additive] +instance characteristic_inf [H.Characteristic] [K.Characteristic] : + (H ⊓ K).Characteristic := by + simp_all [characteristic_iff_comap_eq, comap_inf] + +@[to_additive] +instance characteristic_iInf {ι : Sort*} {H : ι → Subgroup G} [∀ i, (H i).Characteristic] : + (⨅ i, H i).Characteristic := by + simp_all [characteristic_iff_comap_eq, comap_iInf] + +@[to_additive] +theorem characteristic_biInf {ι : Type*} {s : Set ι} {H : ι → Subgroup G} + (h : ∀ i ∈ s, (H i).Characteristic) : (⨅ i ∈ s, H i).Characteristic := by + simp [← iInf_subtype'', characteristic_iInf, h] + +@[to_additive] +theorem characteristic_sInf {Hs : Set (Subgroup G)} (h : ∀ H ∈ Hs, H.Characteristic) : + (sInf Hs).Characteristic := by + simp [sInf_eq_iInf', characteristic_iInf, h] + /-- If `H` is a characteristic subgroup of `G`, then every automorphism of `G` induces an automorphism of `H`. -/ @[to_additive (attr := simps!) diff --git a/Mathlib/Analysis/Convex/Continuous.lean b/Mathlib/Analysis/Convex/Continuous.lean index b43a4a7564..5c6ace7d82 100644 --- a/Mathlib/Analysis/Convex/Continuous.lean +++ b/Mathlib/Analysis/Convex/Continuous.lean @@ -233,3 +233,96 @@ protected lemma ConcaveOn.locallyLipschitz (hf : ConcaveOn ℝ univ f) : Locally -- proof_wanted ConcaveOn.continuousOn_intrinsicInterior (hf : ConcaveOn ℝ C f) : -- ContinuousOn f (intrinsicInterior ℝ C) + +section Intervals + +lemma ConvexOn.continuousOn_Ici {f : ℝ → ℝ} {y : ℝ} (hf_cvx : ConvexOn ℝ (Ici y) f) + (hf_cont : ContinuousWithinAt f (Ici y) y) : + ContinuousOn f (Ici y) := by + intro x hx + rcases eq_or_lt_of_le (α := ℝ) hx with rfl | hxy + · exact hf_cont + · have h := hf_cvx.continuousOn_interior x + simp only [nonempty_Iio, interior_Ici', mem_Ioi] at h + rw [continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hxy)] at h + exact (h hxy).continuousWithinAt + +lemma ConcaveOn.continuousOn_Ici {f : ℝ → ℝ} {y : ℝ} (hf_cnv : ConcaveOn ℝ (Ici y) f) + (hf_cont : ContinuousWithinAt f (Ici y) y) : + ContinuousOn f (Ici y) := by + simpa using hf_cnv.neg.continuousOn_Ici hf_cont.neg + +lemma ConvexOn.continuousOn_Iic {f : ℝ → ℝ} {y : ℝ} (hf_cvx : ConvexOn ℝ (Iic y) f) + (hf_cont : ContinuousWithinAt f (Iic y) y) : + ContinuousOn f (Iic y) := by + intro x hx + rcases eq_or_lt_of_le (α := ℝ) hx with rfl | hxy + · exact hf_cont + · have h := hf_cvx.continuousOn_interior x + simp only [nonempty_Ioi, interior_Iic', mem_Iio] at h + rw [continuousWithinAt_iff_continuousAt (Iio_mem_nhds hxy)] at h + exact (h hxy).continuousWithinAt + +lemma ConcaveOn.continuousOn_Iic {f : ℝ → ℝ} {y : ℝ} (hf_cnv : ConcaveOn ℝ (Iic y) f) + (hf_cont : ContinuousWithinAt f (Iic y) y) : + ContinuousOn f (Iic y) := by + simpa using hf_cnv.neg.continuousOn_Iic hf_cont.neg + +lemma ConvexOn.continuousOn_Ioc {f : ℝ → ℝ} {y z : ℝ} (hf_cvx : ConvexOn ℝ (Ioc y z) f) + (hf_cont : ContinuousWithinAt f (Iic z) z) : + ContinuousOn f (Ioc y z) := by + intro x hx + rcases eq_or_lt_of_le (α := ℝ) hx.2 with rfl | hxz + · rw [continuousWithinAt_Ioc_iff_Iic hx.1] + exact hf_cont + · have h := hf_cvx.continuousOn_interior x + simp only [interior_Ioc, mem_Ioo, hx.1, hxz, and_self, forall_const] at h + rw [continuousWithinAt_iff_continuousAt (Ioo_mem_nhds hx.1 hxz)] at h + exact h.continuousWithinAt + +lemma ConcaveOn.continuousOn_Ioc {f : ℝ → ℝ} {y z : ℝ} (hf_cnv : ConcaveOn ℝ (Ioc y z) f) + (hf_cont : ContinuousWithinAt f (Iic z) z) : + ContinuousOn f (Ioc y z) := by + simpa using hf_cnv.neg.continuousOn_Ioc hf_cont.neg + +lemma ConvexOn.continuousOn_Ico {f : ℝ → ℝ} {y z : ℝ} (hf_cvx : ConvexOn ℝ (Ico y z) f) + (hf_cont : ContinuousWithinAt f (Ici y) y) : + ContinuousOn f (Ico y z) := by + intro x hx + rcases eq_or_lt_of_le (α := ℝ) hx.1 with rfl | hyx + · rw [continuousWithinAt_Ico_iff_Ici hx.2] + exact hf_cont + · have h := hf_cvx.continuousOn_interior x + simp only [interior_Ico, mem_Ioo, hyx, hx.2, and_self, forall_const] at h + rw [continuousWithinAt_iff_continuousAt (Ioo_mem_nhds hyx hx.2)] at h + exact h.continuousWithinAt + +lemma ConcaveOn.continuousOn_Ico {f : ℝ → ℝ} {y z : ℝ} (hf_cnv : ConcaveOn ℝ (Ico y z) f) + (hf_cont : ContinuousWithinAt f (Ici y) y) : + ContinuousOn f (Ico y z) := by + simpa using hf_cnv.neg.continuousOn_Ico hf_cont.neg + +lemma ConvexOn.continuousOn_Icc {f : ℝ → ℝ} {y z : ℝ} (hf_cvx : ConvexOn ℝ (Icc y z) f) + (hyz : y < z) + (hfy : ContinuousWithinAt f (Ici y) y) (hfz : ContinuousWithinAt f (Iic z) z) : + ContinuousOn f (Icc y z) := by + suffices ContinuousOn f (Ico y z) ∧ ContinuousOn f (Ioc y z) by + intro x hx + rcases eq_or_lt_of_le (α := ℝ) hx.1 with rfl | hyx + · exact hfy.mono (by grind) + rcases eq_or_lt_of_le (α := ℝ) hx.2 with rfl | hxz + · exact hfz.mono (by grind) + have hx := this.1 x (by grind) + rw [continuousWithinAt_iff_continuousAt (Ico_mem_nhds hyx hxz)] at hx + exact hx.continuousWithinAt + refine ⟨ConvexOn.continuousOn_Ico ?_ hfy, ConvexOn.continuousOn_Ioc ?_ hfz⟩ + · exact hf_cvx.subset Ico_subset_Icc_self (convex_Ico y z) + · exact hf_cvx.subset Ioc_subset_Icc_self (convex_Ioc y z) + +lemma ConcaveOn.continuousOn_Icc {f : ℝ → ℝ} {y z : ℝ} (hf_cnv : ConcaveOn ℝ (Icc y z) f) + (hyz : y < z) + (hfy : ContinuousWithinAt f (Ici y) y) (hfz : ContinuousWithinAt f (Iic z) z) : + ContinuousOn f (Icc y z) := by + simpa using hf_cnv.neg.continuousOn_Icc hyz hfy.neg hfz.neg + +end Intervals diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index d9ed9660d2..c7bddb2183 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -68,8 +68,6 @@ namespace ContinuousLinearMap variable [CompleteSpace E] [CompleteSpace G] --- Note: made noncomputable to stop excess compilation --- https://github.com/leanprover-community/mathlib4/issues/7103 /-- The adjoint, as a continuous conjugate-linear map. This is only meant as an auxiliary definition for the main definition `adjoint`, where this is bundled as a conjugate-linear isometric equivalence. -/ diff --git a/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean new file mode 100644 index 0000000000..1bb7d526df --- /dev/null +++ b/Mathlib/Analysis/InnerProductSpace/ExteriorPower.lean @@ -0,0 +1,155 @@ +/- +Copyright (c) 2026 Justus Springer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Justus Springer +-/ +module + +public import Mathlib.Analysis.InnerProductSpace.GramMatrix +public import Mathlib.LinearAlgebra.ExteriorPower.Basis + +/-! +# Inner product space structure on exterior powers + +Given a real inner product space `E`, we construct a canonical inner product on `⋀[ℝ]^n E` +via the Gram determinant formula: on decomposable elements, +`⟪v₁ ∧ ⋯ ∧ vₙ, w₁ ∧ ⋯ ∧ wₙ⟫ = det (⟪vⱼ, wᵢ⟫)ᵢⱼ`. + +## Main results + +- `exteriorPower.inner_ιMulti_ιMulti`: The inner product on decomposable elements equals the + Gram determinant. +- `exteriorPower.inner_ιMulti_self`: `⟪v₁ ∧ ⋯ ∧ vₙ, v₁ ∧ ⋯ ∧ vₙ⟫ = det (gram ℝ v)`. +- `OrthonormalBasis.exteriorPower`: An orthonormal basis of `E` induces an orthonormal basis + of `⋀[ℝ]^n E`. + +## Future work + +- Generalize to `RCLike 𝕜`. To define `innerProductForm` in this case, we would probably + want a semilinear generalization of `exteriorPower.map`, which in turn requires + generalizing `AlternatingMap` to the semilinear setting. +- Remove the `FiniteDimensional` hypothesis from the `InnerProductSpace` instance. + Currently the proofs of `re_inner_nonneg` and `definite` require finite dimension, because + we need to choose an orthonormal basis of `E`. But we can reduce the general case to + the finite-dimensional case by noticing that any `x : ⋀[𝕜]^n E` is contained in some + `⋀[𝕜]^n F` for a finite-dimensional subspace `F ≤ E`. + +-/ + +@[expose] public noncomputable section + +namespace exteriorPower + +open RealInnerProductSpace Matrix + +variable {n : ℕ} {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- The inner product on `⋀[ℝ]^n E` as a bilinear map. This is an implementation detail +for constructing the `InnerProductSpace` instance and should not be used directly. +Use `⟪·, ·⟫` instead. -/ +private def innerProductForm : ⋀[ℝ]^n E →ₗ[ℝ] ⋀[ℝ]^n E →ₗ[ℝ] ℝ := + pairingDual ℝ E n ∘ₗ map n (innerₗ E) + +private lemma innerProductForm_ιMulti_ιMulti (x y : Fin n → E) : + innerProductForm (ιMulti ℝ n x) (ιMulti ℝ n y) = det (of fun i j ↦ ⟪x j, y i⟫) := by + simp [innerProductForm] + +@[simp] +private lemma innerProductForm_ιMulti_self (x : Fin n → E) : + innerProductForm (ιMulti ℝ n x) (ιMulti ℝ n x) = det (gram ℝ x) := by + simp [gram, innerProductForm_ιMulti_ιMulti, real_inner_comm] + +private lemma flip_innerProductForm : + (innerProductForm (E := E) (n := n)).flip = innerProductForm := by + apply linearMap_ext + ext + simp only [LinearMap.compAlternatingMap_apply, LinearMap.flip_apply, + innerProductForm_ιMulti_ιMulti] + rw [← Matrix.det_transpose] + congr 1 + ext + exact real_inner_comm _ _ + +private lemma innerProductForm_symm (x y : ⋀[ℝ]^n E) : + innerProductForm y x = innerProductForm x y := + congr($flip_innerProductForm x y) + +@[simp] +private lemma innerProductForm_ιMulti_family_of_orthonormal {ι : Type*} [LinearOrder ι] {v : ι → E} + (hv : Orthonormal ℝ v) (s t : Set.powersetCard ι n) : + innerProductForm (ιMulti_family ℝ n v s) (ιMulti_family ℝ n v t) = if s = t then 1 else 0 := by + simp only [ιMulti_family] + split_ifs with h + · subst h + simp [gram_eq_one_iff_orthonormal.mpr (hv.comp _ (RelEmbedding.injective _))] + · rw [innerProductForm_ιMulti_ιMulti] + obtain ⟨x, hxt, hxs⟩ := (Set.powersetCard.exists_mem_notMem_iff_ne t s).mp (.symm h) + simp only [Set.mem_range, not_exists, + ← Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem] at hxs hxt + obtain ⟨i, rfl⟩ := hxt + exact det_eq_zero_of_row_eq_zero i (fun j ↦ hv.inner_eq_zero (hxs j)) + +private lemma innerProductForm_eq_sum {ι : Type*} [Fintype ι] [LinearOrder ι] + (b : OrthonormalBasis ι ℝ E) (x y : ⋀[ℝ]^n E) : + innerProductForm x y = + ∑ s, (b.toBasis.exteriorPower n).repr y s * (b.toBasis.exteriorPower n).repr x s := by + conv_lhs => + rw [← (b.toBasis.exteriorPower n).sum_repr x, ← (b.toBasis.exteriorPower n).sum_repr y] + simp + +private lemma innerProductForm_self (x : ⋀[ℝ]^n E) {ι : Type*} [Fintype ι] [LinearOrder ι] + (b : OrthonormalBasis ι ℝ E) : + innerProductForm x x = ∑ s, (b.toBasis.exteriorPower n).repr x s ^ 2 := by + simp_rw [innerProductForm_eq_sum b, pow_two] + +@[no_expose] instance [FiniteDimensional ℝ E] : InnerProductSpace.Core ℝ (⋀[ℝ]^n E) where + inner x y := innerProductForm x y + conj_inner_symm := innerProductForm_symm + add_left := by simp + smul_left := by simp + re_inner_nonneg x := by + rw [innerProductForm_self x (stdOrthonormalBasis ℝ E)] + exact Finset.sum_nonneg (fun _ _ ↦ sq_nonneg _) + definite x h := by + rw [innerProductForm_self x (stdOrthonormalBasis ℝ E), + Finset.sum_eq_zero_iff_of_nonneg (fun _ _ ↦ sq_nonneg _)] at h + apply Module.Basis.ext_elem ((stdOrthonormalBasis ℝ E).toBasis.exteriorPower n) + simpa using h + +instance [FiniteDimensional ℝ E] : NormedAddCommGroup (⋀[ℝ]^n E) := + InnerProductSpace.Core.toNormedAddCommGroup (𝕜 := ℝ) + +instance [FiniteDimensional ℝ E] : InnerProductSpace ℝ (⋀[ℝ]^n E) := + InnerProductSpace.ofCore _ + +lemma inner_ιMulti_ιMulti [FiniteDimensional ℝ E] (x y : Fin n → E) : + ⟪ιMulti ℝ n x, ιMulti ℝ n y⟫ = det (of fun i j ↦ ⟪x j, y i⟫) := + innerProductForm_ιMulti_ιMulti x y + +lemma inner_ιMulti_self [FiniteDimensional ℝ E] (x : Fin n → E) : + ⟪ιMulti ℝ n x, ιMulti ℝ n x⟫ = det (gram ℝ x) := + innerProductForm_ιMulti_self x + +end exteriorPower + +section OrthonormalBasis + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] +variable {I : Type*} [Fintype I] [LinearOrder I] + +/-- An orthonormal basis of a finite-dimensional real inner product space `E` induces an +orthonormal basis of `⋀[ℝ]^n E`, indexed by `n`-element subsets of the index type. -/ +def OrthonormalBasis.exteriorPower (b : OrthonormalBasis I ℝ E) (n : ℕ) : + OrthonormalBasis (Set.powersetCard I n) ℝ (⋀[ℝ]^n E) := + (b.toBasis.exteriorPower n).toOrthonormalBasis <| by + rw [orthonormal_iff_ite] + intro i j + rw [exteriorPower.coe_basis, OrthonormalBasis.coe_toBasis] + exact exteriorPower.innerProductForm_ιMulti_family_of_orthonormal b.orthonormal i j + +@[simp] +lemma OrthonormalBasis.toBasis_exteriorPower (b : OrthonormalBasis I ℝ E) (n : ℕ) : + (b.exteriorPower n).toBasis = b.toBasis.exteriorPower n := + (b.toBasis.exteriorPower n).toBasis_toOrthonormalBasis _ + +end OrthonormalBasis diff --git a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean index 5137d3a797..7bc693a2dd 100644 --- a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean +++ b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean @@ -134,6 +134,11 @@ theorem gram_eq_conjTranspose_mul {ι : Type*} [Fintype ι] (b : OrthonormalBasi ext i j simp [mul_apply, b.repr_apply_apply, b.sum_inner_mul_inner] +omit [Finite n] in +@[simp] +lemma gram_eq_one_iff_orthonormal [DecidableEq n] {v : n → E} : gram 𝕜 v = 1 ↔ Orthonormal 𝕜 v := by + simp [← Matrix.ext_iff, orthonormal_iff_ite, Matrix.one_apply] + omit [Finite n] in /-- Inequality `‖f x‖ ≤ ‖f‖ * ‖x‖` lifted to Gram matrices. -/ theorem posSemidef_opNorm_smul_gram_sub_gram {F} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean index 6c642b86a8..da5718034d 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean @@ -178,15 +178,6 @@ open Complex variable {f g : ℂ → ℂ} {s : Set ℂ} {f' g' x c : ℂ} -/-- A private lemma that rewrites the output of lemmas like `HasFDerivAt.cpow` to the form -expected by lemmas like `HasDerivAt.cpow`. -/ -private theorem aux : ((g x * f x ^ (g x - 1)) • (1 : ℂ →L[ℂ] ℂ).smulRight f' + - (f x ^ g x * log (f x)) • (1 : ℂ →L[ℂ] ℂ).smulRight g') 1 = - g x * f x ^ (g x - 1) * f' + f x ^ g x * log (f x) * g' := by - simp only [smul_eq_mul, one_mul, one_apply_eq_self, - ContinuousLinearMap.smulRight_apply, add_apply, Pi.smul_apply, - FunLike.coe_smul'] - nonrec theorem HasStrictDerivAt.cpow (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) (h0 : f x ∈ slitPlane) : HasStrictDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x := by @@ -209,7 +200,7 @@ theorem HasStrictDerivAt.cpow_const (hf : HasStrictDerivAt f f' x) theorem HasDerivAt.cpow (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) (h0 : f x ∈ slitPlane) : HasDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x := by - simpa [aux] using (hf.hasFDerivAt.cpow hg h0).hasDerivAt + simpa using (hf.hasFDerivAt.cpow hg h0).hasDerivAt theorem HasDerivAt.const_cpow (hf : HasDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0) : HasDerivAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') x := @@ -222,7 +213,7 @@ theorem HasDerivAt.cpow_const (hf : HasDerivAt f f' x) (h0 : f x ∈ slitPlane) theorem HasDerivWithinAt.cpow (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) (h0 : f x ∈ slitPlane) : HasDerivWithinAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x := by - simpa [aux] using (hf.hasFDerivWithinAt.cpow hg h0).hasDerivWithinAt + simpa using (hf.hasFDerivWithinAt.cpow hg h0).hasDerivWithinAt theorem HasDerivWithinAt.const_cpow (hf : HasDerivWithinAt f f' s x) (h0 : c ≠ 0 ∨ f x ≠ 0) : HasDerivWithinAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') s x := diff --git a/Mathlib/CategoryTheory/Limits/Comma.lean b/Mathlib/CategoryTheory/Limits/Comma.lean index 533ff3d5c6..95a6c9e6df 100644 --- a/Mathlib/CategoryTheory/Limits/Comma.lean +++ b/Mathlib/CategoryTheory/Limits/Comma.lean @@ -72,24 +72,39 @@ noncomputable def coneOfPreserves [PreservesLimit (F ⋙ snd L R) R] (c₁ : Con · simp [← c₂.w t] } set_option backward.isDefEq.respectTransparency false in +set_option backward.defeqAttrib.useBackward true in +/-- Let `F : J ⥤ Comma L R`. If `R` preserves the limit of +`F ⋙ snd _ _`, then `Comma.fst L R` and `Comma.snd L R` jointly +reflect the limit of `F`, i.e. if `c` is a cone for `F` which +becomes a limit after applying `Comma.fst L R` and `Comma.snd L R`, +then `c` is a limit. -/ +def fstSndJointlyReflectLimit {F : J ⥤ Comma L R} {c : Cone F} + [PreservesLimit (F ⋙ snd _ _) R] + (h₁ : IsLimit ((fst _ _).mapCone c)) + (h₂ : IsLimit ((snd _ _).mapCone c)) : + IsLimit c where + lift s := + { left := h₁.lift ((fst _ _).mapCone s) + right := h₂.lift ((snd _ _).mapCone s) + w := (isLimitOfPreserves R h₂).hom_ext (fun j ↦ by + simp [← Functor.map_comp, ← Functor.map_comp_assoc, ← CommaMorphism.w, + dsimp% h₂.fac ((snd _ _).mapCone s) j, + dsimp% h₁.fac ((fst _ _).mapCone s) j]) } + fac s j := by + ext + · exact h₁.fac ((fst _ _).mapCone s) j + · exact h₂.fac ((snd _ _).mapCone s) j + uniq s _ hm := by + ext + · exact h₁.uniq ((fst _ _).mapCone s) _ (by simp [← hm]) + · exact h₂.uniq ((snd _ _).mapCone s) _ (by simp [← hm]) + /-- Provided that `R` preserves the appropriate limit, then the cone in `coneOfPreserves` is a limit. -/ noncomputable def coneOfPreservesIsLimit [PreservesLimit (F ⋙ snd L R) R] {c₁ : Cone (F ⋙ fst L R)} (t₁ : IsLimit c₁) {c₂ : Cone (F ⋙ snd L R)} (t₂ : IsLimit c₂) : - IsLimit (coneOfPreserves F c₁ t₂) where - lift s := - { left := t₁.lift ((fst L R).mapCone s) - right := t₂.lift ((snd L R).mapCone s) - w := - (isLimitOfPreserves R t₂).hom_ext fun j => by - rw [coneOfPreserves_pt_hom, assoc, assoc, (isLimitOfPreserves R t₂).fac, - limitAuxiliaryCone_π_app, ← L.map_comp_assoc, t₁.fac, R.mapCone_π_app, - ← R.map_comp, t₂.fac] - exact (s.π.app j).w } - uniq s m w := by - apply CommaMorphism.ext - · exact t₁.uniq ((fst L R).mapCone s) _ (fun j => by simp [← w]) - · exact t₂.uniq ((snd L R).mapCone s) _ (fun j => by simp [← w]) + IsLimit (coneOfPreserves F c₁ t₂) := + fstSndJointlyReflectLimit t₁ t₂ /-- (Implementation). An auxiliary cocone which is useful in order to construct colimits in the comma category. -/ @@ -121,25 +136,40 @@ noncomputable def coconeOfPreserves [PreservesColimit (F ⋙ fst L R) L] {c₁ : · simp [← c₂.w t] } set_option backward.isDefEq.respectTransparency false in +set_option backward.defeqAttrib.useBackward true in +/-- Let `F : J ⥤ Comma L R`. If `L` preserves the colimit of +`F ⋙ fst _ _`, then `Comma.fst L R` and `Comma.snd L R` jointly +reflect the colimit of `F`, i.e. if `c` is a cocone for `F` which +becomes a colimit after applying `Comma.fst L R` and `Comma.snd L R`, +then `c` is a colimit. -/ +def fstSndJointlyReflectColimit {F : J ⥤ Comma L R} {c : Cocone F} + [PreservesColimit (F ⋙ fst _ _) L] + (h₁ : IsColimit ((fst _ _).mapCocone c)) + (h₂ : IsColimit ((snd _ _).mapCocone c)) : + IsColimit c where + desc s := + { left := h₁.desc ((fst _ _).mapCocone s) + right := h₂.desc ((snd _ _).mapCocone s) + w := (isColimitOfPreserves L h₁).hom_ext (fun j ↦ by + simp [← Functor.map_comp_assoc, ← Functor.map_comp, + dsimp% h₁.fac ((fst _ _).mapCocone s) j, + dsimp% h₂.fac ((snd _ _).mapCocone s) j]) } + fac s j := by + ext + · exact h₁.fac ((fst _ _).mapCocone s) j + · exact h₂.fac ((snd _ _).mapCocone s) j + uniq s _ hm := by + ext + · exact h₁.uniq ((fst _ _).mapCocone s) _ (by simp [← hm]) + · exact h₂.uniq ((snd _ _).mapCocone s) _ (by simp [← hm]) + /-- Provided that `L` preserves the appropriate colimit, then the cocone in `coconeOfPreserves` is a colimit. -/ noncomputable def coconeOfPreservesIsColimit [PreservesColimit (F ⋙ fst L R) L] {c₁ : Cocone (F ⋙ fst L R)} (t₁ : IsColimit c₁) {c₂ : Cocone (F ⋙ snd L R)} (t₂ : IsColimit c₂) : - IsColimit (coconeOfPreserves F t₁ c₂) where - desc s := - { left := t₁.desc ((fst L R).mapCocone s) - right := t₂.desc ((snd L R).mapCocone s) - w := - (isColimitOfPreserves L t₁).hom_ext fun j => by - rw [coconeOfPreserves_pt_hom, (isColimitOfPreserves L t₁).fac_assoc, - colimitAuxiliaryCocone_ι_app, assoc, ← R.map_comp, t₂.fac, L.mapCocone_ι_app, ← - L.map_comp_assoc, t₁.fac] - exact (s.ι.app j).w } - uniq s m w := by - apply CommaMorphism.ext - · exact t₁.uniq ((fst L R).mapCocone s) _ (fun j => by simp [← w]) - · exact t₂.uniq ((snd L R).mapCocone s) _ (fun j => by simp [← w]) + IsColimit (coconeOfPreserves F t₁ c₂) := + fstSndJointlyReflectColimit t₁ t₂ instance hasLimit (F : J ⥤ Comma L R) [HasLimit (F ⋙ fst L R)] [HasLimit (F ⋙ snd L R)] [PreservesLimit (F ⋙ snd L R) R] : HasLimit F := diff --git a/Mathlib/Combinatorics/Quiver/Path.lean b/Mathlib/Combinatorics/Quiver/Path.lean index ddd9d524ee..0795ef0ea0 100644 --- a/Mathlib/Combinatorics/Quiver/Path.lean +++ b/Mathlib/Combinatorics/Quiver/Path.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2021 David Wärn,. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: David Wärn, Kim Morrison, Matteo Cipollina +Authors: David Wärn, Kim Morrison, Matteo Cipollina, Runtian Zhou -/ module @@ -14,6 +14,8 @@ public import Batteries.Data.List.Basic Given a quiver `V`, we define the type of paths from `a : V` to `b : V` as an inductive family. We define composition of paths and the action of prefunctors on paths. + +We also define `Quiver.Reachable a b`, the existence of a directed path from `a` to `b`. -/ @[expose] public section @@ -309,6 +311,43 @@ end BoundedPath end Path +section Reachable + +variable {V : Type u} [Quiver V] + +/-- `Reachable a b` holds when there is a directed path from `a` to `b`. + +This is a preorder rather than an equivalence, since quiver paths are directed (compare the +symmetric `SimpleGraph.Reachable`). -/ +def Reachable (a b : V) : Prop := Nonempty (Path a b) + +variable {a b c : V} + +protected theorem Reachable.elim {p : Prop} (h : Reachable a b) (hp : Path a b → p) : p := + Nonempty.elim h hp + +@[refl] +protected theorem Reachable.refl (a : V) : Reachable a a := ⟨.nil⟩ + +@[simp] +protected theorem Reachable.rfl : Reachable a a := .refl _ + +@[trans] +protected theorem Reachable.trans (hab : Reachable a b) (hbc : Reachable b c) : Reachable a c := + hab.elim fun p => hbc.elim fun q => ⟨p.comp q⟩ + +instance : IsPreorder V Reachable where + refl := .refl + trans _ _ _ := .trans + +/-- A path witnesses that its target is reachable from its source. -/ +protected theorem Path.reachable (p : Path a b) : Reachable a b := ⟨p⟩ + +/-- An arrow witnesses that its target is reachable from its source. -/ +protected theorem Hom.reachable (e : a ⟶ b) : Reachable a b := ⟨e.toPath⟩ + +end Reachable + end Quiver namespace Prefunctor diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean index c2b8107c55..f6adc4c39b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean @@ -821,6 +821,32 @@ theorem disjoint_neighborSet : (∀ v, Disjoint (G.neighborSet v) (H.neighborSet v)) ↔ Disjoint G H := by simp_rw [← disjoint_edgeSet, Set.disjoint_left, mem_neighborSet, Sym2.forall, mem_edgeSet] +@[simp] +theorem neighborSet_sup {G₁ G₂ : SimpleGraph V} (v : V) : + (G₁ ⊔ G₂).neighborSet v = G₁.neighborSet v ∪ G₂.neighborSet v := + rfl + +@[simp] +theorem neighborSet_inf {G₁ G₂ : SimpleGraph V} (v : V) : + (G₁ ⊓ G₂).neighborSet v = G₁.neighborSet v ∩ G₂.neighborSet v := + rfl + +@[simp] +theorem neighborSet_sdiff {G₁ G₂ : SimpleGraph V} (v : V) : + (G₁ \ G₂).neighborSet v = G₁.neighborSet v \ G₂.neighborSet v := + rfl + +@[simp] +theorem neighborSet_iSup {s : ι → SimpleGraph V} (v : V) : + (⨆ i, s i).neighborSet v = ⋃ i, (s i).neighborSet v := by + ext; simp + +@[simp] +theorem neighborSet_iInf [Nonempty ι] {s : ι → SimpleGraph V} (v : V) : + (⨅ i, s i).neighborSet v = ⋂ i, (s i).neighborSet v := by + ext + simp_rw [Set.mem_iInter, mem_neighborSet, iInf_adj_of_nonempty] + @[simp] theorem mem_incidenceSet (v w : V) : s(v, w) ∈ G.incidenceSet v ↔ G.Adj v w := by simp [incidenceSet] diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean index 7f557583f5..3c7e0f8564 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Finite.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Finite.lean @@ -186,6 +186,45 @@ theorem neighborFinset_disjoint_singleton : Disjoint (G.neighborFinset v) {v} := theorem singleton_disjoint_neighborFinset : Disjoint {v} (G.neighborFinset v) := Finset.disjoint_singleton_left.mpr <| notMem_neighborFinset_self _ _ +theorem neighborFinset_bot [Fintype ((⊥ : SimpleGraph V).neighborSet v)] : + (⊥ : SimpleGraph V).neighborFinset v = ∅ := by + ext; simp + +@[simp] +theorem neighborFinset_top [Fintype V] [DecidableEq V] : + (⊤ : SimpleGraph V).neighborFinset v = {v}ᶜ := by + simp [← Finset.coe_inj] + +@[simp] +theorem neighborFinset_sup [DecidableEq V] {G₁ G₂ : SimpleGraph V} + [Fintype ((G₁ ⊔ G₂).neighborSet v)] [Fintype (G₁.neighborSet v)] [Fintype (G₂.neighborSet v)] : + (G₁ ⊔ G₂).neighborFinset v = G₁.neighborFinset v ∪ G₂.neighborFinset v := by + simp [← Finset.coe_inj] + +@[simp] +theorem neighborFinset_inf [DecidableEq V] {G₁ G₂ : SimpleGraph V} + [Fintype ((G₁ ⊓ G₂).neighborSet v)] [Fintype (G₁.neighborSet v)] [Fintype (G₂.neighborSet v)] : + (G₁ ⊓ G₂).neighborFinset v = G₁.neighborFinset v ∩ G₂.neighborFinset v := by + simp [← Finset.coe_inj] + +@[simp] +theorem neighborFinset_sdiff [DecidableEq V] {G₁ G₂ : SimpleGraph V} + [Fintype ((G₁ \ G₂).neighborSet v)] [Fintype (G₁.neighborSet v)] [Fintype (G₂.neighborSet v)] : + (G₁ \ G₂).neighborFinset v = G₁.neighborFinset v \ G₂.neighborFinset v := by + simp [← Finset.coe_inj] + +theorem disjoint_neighborFinset_of_disjoint [Fintype <| H.neighborSet v] (h : Disjoint G H) : + Disjoint (G.neighborFinset v) (H.neighborFinset v) := by + simp [← Finset.disjoint_coe, disjoint_neighborSet.mpr h v] + +theorem neighborFinset_sup_of_disjoint {G₁ G₂ : SimpleGraph V} + [Fintype ((G₁ ⊔ G₂).neighborSet v)] [Fintype (G₁.neighborSet v)] [Fintype (G₂.neighborSet v)] + (h : Disjoint G₁ G₂) : + (G₁ ⊔ G₂).neighborFinset v = + (G₁.neighborFinset v).disjUnion (G₂.neighborFinset v) + (disjoint_neighborFinset_of_disjoint G₁ G₂ v h) := by + simp [← Finset.coe_inj, Finset.coe_disjUnion] + @[simp] lemma neighborFinset_eq_empty : G.neighborFinset v = ∅ ↔ G.IsIsolated v := by simp [neighborFinset, IsIsolated, Set.ext_iff] @@ -197,10 +236,6 @@ protected alias ⟨IsIsolated.of_neighborFinset_eq_empty, IsIsolated.neighborFin attribute [simp] IsIsolated.neighborFinset_eq_empty -theorem disjoint_neighborFinset_of_disjoint [Fintype <| H.neighborSet v] (h : Disjoint G H) : - Disjoint (G.neighborFinset v) (H.neighborFinset v) := by - simp [← Finset.disjoint_coe, disjoint_neighborSet.mpr h v] - /-- `G.degree v` is the number of vertices adjacent to `v`. -/ def degree : ℕ := #(G.neighborFinset v) @@ -680,6 +715,20 @@ theorem le_minDegree_induce_of_support_subset (h : G.support ⊆ s) : grw [G.minDegree_le_degree v, degree_induce_of_neighborSet_subset] grw [neighborSet_subset_support, h] +theorem filter_edgeFinset_toFinset_subset [DecidableEq V] (s : Finset V) : + {e ∈ G.edgeFinset | e.toFinset ⊆ s} = G.edgeFinset ∩ s.sym2 := by + simp [subset_iff, ← mem_sym2_iff, filter_mem_eq_inter] + +/-- The edges whose vertices lie in `s` are in bijection with the edges of the induced +subgraph `G.induce s`. -/ +theorem card_filter_edgeFinset_toFinset_subset [DecidableEq V] (s : Finset V) : + #{e ∈ G.edgeFinset | e.toFinset ⊆ s} = #(G.induce ↑s).edgeFinset := by + have h := congrArg Finset.card (map_edgeFinset_induce (s := (↑s : Set V)) (G := G)) + rw [card_map, toFinset_coe] at h + rw [filter_edgeFinset_toFinset_subset] + convert h.symm using 1 + congr! + end Support section Map diff --git a/Mathlib/Data/FunLike/IsApply.lean b/Mathlib/Data/FunLike/IsApply.lean index e8848acbce..8136659ac2 100644 --- a/Mathlib/Data/FunLike/IsApply.lean +++ b/Mathlib/Data/FunLike/IsApply.lean @@ -204,7 +204,7 @@ variable {M M' F F' α β : Type*} [FunLike F α β] [FunLike F' α α] section Coercion -@[to_additive (attr := norm_cast)] +@[to_additive (attr := simp, norm_cast)] theorem coe_one [One F] [One β] [IsOneApply F α β] : ↑(1 : F) = (1 : α → β) := by ext; simp @[to_additive (attr := simp)] @@ -213,67 +213,73 @@ theorem coe_one_iff [One F] [One β] [IsOneApply F α β] (f : F) : (f : α → · intro h simp [DFunLike.ext_iff, h] · intro h - simp [funext_iff, h] + simp [h] -@[to_additive (attr := norm_cast)] +@[to_additive (attr := simp, norm_cast)] theorem coe_mul [Mul F] [Mul β] [IsMulApply F α β] (f g : F) : ↑(f * g) = (f : α → β) * g := by ext; simp -@[to_additive (attr := norm_cast)] +@[to_additive (attr := simp, norm_cast)] theorem coe_div [Div F] [Div β] [IsDivApply F α β] (f g : F) : ↑(f / g) = (f : α → β) / g := by ext; simp -@[to_additive (attr := norm_cast)] +@[to_additive (attr := simp, norm_cast)] theorem coe_inv [Inv F] [Inv β] [IsInvApply F α β] (f : F) : ↑(f⁻¹) = (f : α → β)⁻¹ := by ext; simp -@[to_additive (attr := norm_cast)] +@[to_additive (attr := simp, norm_cast)] theorem coe_smul [SMul M F] [SMul M β] [IsSMulApply M F α β] (n : M) (f : F) : ↑(n • f) = n • (f : α → β) := by ext; simp -@[to_additive coe_smul'] +@[deprecated (since := "2026-07-23")] alias coe_smul' := coe_smul + +@[simp, norm_cast, to_additive existing coe_smul] theorem coe_pow [Pow F M] [Pow β M] [IsPowApply M F α β] (f : F) (n : M) : ↑(f ^ n) = (f : α → β) ^ n := by ext; simp -attribute [norm_cast] coe_pow - -@[norm_cast] +@[simp, norm_cast] theorem coe_one_eq_id [One F'] [IsOneApplyEqSelf F' α] : ↑(1 : F') = id := by ext; simp -@[simp] +@[simp, norm_cast] theorem coe_one_eq_id_iff [One F'] [IsOneApplyEqSelf F' α] (f : F') : (f : α → α) = id ↔ f = 1 := by constructor · intro h simp [DFunLike.ext_iff, h] · intro h - simp [funext_iff, h] + simp [h] -@[norm_cast] +@[simp, norm_cast] theorem coe_mul_eq_comp [Mul F'] [IsMulApplyEqComp F' α] (f g : F') : ↑(f * g) = f ∘ g := by ext; simp -@[norm_cast] +@[simp, norm_cast] lemma coe_pow_eq_iterate [Monoid F'] [IsMulApplyEqComp F' α] [IsOneApplyEqSelf F' α] (f : F') (n : ℕ) : ⇑(f ^ n) = f^[n] := funext <| pow_apply_eq_iterate f n +-- this lemma cannot be `simp` since this creates loops @[norm_cast] -theorem coe_natCast [NatCast F'] [One F'] [SMul Nat α] [SMul Nat F'] [IsSMulApply Nat F' α α] - [IsNatCastApply F' α] [IsOneApplyEqSelf F' α] (n : Nat) : +theorem natCast_eq_nsmul_one [NatCast F'] [One F'] [SMul Nat α] [SMul Nat F'] + [IsSMulApply Nat F' α α] [IsNatCastApply F' α] [IsOneApplyEqSelf F' α] (n : ℕ) : (n : F') = n • (1 : F') := by apply DFunLike.ext simp +@[deprecated (since := "2026-07-24")] alias coe_natCast := natCast_eq_nsmul_one + +-- this lemma cannot be `simp` since this creates loops @[norm_cast] -theorem coe_intCast [IntCast F'] [One F'] [SMul Int α] [SMul Int F'] [IsSMulApply Int F' α α] - [IsIntCastApply F' α] [IsOneApplyEqSelf F' α] (n : Int) : +theorem intCast_eq_zsmul_one [IntCast F'] [One F'] [SMul Int α] [SMul Int F'] + [IsSMulApply Int F' α α] [IsIntCastApply F' α] [IsOneApplyEqSelf F' α] (n : ℤ) : (n : F') = n • (1 : F') := by apply DFunLike.ext simp +@[deprecated (since := "2026-07-24")] alias coe_intCast := intCast_eq_zsmul_one + end Coercion end FunLike diff --git a/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean b/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean index e02c00401d..84ddfd8cf8 100644 --- a/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean +++ b/Mathlib/FieldTheory/Galois/IsGaloisGroup.lean @@ -122,9 +122,8 @@ theorem card_eq_finrank' : Nat.card G = Module.finrank A B := by have := IsDomain.of_faithfulSMul A B let := FractionRing.liftAlgebra A (FractionRing B) let := IsFractionRing.mulSemiringAction G B (FractionRing B) - have : Algebra.IsIntegral A B := IsGaloisGroup.isInvariant.isIntegral A B G rw [IsGaloisGroup.card_eq_finrank G (FractionRing A) (FractionRing B), - Algebra.IsAlgebraic.finrank_of_isFractionRing A (FractionRing A) B (FractionRing B)] + IsFractionRing.finrank_eq A (FractionRing A) B (FractionRing B)] @[simp] theorem map_mulEquivAlgEquiv_fixingSubgroup [IsGaloisGroup G K L] (F : IntermediateField K L) : diff --git a/Mathlib/Geometry/Convex/ConvexSpace/AffineMap.lean b/Mathlib/Geometry/Convex/ConvexSpace/AffineMap.lean new file mode 100644 index 0000000000..af917b6b5b --- /dev/null +++ b/Mathlib/Geometry/Convex/ConvexSpace/AffineMap.lean @@ -0,0 +1,100 @@ +/- +Copyright (c) 2026 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.Geometry.Convex.ConvexSpace.Defs + +/-! +# Bundled affine maps between convex spaces + +If `X` and `Y` are convex spaces (over `R`), we introduce the type +`ConvexSpace.AffineMap R X Y` of bundled affine maps from `X` to `Y`. + +-/ + +@[expose] public section + +variable {R : Type*} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] + +namespace Convexity.ConvexSpace + +variable (R) in +/-- The type of (bundled) affine maps between two convex spaces. -/ +protected structure AffineMap + (X Y : Type*) [ConvexSpace R X] [ConvexSpace R Y] where + /-- The underlying map of an affine map between convex spaces. -/ + toFun : X → Y + isAffineMap_toFun : IsAffineMap R toFun := by fun_prop + +namespace AffineMap + +instance {X Y : Type*} [ConvexSpace R X] [ConvexSpace R Y] : + FunLike (ConvexSpace.AffineMap R X Y) X Y where + coe := ConvexSpace.AffineMap.toFun + coe_injective := fun ⟨f, _⟩ ⟨g, _⟩ h ↦ by simpa + +initialize_simps_projections ConvexSpace.AffineMap (toFun → apply) + +@[ext] +lemma ext {X Y : Type*} [ConvexSpace R X] [ConvexSpace R Y] + {f g : ConvexSpace.AffineMap R X Y} (h : (f : X → Y) = g) : f = g := + DFunLike.coe_injective h + +@[fun_prop] +lemma isAffineMap + {X Y : Type*} [ConvexSpace R X] [ConvexSpace R Y] + (f : ConvexSpace.AffineMap R X Y) : + IsAffineMap R f := + f.isAffineMap_toFun + +/-- The identity map, as a bundled affine map of convex spaces. -/ +@[simps, implicit_reducible] +def id (X : Type*) [ConvexSpace R X] : + ConvexSpace.AffineMap R X X where + toFun := _root_.id + +/-- The composition of bundled affine maps between convex spaces. -/ +@[simps, implicit_reducible] +def comp + {X Y Z : Type*} [ConvexSpace R X] [ConvexSpace R Y] [ConvexSpace R Z] + (g : ConvexSpace.AffineMap R Y Z) (f : ConvexSpace.AffineMap R X Y) : + ConvexSpace.AffineMap R X Z where + toFun := g ∘ f + +@[simp] +lemma coe_comp + {X Y Z : Type*} [ConvexSpace R X] [ConvexSpace R Y] [ConvexSpace R Z] + (g : ConvexSpace.AffineMap R Y Z) (f : ConvexSpace.AffineMap R X Y) : + ⇑(g.comp f) = g ∘ f := rfl + +@[simp] +lemma id_comp + {X Y : Type*} [ConvexSpace R X] [ConvexSpace R Y] + (f : ConvexSpace.AffineMap R X Y) : + (AffineMap.id _).comp f = f := rfl + +@[simp] +lemma comp_id + {X Y : Type*} [ConvexSpace R X] [ConvexSpace R Y] + (f : ConvexSpace.AffineMap R X Y) : + f.comp (.id _) = f := rfl + +lemma assoc {X Y Z T : Type*} + [ConvexSpace R X] [ConvexSpace R Y] [ConvexSpace R Z] [ConvexSpace R T] + (f₁ : ConvexSpace.AffineMap R Z T) (f₂ : ConvexSpace.AffineMap R Y Z) + (f₃ : ConvexSpace.AffineMap R X Y) : + (f₁.comp f₂).comp f₃ = f₁.comp (f₂.comp f₃) := + rfl + +/-- A constant map between convex spaces, as a bundled affine map. -/ +@[simps, implicit_reducible] +def const {X Y : Type*} [ConvexSpace R X] [ConvexSpace R Y] (y : Y) : + ConvexSpace.AffineMap R X Y where + toFun _ := y + +end AffineMap + +end Convexity.ConvexSpace diff --git a/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean b/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean index 80016c836a..49aa134dd9 100644 --- a/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean +++ b/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean @@ -339,6 +339,11 @@ lemma IsAffineMap.comp {g : N → P} (hg : IsAffineMap R g) {f : M → N} (hf : map_sConvexComb s := by simp [StdSimplex.map_comp, hf.map_sConvexComb, hg.map_sConvexComb] +@[fun_prop] +lemma IsAffineMap.const (x : N) : + IsAffineMap R (fun (_ : M) ↦ x) where + map_sConvexComb _ := by simp + variable (R) in @[fun_prop] lemma StdSimplex.isAffineMap_map (f : I → J) : IsAffineMap R (StdSimplex.map (R := R) f) := diff --git a/Mathlib/Geometry/Euclidean/Inversion/Basic.lean b/Mathlib/Geometry/Euclidean/Inversion/Basic.lean index 08b9868f5d..9ced846f55 100644 --- a/Mathlib/Geometry/Euclidean/Inversion/Basic.lean +++ b/Mathlib/Geometry/Euclidean/Inversion/Basic.lean @@ -230,3 +230,23 @@ protected theorem Continuous.inversion (hc : Continuous c) (hR : Continuous R) ( (hne : ∀ a, x a ≠ c a) : Continuous (fun a ↦ inversion (c a) (R a) (x a)) := continuous_iff_continuousAt.2 fun _ ↦ hc.continuousAt.inversion hR.continuousAt hx.continuousAt (hne _) + +namespace EuclideanGeometry + +open Filter in +/-- The inversion of a point tends to infinity as it approaches the center of an inversion. -/ +theorem tendsto_inversion_nhdsNE_center_cobounded {c : P} {R : ℝ} (hR : R ≠ 0) : + Tendsto (inversion c R) (𝓝[≠] c) (Bornology.cobounded P) := by + rw [← tendsto_dist_left_atTop_iff c] + have hdist : Tendsto (dist c) (𝓝[≠] c) (𝓝[>] (0 : ℝ)) := by + rw [tendsto_nhdsWithin_iff] + refine ⟨tendsto_nhdsWithin_of_tendsto_nhds ?_, eventually_nhdsWithin_of_forall ?_⟩ + · rw [← dist_self c] + exact ContinuousAt.tendsto <| by fun_prop + · aesop + have hratio : Tendsto (fun x : P ↦ dist c (inversion c R x)) (𝓝[≠] c) atTop := by + simp_rw [dist_center_inversion, div_eq_mul_inv] + exact hdist.inv_tendsto_nhdsGT_zero.const_mul_atTop <| by rwa [sq_pos_iff] + simpa using hratio + +end EuclideanGeometry diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean index 09085d2180..7d8921e0f6 100644 --- a/Mathlib/Geometry/Manifold/ChartedSpace.lean +++ b/Mathlib/Geometry/Manifold/ChartedSpace.lean @@ -359,7 +359,7 @@ We keep this as a definition (not an instance) to avoid instance search trying t `DiscreteTopology` or `Unique` instances. -/ @[instance_reducible] -def ChartedSpace.of_discreteTopology [TopologicalSpace M] [TopologicalSpace H] +def ChartedSpace.ofDiscreteTopology [TopologicalSpace M] [TopologicalSpace H] [DiscreteTopology M] [h : Unique H] : ChartedSpace H M where atlas := letI f := fun x : M ↦ OpenPartialHomeomorph.const @@ -369,11 +369,14 @@ def ChartedSpace.of_discreteTopology [TopologicalSpace M] [TopologicalSpace H] mem_chart_source x := by simp chart_mem_atlas x := by simp +@[deprecated (since := "2026-07-26")] +alias ChartedSpace.of_discreteTopology := ChartedSpace.ofDiscreteTopology + /-- A chart on the discrete space is the constant chart. -/ @[simp, mfld_simps] lemma chartedSpace_of_discreteTopology_chartAt [TopologicalSpace M] [TopologicalSpace H] [DiscreteTopology M] [h : Unique H] {x : M} : - haveI := ChartedSpace.of_discreteTopology (M := M) (H := H) + haveI := ChartedSpace.ofDiscreteTopology (M := M) (H := H) chartAt H x = OpenPartialHomeomorph.const (isOpen_discrete {x}) (isOpen_discrete {h.default}) := rfl @@ -496,7 +499,7 @@ variable [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace M'] /-- The disjoint union of two charted spaces modelled on a non-empty space `H` is a charted space over `H`. -/ @[instance_reducible] -def ChartedSpace.sum_of_nonempty [Nonempty H] : ChartedSpace H (M ⊕ M') where +def ChartedSpace.sumOfNonempty [Nonempty H] : ChartedSpace H (M ⊕ M') where atlas := ((fun e ↦ e.lift_openEmbedding IsOpenEmbedding.inl) '' cm.atlas) ∪ ((fun e ↦ e.lift_openEmbedding IsOpenEmbedding.inr) '' cm'.atlas) -- At `x : M`, the chart is the chart in `M`; at `x' ∈ M'`, it is the chart in `M'`. @@ -523,9 +526,12 @@ def ChartedSpace.sum_of_nonempty [Nonempty H] : ChartedSpace H (M ⊕ M') where right use ChartedSpace.chartAt x, cm'.chart_mem_atlas x +@[deprecated (since := "2026-07-26")] +alias ChartedSpace.sum_of_nonempty := ChartedSpace.sumOfNonempty + instance ChartedSpace.sum : ChartedSpace H (M ⊕ M') := by by_cases! h : Nonempty H - · exact ChartedSpace.sum_of_nonempty + · exact ChartedSpace.sumOfNonempty have : IsEmpty M := isEmpty_of_chartedSpace H have : IsEmpty M' := isEmpty_of_chartedSpace H exact empty H (M ⊕ M') diff --git a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean index 8e1ea40bbd..7209dff92e 100644 --- a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean +++ b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean @@ -912,14 +912,14 @@ instance empty [IsEmpty M] : IsManifold I n M := by _ = ∅ := empty_inter (range I) apply (this ▸ hx).elim -attribute [local instance] ChartedSpace.of_discreteTopology in +attribute [local instance] ChartedSpace.ofDiscreteTopology in variable (n) in /-- A discrete space `M` is a smooth manifold over the trivial model on a trivial normed space. -/ theorem of_discreteTopology [DiscreteTopology M] [Unique E] : IsManifold (modelWithCornersSelf 𝕜 E) n M := by apply isManifold_of_contDiffOn _ _ _ (fun _ _ _ _ ↦ contDiff_of_subsingleton.contDiffOn) -attribute [local instance] ChartedSpace.of_discreteTopology in +attribute [local instance] ChartedSpace.ofDiscreteTopology in example [Unique E] : IsManifold (𝓘(𝕜, E)) n (Fin 2) := of_discreteTopology _ set_option backward.isDefEq.respectTransparency false in diff --git a/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean b/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean index b110822d13..4b1a5ae994 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean @@ -387,17 +387,20 @@ lemma zero [VectorBundle 𝕜 F V] (cov : CovariantDerivative I F V) : cov 0 = 0 /-- If `cov` is a covariant derivative on each set in an open cover, it is a covariant derivative. -/ -def of_isCovariantDerivativeOn_of_open_cover {ι : Type*} {s : ι → Set M} +def ofIsCovariantDerivativeOnOfOpenCover {ι : Type*} {s : ι → Set M} {cov : (Π x : M, V x) → (Π x : M, TangentSpace I x →L[𝕜] V x)} (hcov : ∀ i, IsCovariantDerivativeOn F cov (s i)) (hs : ⋃ i, s i = Set.univ) : CovariantDerivative I F V := ⟨cov, hs ▸ IsCovariantDerivativeOn.iUnion hcov⟩ +@[deprecated (since := "2026-07-26")] +alias of_isCovariantDerivativeOn_of_open_cover := ofIsCovariantDerivativeOnOfOpenCover + @[simp] lemma of_isCovariantDerivativeOn_of_open_cover_coe {ι : Type*} {s : ι → Set M} {cov : (Π x : M, V x) → (Π x : M, TangentSpace I x →L[𝕜] V x)} (hcov : ∀ i, IsCovariantDerivativeOn F cov (s i)) (hs : ⋃ i, s i = Set.univ) : - of_isCovariantDerivativeOn_of_open_cover hcov hs = cov := rfl + ofIsCovariantDerivativeOnOfOpenCover hcov hs = cov := rfl /-- A covariant derivative ∇ is called of class `C^k` iff, whenever `X` is a `C^k` section and `σ` a @@ -433,39 +436,51 @@ one-forms taking values in the endomorphisms of the bundle, but we don’t packa /-- An affine combination of covariant derivatives as a covariant derivative. -/ @[simps] -def affine_combination (cov cov' : CovariantDerivative I F V) (g : M → 𝕜) : +def affineCombination (cov cov' : CovariantDerivative I F V) (g : M → 𝕜) : CovariantDerivative I F V where toFun := fun σ ↦ (g • (cov σ)) + (1 - g) • (cov' σ) isCovariantDerivativeOnUniv := cov.isCovariantDerivativeOn.affine_combination cov'.isCovariantDerivativeOn _ +@[deprecated (since := "2026-07-26")] alias affine_combination := affineCombination + /-- A finite affine combination of covariant derivatives as a covariant derivative. -/ -def finite_affine_combination {ι : Type*} {s : Finset ι} +def finiteAffineCombination {ι : Type*} {s : Finset ι} (cov : ι → CovariantDerivative I F V) {f : ι → M → 𝕜} (hf : ∑ i ∈ s, f i = 1) : CovariantDerivative I F V where toFun t x := ∑ i ∈ s, (f i x) • (cov i) t x isCovariantDerivativeOnUniv := IsCovariantDerivativeOn.finite_affine_combination (fun i ↦ (cov i).isCovariantDerivativeOn) hf +@[deprecated (since := "2026-07-26")] alias finite_affine_combination := finiteAffineCombination + /-- An affine combination of two `C^k` connections is a `C^k` connection. -/ -lemma ContMDiffCovariantDerivative.affine_combination [IsManifold I 1 M] [VectorBundle 𝕜 F V] +lemma ContMDiffCovariantDerivative.affineCombination [IsManifold I 1 M] [VectorBundle 𝕜 F V] (cov cov' : CovariantDerivative I F V) {f : M → 𝕜} {n : ℕ∞ω} (hf : CMDiff n f) (hcov : ContMDiffCovariantDerivative cov n) (hcov' : ContMDiffCovariantDerivative cov' n) : - ContMDiffCovariantDerivative (affine_combination cov cov' f) n where + ContMDiffCovariantDerivative (affineCombination cov cov' f) n where contMDiff := ContMDiffCovariantDerivativeOn.affine_combination hf.contMDiffOn hcov.contMDiff hcov'.contMDiff +@[deprecated (since := "2026-07-26")] +alias ContMDiffCovariantDerivative.affine_combination := + ContMDiffCovariantDerivative.affineCombination + /-- An affine combination of finitely many `C^k` connections is a `C^k` connection. -/ -lemma ContMDiffCovariantDerivative.finite_affine_combination [IsManifold I 1 M] [VectorBundle 𝕜 F V] +lemma ContMDiffCovariantDerivative.finiteAffineCombination [IsManifold I 1 M] [VectorBundle 𝕜 F V] {ι : Type*} {s : Finset ι} (cov : ι → CovariantDerivative I F V) {f : ι → M → 𝕜} (hf : ∑ i ∈ s, f i = 1) {n : ℕ∞ω} (hf' : ∀ i ∈ s, CMDiff n (f i)) (hcov : ∀ i ∈ s, ContMDiffCovariantDerivative (cov i) n) : - ContMDiffCovariantDerivative (finite_affine_combination cov hf) n where + ContMDiffCovariantDerivative (finiteAffineCombination cov hf) n where contMDiff := ContMDiffCovariantDerivativeOn.finite_affine_combination (fun i hi ↦ (hcov i hi).contMDiff) (fun i hi ↦ (hf' i hi).contMDiffOn) +@[deprecated (since := "2026-07-26")] +alias ContMDiffCovariantDerivative.finite_affine_combination := + ContMDiffCovariantDerivative.finiteAffineCombination + -- TODO: prove a version with a locally finite sum, and deduce that C^k connections always -- exist (using a partition of unity argument) diff --git a/Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean b/Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean index c0ffd9fd8f..9c437a587c 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean @@ -66,18 +66,18 @@ the model fiber `F`. * `e.localFrame b`: the local frame on `V` induced by `e` and `b`. Use `e.localFrame b i` to access the i-th section in that frame. * `e.contMDiffOn_localFrame_baseSet`: each section `e.localFrame b i` is smooth on `e.baseSet` -* `e.localFrame_coeff b i` describes the `i`-th coefficient of sections of `V` w.r.t. +* `e.localFrameCoeff b i` describes the `i`-th coefficient of sections of `V` w.r.t. `e.localFrame b`: it is a family of fiberwise linear maps `Π x, V x →ₗ[𝕜] 𝕜`, and the coefficient - function of a section `s` is `(LinearMap.piApply (e.localFrame_coeff b i)) s`. + function of a section `s` is `(LinearMap.piApply (e.localFrameCoeff b i)) s`. * `e.eventually_eq_localFrame_sum_coeff_smul b`: near `x`, we have - `s = ∑ i, (LinearMap.piApply (e.localFrame_coeff b i) s) • e.localFrame b i` -* `e.localFrame_coeff_congr b`: the coefficient `e.localFrame_coeff b i` of `s` in the local frame + `s = ∑ i, (LinearMap.piApply (e.localFrameCoeff b i) s) • e.localFrame b i` +* `e.localFrameCoeff_congr b`: the coefficient `e.localFrameCoeff b i` of `s` in the local frame induced by `e` and `b` at `x` only depends on `s` at `x`. -* `e.contMDiffOn_localFrame_coeff`: if `s` is a `C^k` section, each coefficient - `(LinearMap.piApply (e.localFrame_coeff b i) s)` is `C^k` on `e.baseSet` -* `e.contMDiffAt_iff_localFrame_coeff b`: a section `s` is `C^k` at `x ∈ e.baseSet` +* `e.contMDiffOn_localFrameCoeff`: if `s` is a `C^k` section, each coefficient + `(LinearMap.piApply (e.localFrameCoeff b i) s)` is `C^k` on `e.baseSet` +* `e.contMDiffAt_iff_localFrameCoeff b`: a section `s` is `C^k` at `x ∈ e.baseSet` iff all of its frame coefficients are -* `e.contMDiffOn_iff_localFrame_coeff b`: a section `s` is `C^k` on an open set `t ⊆ e.baseSet` +* `e.contMDiffOn_iff_localFrameCoeff b`: a section `s` is `C^k` on an open set `t ⊆ e.baseSet` iff all of its frame coefficients are ## Note @@ -378,58 +378,73 @@ variable (I) in /-- Coefficients of a section `s` of `V` w.r.t. the local frame `b.localFrame e i`. If x is outside of `e.baseSet`, this returns the junk value 0. -/ -def localFrame_coeff (i : ι) : Π x : M, (V x →ₗ[𝕜] 𝕜) := +def localFrameCoeff (i : ι) : Π x : M, (V x →ₗ[𝕜] 𝕜) := (e.isLocalFrameOn_localFrame_baseSet I 1 b).coeff i +@[deprecated (since := "2026-07-26")] alias localFrame_coeff := localFrameCoeff + variable {e b} variable {x x' : M} variable (e b) in @[simp] -lemma localFrame_coeff_apply_of_notMem_baseSet (hx : x ∉ e.baseSet) (i : ι) : - e.localFrame_coeff I b i x = 0 := by - simpa [localFrame_coeff] using +lemma localFrameCoeff_apply_of_notMem_baseSet (hx : x ∉ e.baseSet) (i : ι) : + e.localFrameCoeff I b i x = 0 := by + simpa [localFrameCoeff] using (e.isLocalFrameOn_localFrame_baseSet I 1 b).coeff_apply_of_notMem hx i +@[deprecated (since := "2026-07-26")] +alias localFrame_coeff_apply_of_notMem_baseSet := localFrameCoeff_apply_of_notMem_baseSet + variable (e b) in @[simp] -lemma localFrame_coeff_apply_of_mem_baseSet (hx : x ∈ e.baseSet) (s : Π x : M, V x) (i : ι) : - (localFrame_coeff I e b i x) (s x) = (e.basisAt b hx).repr (s x) i := by +lemma localFrameCoeff_apply_of_mem_baseSet (hx : x ∈ e.baseSet) (s : Π x : M, V x) (i : ι) : + (localFrameCoeff I e b i x) (s x) = (e.basisAt b hx).repr (s x) i := by have he := e.isLocalFrameOn_localFrame_baseSet I 1 b have hbasis : e.basisAt b hx = he.toBasisAt hx := by ext j simp [IsLocalFrameOn.toBasisAt, localFrame, basisAt, hx] - simp [localFrame_coeff, IsLocalFrameOn.coeff, hx, hbasis] + simp [localFrameCoeff, IsLocalFrameOn.coeff, hx, hbasis] + +@[deprecated (since := "2026-07-26")] +alias localFrame_coeff_apply_of_mem_baseSet := localFrameCoeff_apply_of_mem_baseSet variable {s s' : Π x : M, V x} -lemma eq_sum_localFrame_coeff_smul [Fintype ι] (hx : x' ∈ e.baseSet) : - s x' = ∑ i, e.localFrame_coeff I b i x' (s x') • e.localFrame b i x' := +lemma eq_sum_localFrameCoeff_smul [Fintype ι] (hx : x' ∈ e.baseSet) : + s x' = ∑ i, e.localFrameCoeff I b i x' (s x') • e.localFrame b i x' := (isLocalFrameOn_localFrame_baseSet I 1 e b).coeff_sum_eq s hx +@[deprecated (since := "2026-07-26")] +alias eq_sum_localFrame_coeff_smul := eq_sum_localFrameCoeff_smul + variable (e b) in /-- A local frame locally spans the space of sections for `V`: for each local trivialisation `e` of `V` around `x`, we have -`s = ∑ i, (LinearMap.piApply (b.localFrame_coeff e i) s) • b.localFrame e i` near `x`. -/ +`s = ∑ i, (LinearMap.piApply (b.localFrameCoeff e i) s) • b.localFrame e i` near `x`. -/ lemma eventually_eq_localFrame_sum_coeff_smul [Fintype ι] (hxe : x ∈ e.baseSet) : - ∀ᶠ x' in 𝓝 x, s x' = ∑ i, e.localFrame_coeff I b i x' (s x') • e.localFrame b i x' := - eventually_nhds_iff.mpr ⟨e.baseSet, fun _ ↦ e.eq_sum_localFrame_coeff_smul, e.open_baseSet, hxe⟩ + ∀ᶠ x' in 𝓝 x, s x' = ∑ i, e.localFrameCoeff I b i x' (s x') • e.localFrame b i x' := + eventually_nhds_iff.mpr ⟨e.baseSet, fun _ ↦ e.eq_sum_localFrameCoeff_smul, e.open_baseSet, hxe⟩ variable (e b) in /-- The representation of `s` in a local frame at `x` only depends on `s` at `x`. -/ -lemma localFrame_coeff_congr {i : ι} (hss' : s x = s' x) : - e.localFrame_coeff I b i x (s x) = e.localFrame_coeff I b i x (s' x) := by +lemma localFrameCoeff_congr {i : ι} (hss' : s x = s' x) : + e.localFrameCoeff I b i x (s x) = e.localFrameCoeff I b i x (s' x) := by simpa using! (isLocalFrameOn_localFrame_baseSet I 1 e b).coeff_congr hss' i +@[deprecated (since := "2026-07-26")] alias localFrame_coeff_congr := localFrameCoeff_congr + variable {n} variable (e) in /-- Suppose `e` is a compatible trivialisation around `x ∈ M`, and `s` a bundle section. Then the coefficient of `s` w.r.t. the local frame induced by `b` and `e` equals the coefficient of "`s x` read in the trivialisation `e`" for `b i`. -/ -lemma localFrame_coeff_eq_coeff (hxe : x ∈ e.baseSet) {i : ι} : - e.localFrame_coeff I b i x (s x) = b.repr (e ((T% s) x)).2 i := by - simp [e.localFrame_coeff_apply_of_mem_baseSet b hxe, basisAt] +lemma localFrameCoeff_eq_coeff (hxe : x ∈ e.baseSet) {i : ι} : + e.localFrameCoeff I b i x (s x) = b.repr (e ((T% s) x)).2 i := by + simp [e.localFrameCoeff_apply_of_mem_baseSet b hxe, basisAt] + +@[deprecated (since := "2026-07-26")] alias localFrame_coeff_eq_coeff := localFrameCoeff_eq_coeff end Bundle.Trivialization @@ -446,10 +461,10 @@ variable [VectorBundle 𝕜 F V] [ContMDiffVectorBundle 1 F V I] [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I] set_option backward.isDefEq.respectTransparency false in -/-- If `s` is `C^k` at `x`, so is its coefficient `b.localFrame_coeff e i` in the local frame +/-- If `s` is `C^k` at `x`, so is its coefficient `b.localFrameCoeff e i` in the local frame near `x` induced by `e` and `b` -/ -lemma contMDiffAt_localFrame_coeff (hxe : x ∈ e.baseSet) (hs : CMDiffAt k (T% s) x) (i : ι) : - CMDiffAt k ((LinearMap.piApply (e.localFrame_coeff I b i)) s) x := by +lemma contMDiffAt_localFrameCoeff (hxe : x ∈ e.baseSet) (hs : CMDiffAt k (T% s) x) (i : ι) : + CMDiffAt k ((LinearMap.piApply (e.localFrameCoeff I b i)) s) x := by -- This boils down to computing the frame coefficients in a local trivialisation. -- step 1: on e.baseSet, we know compute the coefficient very well let aux := fun x ↦ b.repr (e ((T% s) x)).2 i @@ -458,7 +473,7 @@ lemma contMDiffAt_localFrame_coeff (hxe : x ∈ e.baseSet) (hs : CMDiffAt k (T% apply this.congr_of_eventuallyEq ?_ apply eventuallyEq_of_mem (s := e.baseSet) (by simp [e.open_baseSet.mem_nhds hxe]) intro y hy - simp [aux, e.localFrame_coeff_eq_coeff hy] + simp [aux, e.localFrameCoeff_eq_coeff hy] simp only [aux] -- step 2: `s` read in trivialization `e` is `C^k` have h₁ : CMDiffAt k (fun x ↦ (e ((T% s) x)).2) x := by @@ -472,52 +487,70 @@ lemma contMDiffAt_localFrame_coeff (hxe : x ∈ e.baseSet) (hs : CMDiffAt k (T% contMDiffAt_iff_contDiffAt.mpr <| by fun_prop exact this.comp x h₁ -/-- If `s` is `C^k` on `t ⊆ e.baseSet`, so is its coefficient `b.localFrame_coeff e i` +@[deprecated (since := "2026-07-26")] +alias contMDiffAt_localFrame_coeff := contMDiffAt_localFrameCoeff + +/-- If `s` is `C^k` on `t ⊆ e.baseSet`, so is its coefficient `b.localFrameCoeff e i` in the local frame induced by `e` -/ -lemma contMDiffOn_localFrame_coeff (ht : IsOpen t) (ht' : t ⊆ e.baseSet) +lemma contMDiffOn_localFrameCoeff (ht : IsOpen t) (ht' : t ⊆ e.baseSet) (hs : CMDiff[t] k (T% s)) (i : ι) : - CMDiff[t] k ((LinearMap.piApply (e.localFrame_coeff I b i)) s) := - fun _ hx ↦ (contMDiffAt_localFrame_coeff b (ht' hx) + CMDiff[t] k ((LinearMap.piApply (e.localFrameCoeff I b i)) s) := + fun _ hx ↦ (contMDiffAt_localFrameCoeff b (ht' hx) (hs.contMDiffAt (ht.mem_nhds hx)) i).contMDiffWithinAt -/-- If `s` is `C^k` on `e.baseSet`, so is its coefficient `b.localFrame_coeff e i` +@[deprecated (since := "2026-07-26")] +alias contMDiffOn_localFrame_coeff := contMDiffOn_localFrameCoeff + +/-- If `s` is `C^k` on `e.baseSet`, so is its coefficient `b.localFrameCoeff e i` in the local frame induced by `e` -/ -lemma contMDiffOn_baseSet_localFrame_coeff (hs : CMDiff[e.baseSet] k (T% s)) (i : ι) : - CMDiff[e.baseSet] k ((LinearMap.piApply (e.localFrame_coeff I b i)) s) := - contMDiffOn_localFrame_coeff b e.open_baseSet (subset_refl _) hs _ +lemma contMDiffOn_baseSet_localFrameCoeff (hs : CMDiff[e.baseSet] k (T% s)) (i : ι) : + CMDiff[e.baseSet] k ((LinearMap.piApply (e.localFrameCoeff I b i)) s) := + contMDiffOn_localFrameCoeff b e.open_baseSet (subset_refl _) hs _ + +@[deprecated (since := "2026-07-26")] +alias contMDiffOn_baseSet_localFrame_coeff := contMDiffOn_baseSet_localFrameCoeff /-- A section `s` of `V` is `C^k` at `x ∈ e.baseSet` iff each of its -coefficients `(LinearMap.piApply (b.localFrame_coeff e i) s)` in a local frame near `x` is -/ -lemma contMDiffAt_iff_localFrame_coeff (hx : x' ∈ e.baseSet) : - CMDiffAt k (T% s) x' ↔ ∀ i, CMDiffAt k ((LinearMap.piApply (e.localFrame_coeff I b i)) s) x' := - ⟨fun h i ↦ contMDiffAt_localFrame_coeff b hx h i, +coefficients `(LinearMap.piApply (b.localFrameCoeff e i) s)` in a local frame near `x` is -/ +lemma contMDiffAt_iff_localFrameCoeff (hx : x' ∈ e.baseSet) : + CMDiffAt k (T% s) x' ↔ ∀ i, CMDiffAt k ((LinearMap.piApply (e.localFrameCoeff I b i)) s) x' := + ⟨fun h i ↦ contMDiffAt_localFrameCoeff b hx h i, fun hi ↦ (e.isLocalFrameOn_localFrame_baseSet I k b).contMDiffAt_of_coeff hi (e.open_baseSet.mem_nhds hx)⟩ +@[deprecated (since := "2026-07-26")] +alias contMDiffAt_iff_localFrame_coeff := contMDiffAt_iff_localFrameCoeff + /-- A section `s` of `V` is `C^k` on `t ⊆ e.baseSet` iff each of its -coefficients `(LinearMap.piApply (b.localFrame_coeff e i) s)` in a local frame near `x` is -/ -lemma contMDiffOn_iff_localFrame_coeff (ht : IsOpen t) (ht' : t ⊆ e.baseSet) : - CMDiff[t] k (T% s) ↔ ∀ i, CMDiff[t] k ((LinearMap.piApply (e.localFrame_coeff I b i)) s) := by - refine ⟨fun h i ↦ contMDiffOn_localFrame_coeff b ht ht' h _, fun h x hx ↦ ?_⟩ - exact (contMDiffAt_iff_localFrame_coeff b (ht' hx)).mpr +coefficients `(LinearMap.piApply (b.localFrameCoeff e i) s)` in a local frame near `x` is -/ +lemma contMDiffOn_iff_localFrameCoeff (ht : IsOpen t) (ht' : t ⊆ e.baseSet) : + CMDiff[t] k (T% s) ↔ ∀ i, CMDiff[t] k ((LinearMap.piApply (e.localFrameCoeff I b i)) s) := by + refine ⟨fun h i ↦ contMDiffOn_localFrameCoeff b ht ht' h _, fun h x hx ↦ ?_⟩ + exact (contMDiffAt_iff_localFrameCoeff b (ht' hx)).mpr (fun i ↦ (h i x hx).contMDiffAt (ht.mem_nhds hx)) |>.contMDiffWithinAt +@[deprecated (since := "2026-07-26")] +alias contMDiffOn_iff_localFrame_coeff := contMDiffOn_iff_localFrameCoeff + /-- A section `s` of `V` is `C^k` on a trivialisation domain `e.baseSet` iff each of its -coefficients `(LinearMap.piApply (b.localFrame_coeff e i) s)` in a local frame near `x` is -/ -lemma contMDiffOn_baseSet_iff_localFrame_coeff : +coefficients `(LinearMap.piApply (b.localFrameCoeff e i) s)` in a local frame near `x` is -/ +lemma contMDiffOn_baseSet_iff_localFrameCoeff : CMDiff[e.baseSet] k (T% s) ↔ - ∀ i, CMDiff[e.baseSet] k ((LinearMap.piApply (e.localFrame_coeff I b i)) s) := by - rw [contMDiffOn_iff_localFrame_coeff b e.open_baseSet (subset_refl _)] + ∀ i, CMDiff[e.baseSet] k ((LinearMap.piApply (e.localFrameCoeff I b i)) s) := by + rw [contMDiffOn_iff_localFrameCoeff b e.open_baseSet (subset_refl _)] + +@[deprecated (since := "2026-07-26")] +alias contMDiffOn_baseSet_iff_localFrame_coeff := contMDiffOn_baseSet_iff_localFrameCoeff -- Differentiability of a section can be checked in terms of its local frame coefficients section MDifferentiable set_option backward.isDefEq.respectTransparency false in -/-- If `s` is differentiable at `x`, so is its coefficient `b.localFrame_coeff e i` in the local +/-- If `s` is differentiable at `x`, so is its coefficient `b.localFrameCoeff e i` in the local frame near `x` induced by `e` and `b` -/ -lemma mdifferentiableAt_localFrame_coeff +lemma mdifferentiableAt_localFrameCoeff (hxe : x ∈ e.baseSet) (hs : MDiffAt (T% s) x) (i : ι) : - MDiffAt ((LinearMap.piApply (e.localFrame_coeff I b i)) s) x := by + MDiffAt ((LinearMap.piApply (e.localFrameCoeff I b i)) s) x := by -- This boils down to computing the frame coefficients in a local trivialisation. -- step 1: on `e.baseSet`, we know the coefficient very well let aux := fun x ↦ b.repr (e ((T% s) x)).2 i @@ -526,7 +559,7 @@ lemma mdifferentiableAt_localFrame_coeff apply this.congr_of_eventuallyEq apply eventuallyEq_of_mem (s := e.baseSet) (by simp [e.open_baseSet.mem_nhds hxe]) intro y hy - simp [aux, e.localFrame_coeff_eq_coeff hy] + simp [aux, e.localFrameCoeff_eq_coeff hy] simp only [aux] -- step 2: `s` read in trivialization `e` is differentiable have h₁ : MDiffAt (fun x ↦ (e ((T% s) x)).2) x := by @@ -540,26 +573,38 @@ lemma mdifferentiableAt_localFrame_coeff mdifferentiableAt_iff_differentiableAt.mpr <| by fun_prop exact this.comp x h₁ -/-- If `s` is differentiable on `t ⊆ e.baseSet`, so is its coefficient `b.localFrame_coeff e i` +@[deprecated (since := "2026-07-26")] +alias mdifferentiableAt_localFrame_coeff := mdifferentiableAt_localFrameCoeff + +/-- If `s` is differentiable on `t ⊆ e.baseSet`, so is its coefficient `b.localFrameCoeff e i` in the local frame induced by `e` -/ -lemma mdifferentiableOn_localFrame_coeff (ht : IsOpen t) (ht' : t ⊆ e.baseSet) - (hs : MDiff[t] (T% s)) (i : ι) : MDiff[t] ((LinearMap.piApply (e.localFrame_coeff I b i)) s) := - fun _ hx ↦ (mdifferentiableAt_localFrame_coeff b (ht' hx) +lemma mdifferentiableOn_localFrameCoeff (ht : IsOpen t) (ht' : t ⊆ e.baseSet) + (hs : MDiff[t] (T% s)) (i : ι) : MDiff[t] ((LinearMap.piApply (e.localFrameCoeff I b i)) s) := + fun _ hx ↦ (mdifferentiableAt_localFrameCoeff b (ht' hx) (hs.mdifferentiableAt (ht.mem_nhds hx)) i).mdifferentiableWithinAt -/-- If `s` is differentiable on `e.baseSet`, so is its coefficient `b.localFrame_coeff e i` in the +@[deprecated (since := "2026-07-26")] +alias mdifferentiableOn_localFrame_coeff := mdifferentiableOn_localFrameCoeff + +/-- If `s` is differentiable on `e.baseSet`, so is its coefficient `b.localFrameCoeff e i` in the local frame induced by `e` -/ -lemma mdifferentiableOn_baseSet_localFrame_coeff (hs : MDiff[e.baseSet] (T% s)) (i : ι) : - MDiff[e.baseSet] ((LinearMap.piApply (e.localFrame_coeff I b i)) s) := - mdifferentiableOn_localFrame_coeff b e.open_baseSet (subset_refl _) hs _ +lemma mdifferentiableOn_baseSet_localFrameCoeff (hs : MDiff[e.baseSet] (T% s)) (i : ι) : + MDiff[e.baseSet] ((LinearMap.piApply (e.localFrameCoeff I b i)) s) := + mdifferentiableOn_localFrameCoeff b e.open_baseSet (subset_refl _) hs _ + +@[deprecated (since := "2026-07-26")] +alias mdifferentiableOn_baseSet_localFrame_coeff := mdifferentiableOn_baseSet_localFrameCoeff /-- A section `s` of `V` is differentiable at `x ∈ e.baseSet` iff each of its -coefficients `(LinearMap.piApply (b.localFrame_coeff e i) s)` in a local frame near `x` is -/ -lemma mdifferentiableAt_iff_localFrame_coeff (hx : x' ∈ e.baseSet) : - MDiffAt (T% s) x' ↔ ∀ i, MDiffAt ((LinearMap.piApply (e.localFrame_coeff I b i)) s) x' := - ⟨fun h i ↦ mdifferentiableAt_localFrame_coeff b hx h i, fun hi ↦ +coefficients `(LinearMap.piApply (b.localFrameCoeff e i) s)` in a local frame near `x` is -/ +lemma mdifferentiableAt_iff_localFrameCoeff (hx : x' ∈ e.baseSet) : + MDiffAt (T% s) x' ↔ ∀ i, MDiffAt ((LinearMap.piApply (e.localFrameCoeff I b i)) s) x' := + ⟨fun h i ↦ mdifferentiableAt_localFrameCoeff b hx h i, fun hi ↦ (e.isLocalFrameOn_localFrame_baseSet I 1 b).mdifferentiableAt_of_coeff_aux hi e.open_baseSet hx⟩ +@[deprecated (since := "2026-07-26")] +alias mdifferentiableAt_iff_localFrame_coeff := mdifferentiableAt_iff_localFrameCoeff + end MDifferentiable end diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean b/Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean index a4b1e19033..f9650307d1 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean @@ -137,12 +137,12 @@ lemma pointwise (hΦ : TensorialAt I F Φ x) {σ σ' : Π x : M, V x} have x_mem : x ∈ t.baseSet := FiberBundle.mem_baseSet_trivializationAt F V x let b := Basis.ofVectorSpace 𝕜 F let s := t.localFrame b - let c := t.localFrame_coeff I b + let c := t.localFrameCoeff I b have hs (i) : MDiffAt (T% (s i)) x := (contMDiffAt_localFrame_of_mem 1 _ b i x_mem).mdifferentiableAt (by simp) have hc {σ : (x : M) → V x} (hσ : MDiffAt (T% σ) x) (i) : MDiffAt (LinearMap.piApply (c i) σ) x := - mdifferentiableAt_localFrame_coeff b x_mem hσ i + mdifferentiableAt_localFrameCoeff b x_mem hσ i -- By the locality of the operation `(Φ · x)`, its value on `σ` agrees with the value of `Φ` on -- the expansion of `σ` into coefficients relative to the frame. have hΦ_eq {σ : (x : M) → V x} (hσ : MDiffAt (T% σ) x) : diff --git a/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean b/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean index cd6e4d4d04..465f87a833 100644 --- a/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean +++ b/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean @@ -48,19 +48,39 @@ open Function Set noncomputable section +/-- A free group basis `FreeAddGroupBasis ι G` is a structure recording the isomorphism between an +additive group `G` and the additive free group over `ι`. One may think of such a basis as a function +from `ι` to `G` (which is registered through a `FunLike` instance) together with the fact that the +morphism induced by this function from `FreeAddGroup ι` to `G` is an isomorphism. -/ +structure FreeAddGroupBasis (ι : Type*) (G : Type*) [AddGroup G] where + /-- `FreeAddGroupBasis.ofRepr` constructs a basis given an equivalence with an additive free + group. -/ + ofRepr :: + /-- `repr` is the isomorphism between the additive group `G` and the additive free group + generated by `ι`. -/ + repr : G ≃+ FreeAddGroup ι + /-- A free group basis `FreeGroupBasis ι G` is a structure recording the isomorphism between a group `G` and the free group over `ι`. One may think of such a basis as a function from `ι` to `G` (which is registered through a `FunLike` instance) together with the fact that the morphism induced by this function from `FreeGroup ι` to `G` is an isomorphism. -/ +@[to_additive] structure FreeGroupBasis (ι : Type*) (G : Type*) [Group G] where /-- `FreeGroupBasis.ofRepr` constructs a basis given an equivalence with a free group. -/ ofRepr :: /-- `repr` is the isomorphism between the group `G` and the free group generated by `ι`. -/ repr : G ≃* FreeGroup ι +/-- An additive group is free if it admits an additive free group basis. In the definition, we +require the basis to be in the same universe as `G`, although this property follows from the +existence of a basis in any universe, see `FreeAddGroupBasis.isFreeAddGroup`. -/ +class IsFreeAddGroup (G : Type u) [AddGroup G] : Prop where + nonempty_basis : ∃ (ι : Type u), Nonempty (FreeAddGroupBasis ι G) + /-- A group is free if it admits a free group basis. In the definition, we require the basis to be in the same universe as `G`, although this property follows from the existence of a basis in any universe, see `FreeGroupBasis.isFreeGroup`. -/ +@[to_additive] class IsFreeGroup (G : Type u) [Group G] : Prop where nonempty_basis : ∃ (ι : Type u), Nonempty (FreeGroupBasis ι G) @@ -70,6 +90,9 @@ variable {ι ι' G H : Type*} [Group G] [Group H] /-- A free group basis for `G` over `ι` is associated to a map `ι → G` recording the images of the generators. -/ +@[to_additive +/-- An additive free group basis for `G` over `ι` is associated to a map `ι → G` recording the +images of the generators. -/] instance instFunLike : FunLike (FreeGroupBasis ι G) ι G where coe b := fun i ↦ b.repr.symm (FreeGroup.of i) coe_injective := by @@ -79,38 +102,49 @@ instance instFunLike : FunLike (FreeGroupBasis ι G) ι G where have : b.symm = b'.symm := by ext x; exact DFunLike.congr_fun H x rw [ofRepr.injEq, ← MulEquiv.symm_symm b, ← MulEquiv.symm_symm b', this] -@[simp] lemma repr_apply_coe (b : FreeGroupBasis ι G) (i : ι) : b.repr (b i) = FreeGroup.of i := by +@[to_additive (attr := simp)] +lemma repr_apply_coe (b : FreeGroupBasis ι G) (i : ι) : b.repr (b i) = FreeGroup.of i := by change b.repr (b.repr.symm (FreeGroup.of i)) = FreeGroup.of i simp /-- The canonical basis of the free group over `X`. -/ +@[to_additive /-- The canonical basis of the additive free group over `X`. -/] def ofFreeGroup (X : Type*) : FreeGroupBasis X (FreeGroup X) := ofRepr (MulEquiv.refl _) -@[simp] lemma ofFreeGroup_apply {X : Type*} (x : X) : +@[to_additive (attr := simp)] +lemma ofFreeGroup_apply {X : Type*} (x : X) : FreeGroupBasis.ofFreeGroup X x = FreeGroup.of x := rfl /-- Reindex a free group basis through a bijection of the indexing sets. -/ +@[to_additive /-- Reindex an additive free group basis through a bijection of the indexing sets. -/] protected def reindex (b : FreeGroupBasis ι G) (e : ι ≃ ι') : FreeGroupBasis ι' G := ofRepr (b.repr.trans (FreeGroup.freeGroupCongr e)) -@[simp] lemma reindex_apply (b : FreeGroupBasis ι G) (e : ι ≃ ι') (x : ι') : +@[to_additive (attr := simp)] +lemma reindex_apply (b : FreeGroupBasis ι G) (e : ι ≃ ι') (x : ι') : b.reindex e x = b (e.symm x) := rfl /-- Pushing a free group basis through a group isomorphism. -/ +@[to_additive /-- Pushing an additive free group basis through a group isomorphism. -/] protected def map (b : FreeGroupBasis ι G) (e : G ≃* H) : FreeGroupBasis ι H := ofRepr (e.symm.trans b.repr) -@[simp] lemma map_apply (b : FreeGroupBasis ι G) (e : G ≃* H) (x : ι) : +@[to_additive (attr := simp)] +lemma map_apply (b : FreeGroupBasis ι G) (e : G ≃* H) (x : ι) : b.map e x = e (b x) := rfl +@[to_additive] protected lemma injective (b : FreeGroupBasis ι G) : Injective b := b.repr.symm.injective.comp FreeGroup.of_injective /-- A group admitting a free group basis is a free group. -/ +@[to_additive +/-- An additive group admitting an additive free group basis is an additive free group. -/] lemma isFreeGroup (b : FreeGroupBasis ι G) : IsFreeGroup G := ⟨range b, ⟨b.reindex (Equiv.ofInjective (↑b) b.injective)⟩⟩ +@[to_additive] instance (X : Type*) : IsFreeGroup (FreeGroup X) := (ofFreeGroup X).isFreeGroup @@ -119,7 +153,9 @@ instance (X : Type*) : IsFreeGroup (FreeGroup X) := set_option backward.isDefEq.respectTransparency.types false in /-- Given a free group basis of `G` over `ι`, there is a canonical bijection between maps from `ι` to a group `H` and morphisms from `G` to `H`. -/ -@[simps!] +@[to_additive (attr := simps!) +/-- Given an additive free group basis of `G` over `ι`, there is a canonical bijection between +maps from `ι` to an additive group `H` and morphisms from `G` to `H`. -/] def lift (b : FreeGroupBasis ι G) : (ι → H) ≃ (G →* H) := FreeGroup.lift.trans { toFun := fun f => f.comp b.repr.toMonoidHom @@ -132,12 +168,18 @@ def lift (b : FreeGroupBasis ι G) : (ι → H) ≃ (G →* H) := simp } /-- If two morphisms on `G` coincide on the elements of a basis, then they coincide. -/ +@[to_additive +/-- If two morphisms on `G` coincide on the elements of a basis, then they coincide. -/] lemma ext_hom (b : FreeGroupBasis ι G) (f g : G →* H) (h : ∀ i, f (b i) = g (b i)) : f = g := b.lift.symm.injective <| funext h /-- If a group satisfies the universal property of a free group with respect to a given type, then it admits a free group basis based on this type. Here, the universal property is expressed as in `IsFreeGroup.lift` and its properties. -/ +@[to_additive +/-- If an additive group satisfies the universal property of an additive free group with respect to +a given type, then it admits an additive free group basis based on this type. Here, the universal +property is expressed as in `IsFreeAddGroup.lift` and its properties. -/] def ofLift {G : Type u} [Group G] (X : Type u) (of : X → G) (lift : ∀ {H : Type u} [Group H], (X → H) ≃ (G →* H)) (lift_of : ∀ {H : Type u} [Group H], ∀ (f : X → H) (a), lift f (of a) = f a) : @@ -157,6 +199,10 @@ def ofLift {G : Type u} [Group G] (X : Type u) (of : X → G) /-- If a group satisfies the universal property of a free group with respect to a given type, then it admits a free group basis based on this type. Here the universal property is expressed as in `IsFreeGroup.unique_lift`. -/ +@[to_additive +/-- If an additive group satisfies the universal property of an additive free group with respect to +a given type, then it admits an additive free group basis based on this type. Here +the universal property is expressed as in `IsFreeAddGroup.unique_lift`. -/] def ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G) (h : ∀ {H : Type u} [Group H] (f : X → H), ∃! F : G →* H, ∀ a, F (of a) = f a) : FreeGroupBasis X G := @@ -176,23 +222,29 @@ namespace IsFreeGroup variable (G : Type*) [Group G] [IsFreeGroup G] /-- A set of generators of a free group, chosen arbitrarily -/ +@[to_additive /-- A set of generators of an additive free group, chosen arbitrarily -/] def Generators : Type _ := (IsFreeGroup.nonempty_basis (G := G)).choose /-- Any free group is isomorphic to "the" free group. -/ +@[to_additive /-- Any additive free group is isomorphic to "the" additive free group. -/] irreducible_def mulEquiv : FreeGroup (Generators G) ≃* G := (IsFreeGroup.nonempty_basis (G := G)).choose_spec.some.repr.symm /-- A free group basis of a free group `G`, over the set `Generators G`. -/ +@[to_additive +/-- An additive free group basis of an additive free group `G`, over the set `Generators G`. -/] def basis : FreeGroupBasis (Generators G) G := FreeGroupBasis.ofRepr (mulEquiv G).symm /-- Any free group is isomorphic to "the" free group. -/ -@[simps!] +@[to_additive (attr := simps!) +/-- Any additive free group is isomorphic to "the" additive free group. -/] def toFreeGroup : G ≃* FreeGroup (Generators G) := (mulEquiv G).symm variable {G} /-- The canonical injection of G's generators into G -/ +@[to_additive /-- The canonical injection of G's generators into G -/] def of : Generators G → G := (mulEquiv G).toFun ∘ FreeGroup.of @@ -200,18 +252,22 @@ variable {H : Type*} [Group H] /-- The equivalence between functions on the generators and group homomorphisms from a free group given by those generators. -/ +@[to_additive +/-- The equivalence between functions on the generators and additive group homomorphisms from an +additive free group given by those generators. -/] def lift : (Generators G → H) ≃ (G →* H) := (basis G).lift -@[simp] +@[to_additive (attr := simp)] theorem lift_of (f : Generators G → H) (a : Generators G) : lift f (of a) = f a := congr_fun (lift.symm_apply_apply f) a -@[simp] +@[to_additive (attr := simp)] theorem lift_symm_apply (f : G →* H) (a : Generators G) : (lift.symm f) a = f (of a) := rfl /- Do not register this as an ext lemma, as `Generators G` is not canonical. -/ +@[to_additive /- Do not register this as an ext lemma, as `Generators G` is not canonical. -/] theorem ext_hom ⦃f g : G →* H⦄ (h : ∀ a : Generators G, f (of a) = g (of a)) : f = g := lift.symm.injective (funext h) @@ -220,12 +276,22 @@ group extends in a unique way to a homomorphism from `G`. Note that since `IsFreeGroup.lift` is expressed as a bijection, it already expresses the universal property. -/ +@[to_additive +/-- The universal property of an additive free group: A function from the generators of `G` to +another additive group extends in a unique way to a homomorphism from `G`. + +Note that since `IsFreeAddGroup.lift` is expressed as a bijection, it already +expresses the universal property. -/] theorem unique_lift (f : Generators G → H) : ∃! F : G →* H, ∀ a, F (of a) = f a := by simpa only [funext_iff] using! lift.symm.bijective.existsUnique f /-- If a group satisfies the universal property of a free group with respect to a given type, then it is free. Here, the universal property is expressed as in `IsFreeGroup.lift` and its properties. -/ +@[to_additive +/-- If an additive group satisfies the universal property of an additive free group with respect to +a given type, then it is free. Here, the universal property is expressed as in `IsFreeAddGroup.lift` +and its properties. -/] lemma ofLift {G : Type u} [Group G] (X : Type u) (of : X → G) (lift : ∀ {H : Type u} [Group H], (X → H) ≃ (G →* H)) (lift_of : ∀ {H : Type u} [Group H], ∀ (f : X → H) (a), lift f (of a) = f a) : @@ -234,11 +300,16 @@ lemma ofLift {G : Type u} [Group G] (X : Type u) (of : X → G) /-- If a group satisfies the universal property of a free group with respect to a given type, then it is free. Here the universal property is expressed as in `IsFreeGroup.unique_lift`. -/ +@[to_additive +/-- If an additive group satisfies the universal property of an additive free group with respect to +a given type, then it is free. Here the universal property is expressed as in +`IsFreeAddGroup.unique_lift`. -/] lemma ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : X → G) (h : ∀ {H : Type u} [Group H] (f : X → H), ∃! F : G →* H, ∀ a, F (of a) = f a) : IsFreeGroup G := (FreeGroupBasis.ofUniqueLift X of h).isFreeGroup +@[to_additive] lemma ofMulEquiv (e : G ≃* H) : IsFreeGroup H := ((basis G).map e).isFreeGroup diff --git a/Mathlib/InformationTheory/KullbackLeibler/DataProcessing.lean b/Mathlib/InformationTheory/KullbackLeibler/DataProcessing.lean new file mode 100644 index 0000000000..31a9e198b2 --- /dev/null +++ b/Mathlib/InformationTheory/KullbackLeibler/DataProcessing.lean @@ -0,0 +1,193 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne, Lorenzo Luccioli +-/ +module + +public import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic +public import Mathlib.InformationTheory.KullbackLeibler.Basic +public import Mathlib.Probability.Kernel.Composition.MeasureComp + +import Mathlib.Analysis.Convex.Approximation +import Mathlib.Analysis.Convex.Deriv +import Mathlib.InformationTheory.KullbackLeibler.ChainRule +import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen +import Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym + +/-! +# Data processing inequality for the Kullback-Leibler divergence + +The data processing inequality is a way to express the intuition that applying a (possibly random) +transformation to random variables cannot increase the information they contain. + +## Main statements + +We prove three versions of the data processing inequality for the Kullback-Leibler divergence, for +measurable maps, restrictions to sub-sigma-algebras, and composition with Markov kernels. +Let `μ, ν` be finite measures on `𝓧`, with sigma-algebra `m𝓧`. + +* `klDiv_map_le`: `klDiv (μ.map g) (ν.map g) ≤ klDiv μ ν` for a measurable function `g`. +* `klDiv_trim_le`: `klDiv (μ.trim hm) (ν.trim hm) ≤ klDiv μ ν` for a sub-sigma-algebra `m` of `m𝓧` + (with `hm : m ≤ m𝓧`). +* `klDiv_comp_right_le`: `klDiv (κ ∘ₘ μ) (κ ∘ₘ ν) ≤ klDiv μ ν` for a Markov kernel `κ`. + +-/ + +public section + +open Real MeasureTheory Set ProbabilityTheory +open scoped ENNReal + +namespace ConvexOn + +variable {𝓧 𝓨 : Type*} {m m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} + {μ ν : Measure 𝓧} [IsFiniteMeasure μ] [IsFiniteMeasure ν] {f : ℝ → ℝ} {g : 𝓧 → 𝓨} + +lemma map_condExp_rnDeriv_le (hm : m ≤ m𝓧) (hf : StronglyMeasurable f) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Ici 0) 0) + (h_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) : + (fun x ↦ f ((ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]) x)) ≤ᵐ[ν.trim hm] + ν[fun x ↦ f (μ.rnDeriv ν x).toReal | m] := + hf_cvx.map_condExp_le_trim hm (hf_cvx.continuousOn_Ici hf_cont_at).lowerSemicontinuousOn hf + (ae_of_all _ fun _ ↦ ENNReal.toReal_nonneg) isClosed_Ici Measure.integrable_toReal_rnDeriv h_int + +lemma comp_rnDeriv_map_le (hμν : μ ≪ ν) (hg : Measurable g) (hf : StronglyMeasurable f) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Ici 0) 0) + (h_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) : + (fun x ↦ f ((μ.map g).rnDeriv (ν.map g) (g x)).toReal) ≤ᵐ[ν] + ν[fun x ↦ f (μ.rnDeriv ν x).toReal | m𝓨.comap g] := by + filter_upwards [toReal_rnDeriv_map hμν hg, + ae_of_ae_trim _ <| hf_cvx.map_condExp_rnDeriv_le hg.comap_le hf hf_cont_at h_int] with a ha1 ha2 + calc f ((μ.map g).rnDeriv (ν.map g) (g a)).toReal + = f ((ν[fun x ↦ (μ.rnDeriv ν x).toReal | m𝓨.comap g]) a) := by rw [ha1] + _ ≤ (ν[fun x ↦ f (μ.rnDeriv ν x).toReal | m𝓨.comap g]) a := ha2 + +lemma integrable_comp_rnDeriv_map (hμν : μ ≪ ν) (hg : Measurable g) (hf : StronglyMeasurable f) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Ici 0) 0) + (h_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) : + Integrable (fun x ↦ f ((μ.map g).rnDeriv (ν.map g) x).toReal) (ν.map g) := by + have hf_cont : ContinuousOn f (Ici 0) := hf_cvx.continuousOn_Ici hf_cont_at + obtain ⟨c, c', h⟩ : ∃ c c', ∀ x, 0 ≤ x → c * x + c' ≤ f x := + hf_cvx.exists_affine_le_real isClosed_Ici hf_cont.lowerSemicontinuousOn + rw [integrable_map_measure (StronglyMeasurable.aestronglyMeasurable (by fun_prop)) + hg.aemeasurable] + refine integrable_of_le_of_le (f := fun x ↦ f ((∂μ.map g/∂ν.map g) (g x)).toReal) + (g₁ := fun x ↦ c * ((∂μ.map g/∂ν.map g) (g x)).toReal + c') + (g₂ := fun x ↦ (ν[fun x ↦ f (μ.rnDeriv ν x).toReal | m𝓨.comap g]) x) + ?_ ?_ ?_ ?_ integrable_condExp + · exact StronglyMeasurable.aestronglyMeasurable (by fun_prop) + · exact ae_of_all _ (fun x ↦ h _ ENNReal.toReal_nonneg) + · exact hf_cvx.comp_rnDeriv_map_le hμν hg hf hf_cont_at h_int + · refine (Integrable.const_mul ?_ _).add (integrable_const _) + rw [integrable_congr (toReal_rnDeriv_map hμν hg)] + fun_prop + +lemma comp_rnDeriv_trim_le (hm : m ≤ m𝓧) (hμν : μ ≪ ν) (hf : StronglyMeasurable f) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Ici 0) 0) + (h_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) : + (fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal) ≤ᵐ[ν.trim hm] + ν[fun x ↦ f (μ.rnDeriv ν x).toReal | m] := by + filter_upwards [toReal_rnDeriv_trim hm hμν, + hf_cvx.map_condExp_rnDeriv_le hm hf hf_cont_at h_int] with a ha1 ha2 + calc f ((∂μ.trim hm/∂ν.trim hm) a).toReal + = f ((ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]) a) := by rw [ha1] + _ ≤ (ν[fun x ↦ f (μ.rnDeriv ν x).toReal | m]) a := ha2 + +lemma integrable_comp_rnDeriv_trim (hm : m ≤ m𝓧) (hμν : μ ≪ ν) (hf : StronglyMeasurable f) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Ici 0) 0) + (h_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) : + Integrable (fun x ↦ f ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) (ν.trim hm) := by + have hf_cont : ContinuousOn f (Ici 0) := hf_cvx.continuousOn_Ici hf_cont_at + obtain ⟨c, c', h⟩ : ∃ c c', ∀ x, 0 ≤ x → c * x + c' ≤ f x := + hf_cvx.exists_affine_le_real isClosed_Ici hf_cont.lowerSemicontinuousOn + refine integrable_of_le_of_le (f := fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal) + (g₁ := fun x ↦ c * ((∂μ.trim hm/∂ν.trim hm) x).toReal + c') + (g₂ := fun x ↦ (ν[fun x ↦ f (μ.rnDeriv ν x).toReal | m]) x) + ?_ ?_ ?_ ?_ ?_ + · exact StronglyMeasurable.aestronglyMeasurable (by fun_prop) + · exact ae_of_all _ (fun x ↦ h _ ENNReal.toReal_nonneg) + · exact hf_cvx.comp_rnDeriv_trim_le hm hμν hf hf_cont_at h_int + · exact (Integrable.const_mul (by fun_prop) _).add (integrable_const _) + · exact integrable_condExp.trim hm stronglyMeasurable_condExp + +lemma integrable_comp_condExp_rnDeriv (hm : m ≤ m𝓧) (hμν : μ ≪ ν) (hf : StronglyMeasurable f) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Ici 0) 0) + (h_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) : + Integrable (fun x ↦ f ((ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]) x)) ν := by + have h := integrable_comp_rnDeriv_trim hm hμν hf hf_cvx hf_cont_at h_int + refine integrable_of_integrable_trim hm ((integrable_congr ?_).mp h) + filter_upwards [toReal_rnDeriv_trim hm hμν] with a ha + rw [ha] + +end ConvexOn + +namespace InformationTheory + +variable {𝓧 𝓨 : Type*} {m m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : Measure 𝓧} + [IsFiniteMeasure μ] [IsFiniteMeasure ν] {g : 𝓧 → 𝓨} + +lemma integrable_llr_map (hμν : μ ≪ ν) (hg : Measurable g) + (h_int : Integrable (llr μ ν) μ) : + Integrable (llr (μ.map g) (ν.map g)) (μ.map g) := by + rw [← integrable_klFun_rnDeriv_iff (hμν.map hg)] + refine convexOn_klFun.integrable_comp_rnDeriv_map hμν hg (by fun_prop) (by fun_prop) ?_ + rwa [integrable_klFun_rnDeriv_iff hμν] + +lemma toReal_klDiv_map_of_ac (hμν : μ ≪ ν) (hg : Measurable g) : + (klDiv (μ.map g) (ν.map g)).toReal = + ∫ x, klFun ((ν[fun x ↦ (μ.rnDeriv ν x).toReal | m𝓨.comap g]) x) ∂ν := by + rw [toReal_klDiv_eq_integral_klFun (hμν.map hg), integral_map hg.aemeasurable + (StronglyMeasurable.aestronglyMeasurable (by fun_prop))] + refine integral_congr_ae ?_ + filter_upwards [toReal_rnDeriv_map hμν hg] with a ha using by rw [ha] + +lemma klDiv_map_of_ac (hμν : μ ≪ ν) (hg : Measurable g) (h_int : Integrable (llr μ ν) μ) : + klDiv (μ.map g) (ν.map g) = + ENNReal.ofReal (∫ x, klFun ((ν[fun x ↦ (μ.rnDeriv ν x).toReal | m𝓨.comap g]) x) ∂ν) := by + rw [klDiv_eq_integral_klFun, if_pos ⟨hμν.map hg, integrable_llr_map hμν hg h_int⟩] + congr + rw [← toReal_klDiv_eq_integral_klFun (hμν.map hg), toReal_klDiv_map_of_ac hμν hg] + +lemma toReal_klDiv_trim_of_ac (hm : m ≤ m𝓧) (hμν : μ ≪ ν) : + (klDiv (μ.trim hm) (ν.trim hm)).toReal = + ∫ x, klFun ((ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]) x) ∂ν := by + simp [trim_eq_map, toReal_klDiv_map_of_ac hμν (measurable_id'' hm)] + +variable (μ ν) in +/-- **Data processing inequality** for the Kullback-Leibler divergence and measurable functions. -/ +theorem klDiv_map_le (hg : Measurable g) : klDiv (μ.map g) (ν.map g) ≤ klDiv μ ν := by + by_cases hμν : μ ≪ ν + swap; · simp [hμν] + by_cases h_int : Integrable (llr μ ν) μ + swap; · simp [klDiv_of_not_integrable h_int] + rw [klDiv_map_of_ac hμν hg h_int, klDiv_eq_integral_klFun] + simp only [hμν, h_int, and_self, ↓reduceIte] + conv_rhs => rw [← integral_condExp hg.comap_le] + gcongr 1 + have hf : StronglyMeasurable klFun := by fun_prop + have hf_cont : ContinuousWithinAt klFun (Ici 0) 0 := by fun_prop + have h_int' : Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν := by + rwa [integrable_klFun_rnDeriv_iff hμν] + refine integral_mono_ae ?_ integrable_condExp ?_ + · exact convexOn_klFun.integrable_comp_condExp_rnDeriv hg.comap_le hμν hf hf_cont h_int' + · refine ae_of_ae_trim hg.comap_le ?_ + exact convexOn_klFun.map_condExp_rnDeriv_le hg.comap_le hf hf_cont h_int' + +variable (μ ν) in +/-- **Data processing inequality** for the Kullback-Leibler divergence and sub-sigma-algebras. -/ +theorem klDiv_trim_le (hm : m ≤ m𝓧) : klDiv (μ.trim hm) (ν.trim hm) ≤ klDiv μ ν := by + simp_rw [trim_eq_map] + exact klDiv_map_le μ ν (measurable_id'' hm) + +variable (μ ν) in +/-- The **Data Processing Inequality** for the Kullback-Leibler divergence and a Markov kernel. -/ +theorem klDiv_comp_right_le (κ : Kernel 𝓧 𝓨) [IsMarkovKernel κ] : + klDiv (κ ∘ₘ μ) (κ ∘ₘ ν) ≤ klDiv μ ν := + calc klDiv (κ ∘ₘ μ) (κ ∘ₘ ν) + _ ≤ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) := by + rw [← Measure.snd_compProd, ← Measure.snd_compProd] + exact klDiv_map_le _ _ measurable_snd + _ = klDiv μ ν := klDiv_compProd_left μ ν κ + +end InformationTheory diff --git a/Mathlib/LinearAlgebra/Dimension/Localization.lean b/Mathlib/LinearAlgebra/Dimension/Localization.lean index d1034e2476..fb6dfbb307 100644 --- a/Mathlib/LinearAlgebra/Dimension/Localization.lean +++ b/Mathlib/LinearAlgebra/Dimension/Localization.lean @@ -5,11 +5,11 @@ Authors: Andrew Yang -/ module +public import Mathlib.Algebra.Group.Pointwise.Finset.Scalar public import Mathlib.Algebra.Module.LocalizedModule.Submodule public import Mathlib.LinearAlgebra.Dimension.DivisionRing -public import Mathlib.RingTheory.IsTensorProduct +public import Mathlib.LinearAlgebra.LinearIndependent.Algebra public import Mathlib.RingTheory.Localization.BaseChange -public import Mathlib.RingTheory.Localization.FractionRing public import Mathlib.RingTheory.OreLocalization.OreSet /-! @@ -77,6 +77,22 @@ theorem IsLocalization.finrank_eq : finrank S N = finrank R N := by end +variable {S} in +theorem IsLocalization.linearIndepOn_finsetIntegerMultiple {A : Type*} [CommRing A] [Algebra S A] + [Algebra R A] [IsScalarTower R S A] (M : Submonoid S) [IsLocalization M A] [FaithfulSMul S A] + {s : Finset A} (hs : LinearIndepOn R id (s : Set A)) [DecidableEq S] : + LinearIndepOn R id (finsetIntegerMultiple M s : Set S) := by + classical + rw [← LinearIndepOn.id_image_algebraMap_iff (A := A), + finsetIntegerMultiple_image, ← s.coe_smul_finset] + rw [linearIndepOn_finset_iff] at hs ⊢ + intro f h + rw [s.smul_finset_def, s.forall_mem_image] + apply hs + have inj := (IsLocalization.smul_bijective A (commonDenomOfFinset M s)).injective + rw [← inj.eq_iff, smul_zero, s.smul_sum, ← h, s.smul_finset_def, s.sum_image inj.injOn] + exact s.sum_congr rfl fun x hx ↦ smul_comm .. + section variable (R N) [IsFractionRing R S] @@ -91,12 +107,48 @@ theorem IsFractionRing.rank_right_eq : Module.rank S N = Module.rank R N := /-- Given `IsScalarTower R S N`, if `S` is the fraction ring of `R`, then the finrank `finrank S N` of the right part of the tower equals the finrank `finrank R N` of the whole tower. -See `IsFractionRing.rank_right_eq` for the rank version. -/ +See `IsFractionRing.rank_right_eq` for the rank version. +See `IsFractionRing.finrank_left_eq` for the left version. +See `IsFractionRing.finrank_eq` for the simultaneous version. -/ theorem IsFractionRing.finrank_right_eq : finrank S N = finrank R N := IsLocalization.finrank_eq S R⁰ le_rfl end +variable (R) in +open IsLocalization in +/-- Given `IsScalarTower R S A`, if `A` is the fraction ring of `S`, then the finrank `finrank R S` +of the left part of the tower equals the finrank `finrank R A` of the whole tower. + +See `IsFractionRing.finrank_right_eq` for the right version. +See `IsFractionRing.finrank_eq` for the simultaneous version. -/ +theorem IsFractionRing.finrank_left_eq (A : Type*) [CommRing A] [Algebra S A] [Algebra R A] + [IsScalarTower R S A] [IsFractionRing S A] : Module.finrank R S = Module.finrank R A := by + nontriviality R + classical + apply Cardinal.toNat_eq_of_forall_le_iff + intro n + simp_rw [Module.le_rank_iff_exists_finset, LinearIndepOn] + constructor + · rintro ⟨s, rfl, hs⟩ + let f : S ↪ A := ⟨algebraMap S A, FaithfulSMul.algebraMap_injective S A⟩ + exact ⟨s.map f, s.card_map f, + (linearIndependent_equiv (s.equivMap f)).mp (LinearIndependent.algebraMap_comp_iff.mpr hs)⟩ + · rintro ⟨s, rfl, hs⟩ + exact ⟨finsetIntegerMultiple S⁰ s, card_finsetIntegerMultiple S⁰ s, + linearIndepOn_finsetIntegerMultiple S⁰ hs⟩ + +/-- If `K` is the fraction ring of `A` and `L` is the fraction ring of `B`, then the finrank +`finrank K L` of the fraction rings equals the finrank `finrank A B` of the base rings. + +See `IsFractionRing.finrank_left_eq` and `IsFractionRing.finrank_right_eq` for one-sided versions. +See `Algebra.IsAlgebraic.rank_of_isFractionRing` for a rank version with additional assumptions. -/ +protected theorem IsFractionRing.finrank_eq (A K B L : Type*) + [CommRing A] [CommRing K] [CommRing B] [CommRing L] [Algebra A B] [Module K L] + [Algebra A K] [Algebra B L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] + [IsFractionRing A K] [IsFractionRing B L] : Module.finrank K L = Module.finrank A B := + (finrank_right_eq A K L).trans (finrank_left_eq A B L).symm + variable (R M) in theorem exists_set_linearIndependent_of_isDomain [IsDomain R] : ∃ s : Set M, #s = Module.rank R M ∧ LinearIndepOn R id s := by diff --git a/Mathlib/LinearAlgebra/Eigenspace/ContinuousLinearMap.lean b/Mathlib/LinearAlgebra/Eigenspace/ContinuousLinearMap.lean index cd95994b29..e270d5292e 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/ContinuousLinearMap.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/ContinuousLinearMap.lean @@ -26,8 +26,7 @@ variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] [TopologicalSp open Module End instance isClosed_genEigenspace : IsClosed (genEigenspace (f : End R M) μ n : Set M) := by - rw [genEigenspace_nat, one_eq_id, ← coe_id, ← toLinearMap_smul, ← toLinearMap_sub, ← coe_pow] - apply isClosed_ker + simpa [genEigenspace_nat] using isClosed_ker ↑((f - μ • 1) ^ n) instance isClosed_eigenspace : IsClosed (eigenspace (f : End R M) μ : Set M) := isClosed_genEigenspace f μ 1 diff --git a/Mathlib/LinearAlgebra/Matrix/Cartan.lean b/Mathlib/LinearAlgebra/Matrix/Cartan.lean index c0fe19186c..bb65489455 100644 --- a/Mathlib/LinearAlgebra/Matrix/Cartan.lean +++ b/Mathlib/LinearAlgebra/Matrix/Cartan.lean @@ -10,6 +10,7 @@ public import Mathlib.LinearAlgebra.Matrix.Notation public import Mathlib.GroupTheory.Perm.Cycle.Concrete public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic public import Mathlib.LinearAlgebra.Matrix.Symmetric +import Mathlib.Tactic.NormDet /-! # Cartan matrices @@ -257,16 +258,16 @@ theorem G₂_det : G₂.det = 1 := by decide theorem F₄_det : F₄.det = 1 := by decide -/-! The determinants of E₆, E₇, E₈ are 3, 2, 1 respectively. -`decide` fails for these larger matrices without increasing the max recursion depth. -We could write manual proofs (e.g., expanding via `det_succ_column_zero`), -but prefer to wait for a more principled determinant tactic. -/ +/-! The determinants of E₆, E₇, E₈ are 3, 2, 1 respectively. -/ -proof_wanted E₆_det : E₆.det = 3 +theorem E₆_det : E₆.det = 3 := by + simp only [E₆, norm_det] -proof_wanted E₇_det : E₇.det = 2 +theorem E₇_det : E₇.det = 2 := by + simp only [E₇, norm_det] -proof_wanted E₈_det : E₈.det = 1 +theorem E₈_det : E₈.det = 1 := by + simp only [E₈, norm_det] /-- A Cartan matrix is simply laced if its off-diagonal entries are all `0` or `-1`. -/ def _root_.Matrix.IsSimplyLaced {ι : Type*} (A : Matrix ι ι ℤ) : Prop := diff --git a/Mathlib/LinearAlgebra/Matrix/Notation.lean b/Mathlib/LinearAlgebra/Matrix/Notation.lean index d0b88f3a65..0508d80710 100644 --- a/Mathlib/LinearAlgebra/Matrix/Notation.lean +++ b/Mathlib/LinearAlgebra/Matrix/Notation.lean @@ -228,7 +228,7 @@ section ColRow variable {ι : Type*} @[simp] -theorem replicateCol_empty (v : Fin 0 → α) : replicateCol ι v = vecEmpty := +theorem replicateCol_empty (v : Fin 0 → α) : replicateCol ι v = of vecEmpty := empty_eq _ set_option backward.isDefEq.respectTransparency false in @@ -368,7 +368,7 @@ section VecMulVec variable [NonUnitalNonAssocSemiring α] @[simp] -theorem empty_vecMulVec (v : Fin 0 → α) (w : n' → α) : vecMulVec v w = ![] := +theorem empty_vecMulVec (v : Fin 0 → α) (w : n' → α) : vecMulVec v w = of ![] := empty_eq _ @[simp] @@ -401,7 +401,7 @@ section Submatrix @[simp] theorem submatrix_empty (A : Matrix m' n' α) (row : Fin 0 → m') (col : o' → n') : - submatrix A row col = ![] := + submatrix A row col = of ![] := empty_eq _ set_option backward.isDefEq.respectTransparency false in diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean index 7e91e553f4..4b990aaa2e 100644 --- a/Mathlib/Logic/Relation.lean +++ b/Mathlib/Logic/Relation.lean @@ -56,9 +56,9 @@ open Function variable {α β γ δ ε ζ : Type*} -theorem Subrelation.antisymm {r r' : α → α → Prop} (h1 : Subrelation r r') (h2 : Subrelation r' r) : +theorem Subrelation.antisymm {r r' : α → α → Prop} (h1 : r ≤ r') (h2 : r' ≤ r) : r = r' := - funext₂ fun _ _ => propext ⟨h1, h2⟩ + funext₂ fun a b => propext ⟨h1 a b, h2 a b⟩ section NeImp @@ -816,34 +816,33 @@ theorem mono {r p : α → α → Prop} (hrp : r ≤ p) : EqvGen r ≤ EqvGen p | symm a b _ ih => exact EqvGen.symm _ _ ih | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc -lemma eqvGen_le {r r' : α → α → Prop} [IsEquiv α r'] (h : Subrelation r r') : - Subrelation (EqvGen r) r' +lemma eqvGen_le {r r' : α → α → Prop} [IsEquiv α r'] (h : r ≤ r') : EqvGen r ≤ r' | _, _, .refl _ => _root_.refl _ - | _, _, .symm _ _ hxy => _root_.symm (eqvGen_le h hxy :) - | _, _, .trans _ _ _ hxy hyz => _root_.trans (eqvGen_le h hxy :) (eqvGen_le h hyz :) - | _, _, .rel _ _ hab => h hab + | _, _, .symm _ _ hxy => _root_.symm (eqvGen_le h _ _ hxy) + | _, _, .trans _ _ _ hxy hyz => _root_.trans (eqvGen_le h _ _ hxy) (eqvGen_le h _ _ hyz) + | _, _, .rel _ _ hab => h _ _ hab -lemma eqvGen_mono {r r' : α → α → Prop} (h : Subrelation r r') : Subrelation (EqvGen r) (EqvGen r') +lemma eqvGen_mono {r r' : α → α → Prop} (h : r ≤ r') : EqvGen r ≤ EqvGen r' | _, _, .refl _ => .refl _ - | _, _, .symm _ _ hxy => .symm _ _ (eqvGen_mono h hxy) - | _, _, .trans _ _ _ hxy hyz => .trans _ _ _ (eqvGen_mono h hxy) (eqvGen_mono h hyz) - | _, _, .rel _ _ hab => .rel _ _ (h hab) + | _, _, .symm _ _ hxy => .symm _ _ (eqvGen_mono h _ _ hxy) + | _, _, .trans _ _ _ hxy hyz => .trans _ _ _ (eqvGen_mono h _ _ hxy) (eqvGen_mono h _ _ hyz) + | _, _, .rel _ _ hab => .rel _ _ (h _ _ hab) -lemma reflGen_le_eqvGen : Subrelation (ReflGen r) (EqvGen r) +lemma reflGen_le_eqvGen : ReflGen r ≤ EqvGen r | _, _, .refl => .refl _ | _, _, .single h => .rel _ _ h -lemma symmGen_le_eqvGen : Subrelation (SymmGen r) (EqvGen r) +lemma symmGen_le_eqvGen : SymmGen r ≤ EqvGen r | _, _, .inl h => .rel _ _ h | _, _, .inr h => _root_.symm <| .rel _ _ h -lemma transGen_le_eqvGen : Subrelation (TransGen r) (EqvGen r) := by +lemma transGen_le_eqvGen : TransGen r ≤ EqvGen r := by intro _ _ h induction h using TransGen.trans_induction_on with | trans _ _ h1 h2 => exact _root_.trans h1 h2 | single h => exact .rel _ _ h -lemma reflTransGen_le_eqvGen : Subrelation (ReflTransGen r) (EqvGen r) := by +lemma reflTransGen_le_eqvGen : ReflTransGen r ≤ EqvGen r := by intro _ _ h induction h using ReflTransGen.trans_induction_on with | refl => exact .refl _ @@ -853,27 +852,27 @@ lemma reflTransGen_le_eqvGen : Subrelation (ReflTransGen r) (EqvGen r) := by @[simp, grind =] lemma eqvGen_reflGen : EqvGen (ReflGen r) = EqvGen r := Subrelation.antisymm - (eqvGen_le (reflGen_le_eqvGen _)) (eqvGen_mono (.single)) + (eqvGen_le (reflGen_le_eqvGen _)) (eqvGen_mono fun _ _ => .single) @[simp, grind =] lemma eqvGen_transGen : EqvGen (TransGen r) = EqvGen r := Subrelation.antisymm - (eqvGen_le (transGen_le_eqvGen _)) (eqvGen_mono .single) + (eqvGen_le (transGen_le_eqvGen _)) (eqvGen_mono fun _ _ => .single) @[simp, grind =] lemma eqvGen_symmGen : EqvGen (SymmGen r) = EqvGen r := Subrelation.antisymm - (eqvGen_le (symmGen_le_eqvGen _)) (eqvGen_mono .inl) + (eqvGen_le (symmGen_le_eqvGen _)) (eqvGen_mono fun _ _ => .inl) @[simp, grind =] lemma eqvGen_reflTransGen : EqvGen (ReflTransGen r) = EqvGen r := Subrelation.antisymm - (eqvGen_le (reflTransGen_le_eqvGen _)) (eqvGen_mono .single) + (eqvGen_le (reflTransGen_le_eqvGen _)) (eqvGen_mono fun _ _ => .single) @[grind =] lemma eqvGen_eq_reflTransGen [Std.Symm r] : EqvGen r = ReflTransGen r := have : IsEquiv α (ReflTransGen r) := ⟨⟩ - Subrelation.antisymm (eqvGen_le .single) (reflTransGen_le_eqvGen _) + Subrelation.antisymm (eqvGen_le fun _ _ => .single) (reflTransGen_le_eqvGen _) lemma reflTransGen_symmGen : ReflTransGen (SymmGen r) = EqvGen r := by rw [← eqvGen_eq_reflTransGen, eqvGen_symmGen] diff --git a/Mathlib/MeasureTheory/Measure/Decomposition/IntegralRNDeriv.lean b/Mathlib/MeasureTheory/Measure/Decomposition/IntegralRNDeriv.lean index c0208fbb63..5d5c670a5a 100644 --- a/Mathlib/MeasureTheory/Measure/Decomposition/IntegralRNDeriv.lean +++ b/Mathlib/MeasureTheory/Measure/Decomposition/IntegralRNDeriv.lean @@ -50,14 +50,7 @@ lemma le_integral_rnDeriv_of_ac [IsFiniteMeasure μ] [IsProbabilityMeasure ν] (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousWithinAt f (Ici 0) 0) (hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) (hμν : μ ≪ ν) : f (μ.real univ) ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν := by - have hf_cont' : ContinuousOn f (Ici 0) := by - intro x hx - rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos - · exact hf_cont - · have h := hf_cvx.continuousOn_interior x - simp only [nonempty_Iio, interior_Ici', mem_Ioi] at h - rw [continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hx_pos)] at h - exact (h hx_pos).continuousWithinAt + have hf_cont' : ContinuousOn f (Ici 0) := hf_cvx.continuousOn_Ici hf_cont calc f (μ.real univ) = f (∫ x, (μ.rnDeriv ν x).toReal ∂ν) := by rw [Measure.integral_toReal_rnDeriv hμν] _ ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν := by @@ -140,14 +133,7 @@ lemma _root_.ConvexOn.apply_rnDeriv_ae_le_integral (hf : StronglyMeasurable f) (hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η) : (fun a ↦ f (μ.rnDeriv ν a).toReal) ≤ᵐ[ν] fun a ↦ ∫ b, f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal ∂(η a) := by - have hf_cont : ContinuousOn f (Ici 0) := by - intro x hx - rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos - · exact hf_cont_at - · have h := hf_cvx.continuousOn_interior x (by simpa) - simp only [nonempty_Iio, interior_Ici', - continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hx_pos)] at h - exact h.continuousWithinAt + have hf_cont : ContinuousOn f (Ici 0) := hf_cvx.continuousOn_Ici hf_cont_at have h_lt_top : ∀ᵐ a ∂ν, ∀ᵐ b ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞ := Measure.ae_ae_of_ae_compProd <| (μ ⊗ₘ κ).rnDeriv_lt_top (ν ⊗ₘ η) have h_integrable : Integrable (fun x ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η) := @@ -193,14 +179,7 @@ lemma _root_.ConvexOn.integrable_apply_rnDeriv_of_integrable_compProd (hf : Stro (hf_int : Integrable (fun p ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)) (hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η) : Integrable (fun a ↦ f (μ.rnDeriv ν a).toReal) ν := by - have hf_cont : ContinuousOn f (Ici 0) := by - intro x hx - rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos - · exact hf_cont_at - · have h := hf_cvx.continuousOn_interior x (by simpa) - simp only [nonempty_Iio, interior_Ici', - continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hx_pos)] at h - exact h.continuousWithinAt + have hf_cont : ContinuousOn f (Ici 0) := hf_cvx.continuousOn_Ici hf_cont_at obtain ⟨c, c', h⟩ : ∃ c c', ∀ x, 0 ≤ x → c * x + c' ≤ f x := hf_cvx.exists_affine_le_real isClosed_Ici hf_cont.lowerSemicontinuousOn refine integrable_of_le_of_le (f := fun a ↦ f (μ.rnDeriv ν a).toReal) diff --git a/Mathlib/MeasureTheory/VectorMeasure/SetIntegral.lean b/Mathlib/MeasureTheory/VectorMeasure/SetIntegral.lean index a875cde597..27d13a7ced 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/SetIntegral.lean +++ b/Mathlib/MeasureTheory/VectorMeasure/SetIntegral.lean @@ -252,7 +252,7 @@ theorem setIntegral_of_variation_apply_eq_zero (f : X → E) {s : Set X} rw [variation_restrict h's] apply Measure.restrict_eq_zero.2 hs have : μ.restrict s = 0 := variation_eq_zero.1 this - simpa [integral_eq_setToFun, this] using! setToFun_zero_left + simp [this] theorem setIntegral_dirac' {mX : MeasurableSpace X} [CompleteSpace G] {a : X} {v : F} (hf : StronglyMeasurable f) {s : Set X} (hs : MeasurableSet s) [Decidable (a ∈ s)] : diff --git a/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean b/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean index 390947d240..a7edac6433 100644 --- a/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean +++ b/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean @@ -182,10 +182,9 @@ lemma norm_jacobiTheta₂_term_fderiv_ge (n : ℤ) (z τ : ℂ) : refine (ContinuousLinearMap.le_opNorm _ _).trans ?_ simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl] refine le_trans ?_ this - simp_rw [jacobiTheta₂_term_fderiv, jacobiTheta₂_term, FunLike.coe_smul', - Pi.smul_apply, add_apply, FunLike.coe_smul', - ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', Pi.smul_apply, smul_zero, zero_add, - smul_eq_mul, mul_one, mul_comm _ ‖cexp _‖, norm_mul] + simp_rw [jacobiTheta₂_term_fderiv, jacobiTheta₂_term, FunLike.coe_smul, Pi.smul_apply, add_apply, + FunLike.coe_smul, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', Pi.smul_apply, + smul_zero, zero_add, smul_eq_mul, mul_one, mul_comm _ ‖cexp _‖, norm_mul] refine mul_le_mul_of_nonneg_left (le_of_eq ?_) (norm_nonneg _) simp_rw [norm_real, norm_of_nonneg pi_pos.le, norm_I, mul_one, Int.cast_abs, ← norm_intCast, norm_pow] @@ -346,11 +345,8 @@ lemma hasDerivAt_jacobiTheta₂_fst (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) : ((jacobiTheta₂_fderiv z τ) (1, 0)) := by apply eval_fst_CLM.hasSum (hasSum_jacobiTheta₂_term_fderiv z hτ) have step2 (n : ℤ) : (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ := by - simp only [jacobiTheta₂_term_fderiv, smul_add, add_apply, - FunLike.coe_smul', ContinuousLinearMap.coe_fst', Pi.smul_apply, smul_eq_mul, - mul_one, ContinuousLinearMap.coe_snd', mul_zero, add_zero, jacobiTheta₂'_term, - jacobiTheta₂_term, mul_comm _ (cexp _)] - rw [funext step2] at step1 + simp [jacobiTheta₂_term_fderiv, jacobiTheta₂'_term, jacobiTheta₂_term, mul_comm] + simp only [step2] at step1 have step3 : HasDerivAt (fun x ↦ jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ) (1, 0)) z := (((hasFDerivAt_jacobiTheta₂ z hτ).comp z (hasFDerivAt_prodMk_left z τ)).hasDerivAt :) rwa [← step1.tsum_eq] at step3 diff --git a/Mathlib/Order/Interval/Finset/Floor.lean b/Mathlib/Order/Interval/Finset/Floor.lean new file mode 100644 index 0000000000..242c5e3662 --- /dev/null +++ b/Mathlib/Order/Interval/Finset/Floor.lean @@ -0,0 +1,84 @@ +/- +Copyright (c) 2026 Terence Tao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Terence Tao +-/ +module + +public import Mathlib.Algebra.Order.Floor.Semiring +public import Mathlib.Data.Int.Interval +public import Mathlib.Order.Interval.Finset.Nat + +/-! +# Membership in intervals via `Int.floor` / `Nat.floor` / `Int.ceil` / `Nat.ceil` + +For a `FloorRing` (resp. `FloorSemiring`) `α`, we relate membership of a cast `↑n` in an interval +of `α` to membership of the integer (resp. natural number) `n` in the corresponding interval with +floor/ceil endpoints, for instance `Int.cast_mem_Ioc_iff : ↑n ∈ Set.Ioc a b ↔ n ∈ Set.Ioc ⌊a⌋ ⌊b⌋`. +If the right-hand side set is finite, we express it as `Finset` instead. + +In the natural number case, non-negativity hypotheses are required when the `Nat.floor` function +is involved. In the `IsStrictOrderedRing` case, one of these hypotheses can be omitted. +-/ + +@[expose] public section + +namespace Int + +variable {α : Type*} [Ring α] [LinearOrder α] [FloorRing α] {a b : α} {n : ℤ} + +lemma cast_mem_Ioc_iff : ↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋ := by + simp [floor_lt, le_floor] + +lemma cast_mem_Ico_iff : ↑n ∈ Set.Ico a b ↔ n ∈ Finset.Ico ⌈a⌉ ⌈b⌉ := by + simp [ceil_le, lt_ceil] + +lemma cast_mem_Icc_iff : ↑n ∈ Set.Icc a b ↔ n ∈ Finset.Icc ⌈a⌉ ⌊b⌋ := by + simp [ceil_le, le_floor] + +lemma cast_mem_Ioo_iff : ↑n ∈ Set.Ioo a b ↔ n ∈ Finset.Ioo ⌊a⌋ ⌈b⌉ := by + simp [floor_lt, lt_ceil] + +lemma cast_mem_Ioi_iff : ↑n ∈ Set.Ioi a ↔ n ∈ Set.Ioi ⌊a⌋ := by simp [floor_lt] + +lemma cast_mem_Ici_iff : ↑n ∈ Set.Ici a ↔ n ∈ Set.Ici ⌈a⌉ := by simp [ceil_le] + +lemma cast_mem_Iic_iff : ↑n ∈ Set.Iic b ↔ n ∈ Set.Iic ⌊b⌋ := by simp [le_floor] + +lemma cast_mem_Iio_iff : ↑n ∈ Set.Iio b ↔ n ∈ Set.Iio ⌈b⌉ := by simp [lt_ceil] + +end Int + +namespace Nat + +variable {α : Type*} [Semiring α] [LinearOrder α] [FloorSemiring α] {a b : α} {n : ℕ} + +lemma cast_mem_Ioc_iff (ha : 0 ≤ a) (hb : 0 ≤ b) : + ↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊ := by simp [floor_lt ha, le_floor_iff hb] + +/-- The `0 ≤ b` hypothesis in `cast_mem_Ioc_iff` can be dropped if `IsStrictOrderedRing α`. -/ +lemma cast_mem_Ioc_iff' [IsStrictOrderedRing α] (ha : 0 ≤ a) : + ↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊ := by + rcases le_or_gt 0 b with hb | hb + · exact cast_mem_Ioc_iff ha hb + · grind [floor_of_nonpos hb.le] + +lemma cast_mem_Ico_iff : ↑n ∈ Set.Ico a b ↔ n ∈ Finset.Ico ⌈a⌉₊ ⌈b⌉₊ := by + simp [ceil_le, lt_ceil] + +lemma cast_mem_Icc_iff (hb : 0 ≤ b) : ↑n ∈ Set.Icc a b ↔ n ∈ Finset.Icc ⌈a⌉₊ ⌊b⌋₊ := by + simp [ceil_le, le_floor_iff hb] + +lemma cast_mem_Ioo_iff (ha : 0 ≤ a) : ↑n ∈ Set.Ioo a b ↔ n ∈ Finset.Ioo ⌊a⌋₊ ⌈b⌉₊ := by + simp [floor_lt ha, lt_ceil] + +lemma cast_mem_Iic_iff (hb : 0 ≤ b) : ↑n ∈ Set.Iic b ↔ n ∈ Finset.Iic ⌊b⌋₊ := by + simp [le_floor_iff hb] + +lemma cast_mem_Iio_iff : ↑n ∈ Set.Iio b ↔ n ∈ Finset.Iio ⌈b⌉₊ := by simp [lt_ceil] + +lemma cast_mem_Ioi_iff (ha : 0 ≤ a) : ↑n ∈ Set.Ioi a ↔ n ∈ Set.Ioi ⌊a⌋₊ := by simp [floor_lt ha] + +lemma cast_mem_Ici_iff : ↑n ∈ Set.Ici a ↔ n ∈ Set.Ici ⌈a⌉₊ := by simp [ceil_le] + +end Nat diff --git a/Mathlib/Order/JordanHolder.lean b/Mathlib/Order/JordanHolder.lean index 7495b6259c..7b7671e89e 100644 --- a/Mathlib/Order/JordanHolder.lean +++ b/Mathlib/Order/JordanHolder.lean @@ -116,7 +116,7 @@ theorem Iso.rel (h_rel : ∀ {x y}, IsMaximal x (x ⊔ y) → e (x, x ⊔ y) (x ⊓ y, y)) {x y : X × X} (h_iso : Iso x y) : e x y := by have : IsEquiv (X × X) e := { refl _ := h_refl, symm _ _ := h_symm, trans _ _ _ := h_trans } - refine Relation.EqvGen.eqvGen_le ?_ h_iso + refine Relation.EqvGen.eqvGen_le ?_ _ _ h_iso rintro ⟨a, b⟩ ⟨c, d⟩ ⟨h, rfl : b = a ⊔ d, rfl : c = a ⊓ d⟩ exact h_rel h diff --git a/Mathlib/Probability/Distributions/Gaussian/Basic.lean b/Mathlib/Probability/Distributions/Gaussian/Basic.lean index 3163c58577..8bf1f96a53 100644 --- a/Mathlib/Probability/Distributions/Gaussian/Basic.lean +++ b/Mathlib/Probability/Distributions/Gaussian/Basic.lean @@ -51,8 +51,10 @@ instance IsGaussian.toIsProbabilityMeasure {E : Type*} [TopologicalSpace E] [Add [Module ℝ E] {mE : MeasurableSpace E} (μ : Measure E) [IsGaussian μ] : IsProbabilityMeasure μ where measure_univ := by - have : μ.map (0 : StrongDual ℝ E) Set.univ = 1 := by simp [IsGaussian.map_eq_gaussianReal] - simpa [Measure.map_apply (by fun_prop : Measurable (0 : StrongDual ℝ E)) .univ] using this + have : μ.map (0 : StrongDual ℝ E) Set.univ = 1 := by + simp [-FunLike.coe_zero, IsGaussian.map_eq_gaussianReal] + simpa [-FunLike.coe_zero, + Measure.map_apply (by fun_prop : Measurable (0 : StrongDual ℝ E)) .univ] using this /-- A real Gaussian measure is Gaussian. -/ instance isGaussian_gaussianReal (m : ℝ) (v : ℝ≥0) : IsGaussian (gaussianReal m v) where @@ -171,8 +173,7 @@ theorem isGaussian_iff_charFunDual_eq {μ : Measure E} [IsFiniteMeasure μ] : refine ⟨fun h ↦ h.charFunDual_eq, fun h ↦ ⟨fun L ↦ Measure.ext_of_charFun ?_⟩⟩ ext u rw [charFun_map_eq_charFunDual_smul L u, h (u • L), charFun_gaussianReal] - simp only [FunLike.coe_smul', Pi.smul_apply, smul_eq_mul, ofReal_mul, - Real.coe_toNNReal'] + simp only [smul_apply, smul_eq_mul, ofReal_mul, Real.coe_toNNReal'] congr · rw [integral_const_mul, integral_complex_ofReal] · rw [max_eq_left (variance_nonneg _ _), mul_comm, ← ofReal_pow, ← ofReal_mul, diff --git a/Mathlib/RepresentationTheory/Rep/Basic.lean b/Mathlib/RepresentationTheory/Rep/Basic.lean index 0927674493..3233d4c0f6 100644 --- a/Mathlib/RepresentationTheory/Rep/Basic.lean +++ b/Mathlib/RepresentationTheory/Rep/Basic.lean @@ -570,6 +570,8 @@ instance : Limits.ReflectsLimitsOfSize.{w, w} (forget₂ (Rep.{w} k G) (ModuleCa instance : Limits.ReflectsColimitsOfSize.{w, w} (forget₂ (Rep.{w} k G) (ModuleCat k)) := Limits.reflectsColimits_of_reflectsIsomorphisms +instance : Abelian (Rep.{w} k G) := abelianOfEquivalence (RepToAction k G) + variable {k G} in theorem epi_iff_surjective (f : A ⟶ B) : Epi f ↔ Function.Surjective f.hom := ⟨fun _ => (ModuleCat.epi_iff_surjective ((forget₂ _ _).map f)).1 inferInstance, diff --git a/Mathlib/RepresentationTheory/Rep/Iso.lean b/Mathlib/RepresentationTheory/Rep/Iso.lean index aa51648026..4c3818e73a 100644 --- a/Mathlib/RepresentationTheory/Rep/Iso.lean +++ b/Mathlib/RepresentationTheory/Rep/Iso.lean @@ -168,8 +168,6 @@ instance : (toModuleMonoidAlgebra.{w} (k := k) (G := G)).IsEquivalence := instance : (ofModuleMonoidAlgebra (k := k) (G := G)).IsEquivalence := (equivalenceModuleMonoidAlgebra (k := k) (G := G)).isEquivalence_inverse -instance : Abelian (Rep.{w} k G) := abelianOfEquivalence toModuleMonoidAlgebra - -- TODO Verify that the equivalence with `ModuleCat k[G]` is a monoidal functor. variable {k G : Type u} [CommRing k] [Monoid G] in diff --git a/Mathlib/RingTheory/Algebraic/Integral.lean b/Mathlib/RingTheory/Algebraic/Integral.lean index c62601e359..1dd7574f73 100644 --- a/Mathlib/RingTheory/Algebraic/Integral.lean +++ b/Mathlib/RingTheory/Algebraic/Integral.lean @@ -547,8 +547,7 @@ theorem lift_rank_of_isFractionRing : rw [IsLocalization.rank_eq R' R⁰ le_rfl, IsLocalizedModule.lift_rank_eq R⁰ (IsScalarTower.toAlgHom R S S').toLinearMap le_rfl] -theorem finrank_of_isFractionRing : Module.finrank R' S' = Module.finrank R S := by - simpa using! congr_arg Cardinal.toNat (lift_rank_of_isFractionRing ..) +@[deprecated (since := "2026-07-13")] alias finrank_of_isFractionRing := IsFractionRing.finrank_eq theorem rank_of_isFractionRing (S' : Type u) [CommRing S'] [Algebra R S'] [Algebra S S'] [Module R' S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsFractionRing S S'] : diff --git a/Mathlib/RingTheory/Finiteness/Basic.lean b/Mathlib/RingTheory/Finiteness/Basic.lean index 48ec5fc228..3f21935a1d 100644 --- a/Mathlib/RingTheory/Finiteness/Basic.lean +++ b/Mathlib/RingTheory/Finiteness/Basic.lean @@ -244,19 +244,18 @@ instance (priority := 100) of_finite [Finite M] : Module.Finite R M := by section -variable {S} {P : Type*} [Semiring S] [AddCommMonoid P] [Module S P] - {σ : R →+* S} [RingHomSurjective σ] +variable {S} {P : Type*} [Semiring S] [AddCommMonoid P] [Module S P] {σ : R →+* S} --- TODO: remove RingHomSurjective @[stacks 0519 "(3)"] theorem of_surjective [hM : Module.Finite R M] (f : M →ₛₗ[σ] P) (hf : Surjective f) : - Module.Finite S P := - ⟨by - rw [← LinearMap.range_eq_top.mpr hf, ← Submodule.map_top] - exact hM.fg_top.map f⟩ - -theorem _root_.LinearMap.finite_iff_of_bijective (f : M →ₛₗ[σ] P) (hf : Function.Bijective f) : - Module.Finite R M ↔ Module.Finite S P := + Module.Finite S P := by + rw [Module.finite_def, Submodule.fg_def] at hM ⊢ + obtain ⟨s, hsfin, hs⟩ := hM + refine ⟨f '' s, hsfin.image f, eq_top_iff.mpr fun p _ ↦ ?_⟩ + exact image_span_subset_span f s (by simpa [hs] using hf p) + +theorem _root_.LinearMap.finite_iff_of_bijective [RingHomSurjective σ] + (f : M →ₛₗ[σ] P) (hf : Function.Bijective f) : Module.Finite R M ↔ Module.Finite S P := ⟨fun _ ↦ of_surjective f hf.surjective, fun _ ↦ ⟨fg_of_fg_map_injective f hf.injective <| by rwa [Submodule.map_top, LinearMap.range_eq_top.mpr hf.surjective, ← Module.finite_def]⟩⟩ diff --git a/Mathlib/RingTheory/RootsOfUnity/Complex.lean b/Mathlib/RingTheory/RootsOfUnity/Complex.lean index 733daaab5a..2eeb4925fb 100644 --- a/Mathlib/RingTheory/RootsOfUnity/Complex.lean +++ b/Mathlib/RingTheory/RootsOfUnity/Complex.lean @@ -35,6 +35,13 @@ open Polynomial Real open scoped Nat Real +theorem isPrimitiveRoot_I : IsPrimitiveRoot I 4 := + .mk_of_lt I zero_lt_four I_pow_four fun l hl0 hl4 ↦ by + interval_cases l <;> norm_num [Complex.ext_iff] + +theorem isPrimitiveRoot_neg_I : IsPrimitiveRoot (-I) 4 := by + simpa only [inv_I] using isPrimitiveRoot_I.inv + theorem isPrimitiveRoot_exp_of_isCoprime (i : ℤ) (n : ℕ) (h0 : n ≠ 0) (hi : IsCoprime i n) : IsPrimitiveRoot (exp (2 * π * I * (i / n))) n := by rw [IsPrimitiveRoot.iff_def] diff --git a/Mathlib/Tactic/Determinant/Bird/Cert.lean b/Mathlib/Tactic/Determinant/Bird/Cert.lean index 4be7b7d4ab..33493a3b40 100644 --- a/Mathlib/Tactic/Determinant/Bird/Cert.lean +++ b/Mathlib/Tactic/Determinant/Bird/Cert.lean @@ -235,9 +235,11 @@ def certEntry (i j : ℕ) : CertM rα (Cert rα) := do let idx := dim * i + j let entry := arrayEntries.getD idx q(0) let ce ← certEval entry - have : $lhs =Q $entry := ⟨⟩ - let h : Q($lhs = $entry) := q(rfl) - let cert := ce.chainProof h + let getD : Q($α) := q(Array.getD $A ($dimLit * $i + $j) 0) + let hGet : Q($lhs = $getD) := q(BirdDet.get_eq $dimLit $A $i $j) + have : $getD =Q $entry := ⟨⟩ + let hGetD : Q($getD = $entry) := q(rfl) + let cert := ce.chainProof q(Eq.trans $hGet $hGetD) modify fun s => {s with entryCache := s.entryCache.insert (i, j) cert} return cert @@ -316,10 +318,12 @@ partial def certIterStepEntry (t i j : ℕ) : CertM rα (Cert rα) := do -- sumFrom n (i + 1) fun k => F_t i k * get n A k j let tailSumCert ← certTail t' i j (i + 1) let rhsCert ← certAdd diagProdCert tailSumCert + let hStep := q(BirdDet.stepEntry_eq $dimLit $A $(ctx.iterStepEntry t') $i $j) + let stepCert := rhsCert.chainProof hStep let hIter := q(Function.iterate_succ_apply' (BirdDet.stepEntry $dimLit $A) $t' (BirdDet.get $dimLit $A)) let h := q(congrArg (fun F : ℕ → ℕ → $α ↦ F $i $j) $hIter) - pure (rhsCert.chainProof h) + pure (stepCert.chainProof h) modify fun s => {s with iterStepEntryCache := s.iterStepEntryCache.insert (t, i, j) cert} return cert diff --git a/Mathlib/Tactic/NormDet.lean b/Mathlib/Tactic/NormDet.lean index de5787fcd9..f94552edc5 100644 --- a/Mathlib/Tactic/NormDet.lean +++ b/Mathlib/Tactic/NormDet.lean @@ -6,7 +6,7 @@ Authors: Paul Cadman module public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic -meta import Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness +public import Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness public meta import Mathlib.Tactic.Determinant.Bird.Cert /-! @@ -31,12 +31,16 @@ private def normalizeBirdDet (e : Expr) : MetaM Simp.Result := do private def normalizeDetFromEntries {u : Level} {α : Q(Type u)} {n : Q(ℕ)} (rα : Q(CommRing $α)) (A : Q(Matrix (Fin $n) (Fin $n) $α)) (entries : Array Q($α)) : MetaM Simp.Result := do - let arrayExpr : Q(Array $α) ← mkArrayLit α entries.toList - let hA ← mkDecideProofQ q(Array.size $arrayExpr = $n * $n) - have : $arrayExpr =Q Array.ofFn fun k : Fin ($n * $n) ↦ $A k.divNat k.modNat := ⟨⟩ - let ofArrayEqA := q(Matrix.ofArray_ofFn $A) + let xs : Q(List $α) ← mkListLit α entries.toList + let arrayExpr : Q(Array $α) := q(List.toArray $xs) + -- `List.ofFn` is exposed (unlike `Array.ofFn`) and so this reduction can be + -- checked by the kernel + have : (List.ofFn fun k : Fin ($n * $n) ↦ $A k.divNat k.modNat) =Q $xs := ⟨⟩ + let hlist : Q(List.ofFn (fun k : Fin ($n * $n) ↦ $A k.divNat k.modNat) = $xs) := q(rfl) + let hArray := q($hlist ▸ List.toArray_ofFn) let birdDet := q(BirdDet.birdDet $n $arrayExpr) - let detEqBirdDet := q($ofArrayEqA ▸ BirdDet.det_eq_birdDet $arrayExpr $hA) + let detEqBirdDet := q($hArray ▸ Matrix.ofArray_ofFn $A ▸ BirdDet.det_eq_birdDet + (Array.ofFn fun k : Fin ($n * $n) ↦ $A k.divNat k.modNat) Array.size_ofFn) let birdDetNorm ← normalizeBirdDet birdDet let detEqBirdDetRes : Simp.Result := ⟨birdDet, some detEqBirdDet, true⟩ detEqBirdDetRes.mkEqTrans birdDetNorm diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean index ed53c3f3e7..2f0b3d8ffb 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean @@ -589,13 +589,14 @@ theorem toLinearMap_mul (f g : M₁ →L[R₁] M₁) : (↑(f * g) : M₁ →ₗ instance monoidWithZero : MonoidWithZero (M₁ →L[R₁] M₁) := fast_instance% FunLike.monoidWithZero -@[simp, norm_cast] -theorem coe_pow' (f : M₁ →L[R₁] M₁) (n : ℕ) : ⇑(f ^ n) = f^[n] := - hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _ +@[deprecated (since := "2026-07-23")] alias coe_pow' := FunLike.coe_pow_eq_iterate @[simp, norm_cast] -theorem coe_pow (f : M₁ →L[R₁] M₁) (n : ℕ) : (↑(f ^ n) : M₁ →ₗ[R₁] M₁) = f ^ n := - DFunLike.ext' <| (coe_pow' f n).trans <| .symm <| hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _ +theorem toLinearMap_pow (f : M₁ →L[R₁] M₁) (n : ℕ) : (↑(f ^ n) : M₁ →ₗ[R₁] M₁) = f ^ n := + DFunLike.ext' <| (FunLike.coe_pow_eq_iterate f n).trans + <| .symm <| hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _ + +@[deprecated (since := "2026-07-24")] protected alias coe_pow := toLinearMap_pow instance instNatCast [ContinuousAdd M₁] : NatCast (M₁ →L[R₁] M₁) where natCast n := n • (1 : M₁ →L[R₁] M₁) diff --git a/Mathlib/Topology/Sheaves/Over.lean b/Mathlib/Topology/Sheaves/Over.lean index b8e74aa674..376d5ecbea 100644 --- a/Mathlib/Topology/Sheaves/Over.lean +++ b/Mathlib/Topology/Sheaves/Over.lean @@ -91,6 +91,11 @@ def overPullbackSheafEquivOver {X : TopCat} (U : Opens X) : (Opens.grothendieckTopology X).overPullback A U ⋙ U.sheafEquivOver.functor ≅ U.sheafRestrict := .refl _ +instance {X : TopCat} (U : Opens X) + [((Opens.grothendieckTopology X).overPullback A U).IsRightAdjoint] : + (U.sheafRestrict (C := A)).IsRightAdjoint := + Functor.isRightAdjoint_of_iso U.overPullbackSheafEquivOver + /-- `overPullback` and `sheafRestrict` are isomorphic under `sheafEquivOver`. -/ def sheafRestrictSheafEquivOver {X : TopCat} (U : Opens X) : U.sheafRestrict ⋙ U.sheafEquivOver.inverse ≅ diff --git a/MathlibTest/matrix.lean b/MathlibTest/matrix.lean index 59a4cd3483..c503fc6ee1 100644 --- a/MathlibTest/matrix.lean +++ b/MathlibTest/matrix.lean @@ -1,7 +1,11 @@ +module + /- manually ported from https://github.com/leanprover-community/mathlib/blob/4f4a1c875d0baa92ab5d92f3fb1bb258ad9f3e5b/test/matrix.lean -/ + +public import Lean import Mathlib.GroupTheory.Perm.Fin import Mathlib.LinearAlgebra.Matrix.Determinant.Basic import Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs @@ -9,12 +13,12 @@ import Mathlib.LinearAlgebra.Matrix.Notation import Mathlib.RingTheory.Polynomial.Basic import Mathlib.Tactic.FieldSimp import Mathlib.Tactic.NormDet -import Qq +meta import Mathlib.Data.Fin.VecNotation +meta import Mathlib.Data.Matrix.Basic +meta import Qq open Qq -variable {α β : Type} [Semiring α] [Ring β] - namespace Matrix /-! Test that the dimensions are inferred correctly, even for empty matrices -/ @@ -114,6 +118,8 @@ section delaborators end delaborators +variable {α β : Type} [Semiring α] [Ring β] + example {a a' b b' c c' d d' : α} : !![a, b; c, d] + !![a', b'; c', d'] = !![a + a', b + b'; c + c', d + d'] := by simp diff --git a/upstream_sha b/upstream_sha index a674d0877d..d1cbab04ba 100644 --- a/upstream_sha +++ b/upstream_sha @@ -1 +1 @@ -65fe2a1f85b506b0ef7df1990697be5a1ad64317 +996c094298abe6682d90e374ffc84b6419b6d2ce