diff --git a/Counterexamples/DirectSumIsInternal.lean b/Counterexamples/DirectSumIsInternal.lean index 638eaae576..2b50b5a7d2 100644 --- a/Counterexamples/DirectSumIsInternal.lean +++ b/Counterexamples/DirectSumIsInternal.lean @@ -60,8 +60,7 @@ theorem withSign.isCompl : IsCompl ℤ≥0 ℤ≤0 := by · exact Submodule.mem_sup_left (mem_withSign_one.mpr hp) · exact Submodule.mem_sup_right (mem_withSign_neg_one.mpr hn) -set_option linter.defProp false in -def withSign.independent : iSupIndep withSign := by +theorem withSign.independent : iSupIndep withSign := by apply (iSupIndep_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint intro i diff --git a/Mathlib.lean b/Mathlib.lean index 58520b10d3..808fbf72d0 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6483,6 +6483,7 @@ public import Mathlib.RingTheory.AlgebraTower public import Mathlib.RingTheory.Algebraic.Basic public import Mathlib.RingTheory.Algebraic.Cardinality public import Mathlib.RingTheory.Algebraic.Defs +public import Mathlib.RingTheory.Algebraic.Denominator public import Mathlib.RingTheory.Algebraic.Integral public import Mathlib.RingTheory.Algebraic.LinearIndependent public import Mathlib.RingTheory.Algebraic.MvPolynomial diff --git a/Mathlib/Algebra/Module/Equiv/Basic.lean b/Mathlib/Algebra/Module/Equiv/Basic.lean index 93a26c2d2e..a805a427a6 100644 --- a/Mathlib/Algebra/Module/Equiv/Basic.lean +++ b/Mathlib/Algebra/Module/Equiv/Basic.lean @@ -509,12 +509,14 @@ theorem ofLinear_symm_apply {h₁ h₂} (x : M₂) : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm x = g x := rfl -@[deprecated "Follows from simp lemmas `symm_ofLinearMap` and `ofLinear_toLinearMap`" +@[deprecated "Follows from simp lemmas `symm_ofLinearMap` and `toLinearMap_ofLinearMap`" (since := "2026-06-23")] theorem ofLinear_symm_toLinearMap {h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm = g := rfl @[simp] -theorem ofLinear_toLinearMap (h₁ h₂) : (ofLinearMap f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) = f := rfl +theorem toLinearMap_ofLinearMap (h₁ h₂) : (ofLinearMap f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) = f := rfl + +@[deprecated (since := "2026-08-04")] alias ofLinear_toLinearMap := toLinearMap_ofLinearMap end diff --git a/Mathlib/Analysis/Calculus/FDeriv/Extend.lean b/Mathlib/Analysis/Calculus/FDeriv/Extend.lean index ade989ad91..c7dc9d0400 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Extend.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Extend.lean @@ -84,7 +84,7 @@ theorem hasFDerivWithinAt_closure_of_tendsto_fderiv {f : E → F} {s : Set E} {x refine ContinuousWithinAt.closure_le uv_in ?_ ?_ key all_goals -- common start for both continuity proofs - have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by gcongr <;> exact inter_subset_right + have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by grw [inter_subset_right] obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s := by simpa [closure_prod_eq] using closure_mono this uv_in apply ContinuousWithinAt.mono _ this diff --git a/Mathlib/Analysis/Complex/HalfPlane.lean b/Mathlib/Analysis/Complex/HalfPlane.lean index 009b9704f5..3306682705 100644 --- a/Mathlib/Analysis/Complex/HalfPlane.lean +++ b/Mathlib/Analysis/Complex/HalfPlane.lean @@ -12,7 +12,7 @@ public import Mathlib.Topology.Instances.EReal.Lemmas # Half-planes in ℂ are open We state that open left, right, upper and lower half-planes in the complex numbers are open sets, -where the bounding value of the real or imaginary part is given by an `EReal` `x`. +where the bounding value of the real or imaginary part is given by a real or `EReal` `x`. So this includes the full plane and the empty set for `x = ⊤`/`x = ⊥`. -/ @@ -40,4 +40,20 @@ in the complex plane. -/ lemma isOpen_im_gt_EReal (x : EReal) : IsOpen {z : ℂ | x < z.im} := isOpen_lt continuous_const <| EReal.continuous_coe_iff.mpr continuous_im +/-- An open left half-plane is an open set in the complex plane. -/ +lemma isOpen_re_lt (x : ℝ) : IsOpen {z : ℂ | z.re < x} := by + simpa using isOpen_re_lt_EReal x + +/-- An open right half-plane is an open set in the complex plane. -/ +lemma isOpen_re_gt (x : ℝ) : IsOpen {z : ℂ | x < z.re} := by + simpa using isOpen_re_gt_EReal x + +/-- An open lower half-plane is an open set in the complex plane. -/ +lemma isOpen_im_lt (x : ℝ) : IsOpen {z : ℂ | z.im < x} := by + simpa using isOpen_im_lt_EReal x + +/-- An open upper half-plane is an open set in the complex plane. -/ +lemma isOpen_im_gt (x : ℝ) : IsOpen {z : ℂ | x < z.im} := by + simpa using isOpen_im_gt_EReal x + end Complex diff --git a/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean b/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean index 0ccb13f47c..e033d86ed2 100644 --- a/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean +++ b/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean @@ -5,12 +5,10 @@ Authors: Anatole Dedecker, Luigi Massacci -/ module -public import Mathlib.Analysis.Calculus.ContDiff.Operations -public import Mathlib.MeasureTheory.Function.LocallyIntegrable +public import Mathlib.Analysis.Calculus.ContDiff.Bounds +public import Mathlib.Analysis.InnerProductSpace.Basic public import Mathlib.MeasureTheory.Function.Holder public import Mathlib.MeasureTheory.Integral.Bochner.Set -public import Mathlib.Topology.ContinuousMap.Bounded.Normed -public import Mathlib.Topology.Sets.Compacts /-! # Continuously differentiable functions supported in a given compact set @@ -715,6 +713,45 @@ theorem norm_toBoundedContinuousFunction (f : 𝓓^{n}_{K}(E, F)) : simp [BoundedContinuousFunction.norm_eq_iSup_norm, ContDiffMapSupportedIn.seminorm_apply, structureMapCLM_apply] +/-- Define a continuous `𝕜`-linear map from `𝓓^{n₁}_{K₁}(E, F)` to `𝓓^{n₂}_{K₂}(E, F')`. -/ +protected noncomputable def mkCLM (A : 𝓓^{n₁}_{K₁}(E, F) → E → F') + (hadd : ∀ f g x, A (f + g) x = A f x + A g x) + (hsmul : ∀ (c : 𝕜) f x, A (c • f) x = c • A f x) + (hsmooth : ∀ f, ContDiff ℝ n₂ (A f)) + (hsupp : ∀ f, EqOn (A f) 0 K₂ᶜ) + (hbound : ∀ i : ℕ, i ≤ n₂ → ∃ (s : Finset ℕ) (C : ℝ), 0 ≤ C ∧ ∀ f, ∀ x ∈ K₂, + ‖iteratedFDeriv ℝ i (A f) x‖ ≤ C * (s.sup fun j ↦ N[𝕜]_{K₁, n₁, j}) f) : + 𝓓^{n₁}_{K₁}(E, F) →L[𝕜] 𝓓^{n₂}_{K₂}(E, F') := + letI Φ : 𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F') := + { toFun f := ⟨A f, hsmooth f, hsupp f⟩ + map_add' f g := ext (hadd f g) + map_smul' c f := ext (hsmul c f) } + { toLinearMap := Φ + cont := show Continuous Φ by + refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..) + (ContDiffMapSupportedIn.withSeminorms ..) _ (.of_real fun i ↦ ?_) + by_cases hi : i ≤ n₂ + · obtain ⟨s, C, hC, h⟩ := hbound i hi + exact ⟨s, C, fun f ↦ ((Φ f).seminorm_le_iff 𝕜 (mul_nonneg hC (apply_nonneg _ _)) i).2 + fun _ x hx ↦ h f x hx⟩ + · exact ⟨∅, 0, fun f ↦ by + simp [ContDiffMapSupportedIn.seminorm_eq_bot_of_gt 𝕜 (not_le.1 hi)]⟩ } + +/-- Define a continous `𝕜`-linear map fom `𝓓^{n}_{K}(E, F)` to a normed space. -/ +protected noncomputable def mkCLMtoNormedSpace {G : Type*} [NormedAddCommGroup G] + [NormedSpace 𝕜 G] (A : 𝓓^{n}_{K}(E, F) → G) + (hadd : ∀ f g, A (f + g) = A f + A g) + (hsmul : ∀ (c : 𝕜) f, A (c • f) = c • A f) + (hbound : ∃ (s : Finset ℕ) (C : ℝ), 0 ≤ C ∧ ∀ f, + ‖A f‖ ≤ C * (s.sup fun i ↦ N[𝕜]_{K, n, i}) f) : + 𝓓^{n}_{K}(E, F) →L[𝕜] G := + letI Φ : 𝓓^{n}_{K}(E, F) →ₗ[𝕜] G := ⟨⟨A, hadd⟩, hsmul⟩ + { toLinearMap := Φ + cont := show Continuous Φ by + obtain ⟨s, C, hC, h⟩ := hbound + exact continuous_normedSpace_rng G (ContDiffMapSupportedIn.withSeminorms 𝕜 E F n K) + Φ ⟨s, ⟨C, hC⟩, h⟩ } + /-- The inclusion of the space `𝓓^{n}_{K}(E, F)` into the space `E →ᵇ F` of bounded continuous functions as a continuous `𝕜`-linear map. -/ noncomputable def toBoundedContinuousFunctionCLM : 𝓓^{n}_{K}(E, F) →L[𝕜] E →ᵇ F where @@ -974,13 +1011,11 @@ lemma norm_integralAgainstBilinLM_le {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} and a function `φ : E → F₂` which is integrable on `K`, this is the *continuous* `𝕜`-linear map `f ↦ ∫ x, B (f x) (φ x) ∂μ` from `𝓓^{n}_{K}(E, F₁)` to `F₃`. Otherwise, this is the zero map. -/ noncomputable def integralAgainstBilinCLM (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) (μ : Measure E) (φ : E → F₂) : - 𝓓^{n}_{K}(E, F₁) →L[𝕜] F₃ where - toLinearMap := integralAgainstBilinLM B μ φ - cont := show Continuous (integralAgainstBilinLM B μ φ) by - refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..) - (norm_withSeminorms 𝕜 _) _ - (.of_real fun _ ↦ ⟨{0}, (∫ x in K, ‖φ x‖ ∂μ) * ‖B‖, fun f ↦ ?_⟩) - simpa using! norm_integralAgainstBilinLM_le + 𝓓^{n}_{K}(E, F₁) →L[𝕜] F₃ := + ContDiffMapSupportedIn.mkCLMtoNormedSpace 𝕜 (integralAgainstBilinLM B μ φ) + (integralAgainstBilinLM B μ φ).map_add (integralAgainstBilinLM B μ φ).map_smul + ⟨{0}, (∫ x in K, ‖φ x‖ ∂μ) * ‖B‖, by positivity, + fun f ↦ by simpa using! norm_integralAgainstBilinLM_le⟩ @[simp] lemma integralAgainstBilinCLM_apply {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : Measure E} {φ : E → F₂} @@ -1001,4 +1036,68 @@ lemma integralAgainstBilinCLM_eq_setIntegral {B : F₁ →L[𝕜] F₂ →L[𝕜 end Integral +section Multiplication + +section bilin + +open ContDiffMapSupportedIn + +variable {F₁ F₂ F₃ G : Type*} [NormedAlgebra ℝ 𝕜] + [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [NormedSpace ℝ F₁] + [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [NormedSpace ℝ F₂] + [NormedAddCommGroup F₃] [NormedSpace 𝕜 F₃] [NormedSpace ℝ F₃] + +open ContinuousLinearMap Finset + +variable {𝕜} +/-- The map `f ↦ (x ↦ B (f x) (g x))` as a continuous `𝕜`-linear map on 𝓓^{n}_{K}(E, F₁), +where `B` is a continuous `𝕜`-linear map and `g` is a C^n function. + +TODO: Introduce a type of bundled C^k functions. -/ +noncomputable def bilinLeftCLM (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {g : E → F₂} (hg : ContDiff ℝ n g) : + 𝓓^{n}_{K}(E, F₁) →L[𝕜] 𝓓^{n}_{K}(E, F₃) := + ContDiffMapSupportedIn.mkCLM 𝕜 (fun φ x ↦ B (φ x) (g x)) ?hadd ?hsmul (fun φ ↦ ?hsmooth) + (fun φ x hx ↦ ?hsupp) (fun k hk ↦ ?hbound) +where finally + case hadd | hsmul => intros; simp + case hsmooth => + exact (B.bilinearRestrictScalars ℝ).isBoundedBilinearMap.contDiff.comp (φ.contDiff.prodMk hg) + case hsupp => simp only [φ.zero_on_compl hx, Pi.zero_apply, map_zero, zero_apply] + case hbound => + have hcont : Continuous fun x ↦ (Finset.range (k + 1)).sup' Finset.nonempty_range_add_one + (fun i ↦ ‖iteratedFDeriv ℝ i g x‖) := + Continuous.finset_sup'_apply Finset.nonempty_range_add_one fun i hi ↦ + (hg.continuous_iteratedFDeriv (WithTop.coe_le_coe.2 + (le_trans (WithTop.coe_le_coe.2 (mem_range_succ_iff.mp hi)) hk))).norm + obtain ⟨C₀, hC₀⟩ := K.isCompact.exists_bound_of_continuousOn hcont.continuousOn + have hgC₀ : ∀ i ≤ k, ∀ x ∈ K, ‖iteratedFDeriv ℝ i g x‖ ≤ ‖C₀‖ := fun i hi x hx ↦ + (Finset.le_sup' _ (Finset.mem_range_succ_iff.2 hi)).trans + ((Real.le_norm_self _).trans ((hC₀ x hx).trans (Real.le_norm_self C₀))) + refine ⟨Finset.Iic k, ‖B‖ * 2 ^ k * ‖C₀‖, by positivity, fun φ x hx ↦ ?_⟩ + calc + ‖iteratedFDeriv ℝ k (fun y ↦ B (φ y) (g y)) x‖ + ≤ ‖B‖ * ∑ i ∈ Finset.range (k + 1), (k.choose i : ℝ) * ‖iteratedFDeriv ℝ i φ x‖ * + ‖iteratedFDeriv ℝ (k - i) g x‖ := by + simpa using (B.bilinearRestrictScalars ℝ).norm_iteratedFDeriv_le_of_bilinear + φ.contDiff hg x (mod_cast hk) + _ ≤ ‖B‖ * ∑ i ∈ Finset.range (k + 1), (k.choose i : ℝ) * + ((Finset.Iic k).sup fun m ↦ N[𝕜]_{K, n, m}) φ * ‖C₀‖ := by + gcongr with i hi + · exact (norm_iteratedFDeriv_apply_le_seminorm 𝕜 + ((WithTop.coe_le_coe.2 (mem_range_succ_iff.mp hi)).trans hk)).trans + (Seminorm.le_finset_sup_apply (Finset.mem_Iic.2 (mem_range_succ_iff.mp hi))) + · exact hgC₀ (k - i) (Nat.sub_le k i) x hx + _ = ‖B‖ * 2 ^ k * ‖C₀‖ * ((Finset.Iic k).sup fun m ↦ N[𝕜]_{K, n, m}) φ := by + simp_rw [← Finset.sum_mul, ← Nat.cast_sum, Nat.sum_range_choose] + push_cast + ring + +@[simp] +theorem bilinLeftCLM_apply (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {g : E → F₂} (hg : ContDiff ℝ n g) + (φ : 𝓓^{n}_{K}(E, F₁)) : bilinLeftCLM B hg φ = fun x => B (φ x) (g x) := rfl + +end bilin + +end Multiplication + end ContDiffMapSupportedIn diff --git a/Mathlib/Analysis/Normed/Algebra/Spectrum.lean b/Mathlib/Analysis/Normed/Algebra/Spectrum.lean index ce61033d88..a65c8239c4 100644 --- a/Mathlib/Analysis/Normed/Algebra/Spectrum.lean +++ b/Mathlib/Analysis/Normed/Algebra/Spectrum.lean @@ -545,8 +545,7 @@ lemma Subalgebra.frontier_subset_frontier : (spectrum.isClosed (x : A)).closure_eq] apply subset_inter (frontier_spectrum S x) rw [frontier_eq_closure_inter_closure] - exact inter_subset_right |>.trans <| - closure_mono <| compl_subset_compl.mpr <| spectrum.subset_subalgebra x + grw [inter_subset_right, spectrum.subset_subalgebra] open Set Notation @@ -568,12 +567,8 @@ lemma Subalgebra.spectrum_sUnion_connectedComponentIn : suffices h_frontier : frontier (σ 𝕜 x \ σ 𝕜 (x : A)) ⊆ frontier (σ 𝕜 (x : A)) from disjoint_of_subset_left h_frontier <| disjoint_compl_right.frontier_left (spectrum.isClosed _).isOpen_compl - rw [sdiff_eq_compl_inter] - apply (frontier_inter_subset _ _).trans - rw [frontier_compl] - apply union_subset <| inter_subset_left - refine inter_subset_inter_right _ ?_ |>.trans <| inter_subset_right - exact frontier_subset_frontier S x + grw [sdiff_eq_compl_inter, frontier_inter_subset, inter_subset_left, inter_subset_right, + frontier_compl, frontier_subset_frontier, union_self] /-- Let `S` be a closed subalgebra of a Banach algebra `A`, and let `x : S`. If `z` is in the spectrum of `x`, then the connected component of `z` in the complement of the spectrum of `↑x : A` diff --git a/Mathlib/Combinatorics/SimpleGraph/Maps.lean b/Mathlib/Combinatorics/SimpleGraph/Maps.lean index 79ab2b98e6..3768ec77d9 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Maps.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Maps.lean @@ -377,6 +377,7 @@ theorem mapDart_apply (d : G.Dart) : f.mapDart d = ⟨d.1.map f f, f.map_adj d.2 rfl /-- The graph homomorphism from a smaller graph to a bigger one. -/ +@[implicit_reducible] def ofLE (h : G₁ ≤ G₂) : G₁ →g G₂ := ⟨id, @h⟩ @[simp, norm_cast] lemma coe_ofLE (h : G₁ ≤ G₂) : ⇑(ofLE h) = id := rfl diff --git a/Mathlib/Combinatorics/SimpleGraph/Paths.lean b/Mathlib/Combinatorics/SimpleGraph/Paths.lean index 72c20270bc..3897513af0 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Paths.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Paths.lean @@ -373,7 +373,7 @@ theorem IsCycle.isPath_drop {u n} {p : G.Walk u u} (h : p.IsCycle) (hn : 0 < n) (p.drop n).IsPath := by replace h : (p.drop 1).IsPath := h.isPath_tail rw [← Nat.add_sub_of_le hn, drop_add_eq] - simp [h.drop (n - 1)] + simp [h.drop (n - 1), -drop_drop] theorem IsCycle.isPath_take {u n} {p : G.Walk u u} (h : p.IsCycle) (hn : n < p.length) : (p.take n).IsPath := by diff --git a/Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean b/Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean index 818eeb1e01..f74b63651b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean @@ -117,7 +117,7 @@ lemma dropUntil_eq_drop (p : G.Walk u v) (h : w ∈ p.support) : | @cons a _ _ _ p ih => by_cases! h' : w = a · subst h' - simp [dropUntil_first, drop_support_eq_support_drop_min] + simp [dropUntil_first] · rw [drop_cons_eq _ _ _ (by grind), support_copy, dropUntil] grind diff --git a/Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean b/Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean index bfb974927b..36bffe5606 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean @@ -86,6 +86,7 @@ theorem map_eq_nil_iff {p : G.Walk u u} : p.map f = nil ↔ p = nil := by cases @[simp] theorem length_map : (p.map f).length = p.length := by induction p <;> simp [*] +@[simp] theorem map_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : (p.append q).map f = (p.map f).append (q.map f) := by induction p <;> simp [*] @@ -129,14 +130,24 @@ variable {G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v) abbrev mapLe : G'.Walk u v := p.map (.ofLE h) -set_option backward.isDefEq.respectTransparency false in -lemma support_mapLe_eq_support : (p.mapLe h).support = p.support := by simp +theorem length_mapLe : (p.mapLe h).length = p.length := by + simp + +lemma support_mapLe_eq_support : (p.mapLe h).support = p.support := by + simp + +lemma edges_mapLe_eq_edges : (p.mapLe h).edges = p.edges := by + simp + +lemma edgeSet_mapLe_eq_edgeSet : (p.mapLe h).edgeSet = p.edgeSet := by + simp -set_option backward.isDefEq.respectTransparency false in -lemma edges_mapLe_eq_edges : (p.mapLe h).edges = p.edges := by simp +theorem reverse_mapLe : (p.mapLe h).reverse = p.reverse.mapLe h := by + simp -set_option backward.isDefEq.respectTransparency false in -lemma edgeSet_mapLe_eq_edgeSet : (p.mapLe h).edgeSet = p.edgeSet := by simp +theorem mapLe_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : + (p.append q).mapLe h = (p.mapLe h).append (q.mapLe h) := by + simp end mapLe diff --git a/Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean b/Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean index aea91e0f61..b028a0cc11 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean @@ -246,6 +246,11 @@ theorem getVert_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) (i : ℕ) : (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length) := by induction p generalizing i <;> cases i <;> simp [*] +/-- This uses `p` instead of `q` when `i = p.length` unlike the unprimed version. -/ +theorem getVert_append' (p : G.Walk u v) (q : G.Walk v w) (i : ℕ) : + (p.append q).getVert i = if i ≤ p.length then p.getVert i else q.getVert (i - p.length) := by + induction p generalizing i <;> cases i <;> simp [*] + theorem getVert_reverse {u v : V} (p : G.Walk u v) (i : ℕ) : p.reverse.getVert i = p.getVert (p.length - i) := by induction p with @@ -626,6 +631,7 @@ lemma support_take {u v} (p : G.Walk u v) (n : ℕ) : @[deprecated (since := "2026-05-20")] alias take_support_eq_support_take_succ := support_take +@[simp] lemma take_take (p : G.Walk u v) (n m : ℕ) : (p.take n).take m = (p.take (min n m)).copy rfl (p.take_getVert n m).symm := by apply ext_support @@ -667,6 +673,14 @@ lemma penultimate_reverse (p : G.Walk u v) : p.reverse.penultimate = p.snd := by /-- The walk obtained by removing the first dart of a walk. A nil walk stays nil. -/ def tail (p : G.Walk u v) : G.Walk (p.snd) v := p.drop 1 +@[simp] +theorem darts_tail {p : G.Walk u v} : p.tail.darts = p.darts.tail := by + simp [tail, darts_drop] + +@[simp] +theorem edges_tail {p : G.Walk u v} : p.tail.edges = p.edges.tail := by + simp [tail, edges_drop] + @[simp] lemma drop_zero {u v} (p : G.Walk u v) : p.drop 0 = p.copy (getVert_zero p).symm rfl := by @@ -676,10 +690,17 @@ lemma nil_drop_of_length_le {u v n} {p : G.Walk u v} (h : p.length ≤ n) : (p.drop n).Nil := by rw [← length_eq_zero_iff, drop_length, Nat.sub_eq_zero_of_le h] +@[simp] lemma drop_support_eq_support_drop_min {u v} (p : G.Walk u v) (n : ℕ) : (p.drop n).support = p.support.drop (n ⊓ p.length) := by induction p generalizing n <;> cases n <;> simp [*, drop] +@[simp] +theorem drop_drop (p : G.Walk u v) (n m : ℕ) : + (p.drop n).drop m = (p.drop (n + m)).copy (drop_getVert ..).symm rfl := by + apply ext_support + grind [support_copy, drop_support_eq_support_drop_min, drop_length, List.drop_drop] + @[simp] theorem append_take_drop_eq (p : G.Walk u v) (n : ℕ) : (p.take n).append (p.drop n) = p := by apply ext_support @@ -718,6 +739,14 @@ lemma dropLast_cons_of_not_nil (h : G.Adj u v) (p : G.Walk v w) (hp : ¬ p.Nil) (cons h p).dropLast = cons h (p.dropLast.copy rfl (penultimate_cons_of_not_nil _ _ hp).symm) := p.notNilRec (by simp) hp h +@[simp] +theorem darts_dropLast {p : G.Walk u v} : p.dropLast.darts = p.darts.dropLast := by + simp [dropLast, darts_take, List.dropLast_eq_take] + +@[simp] +theorem edges_dropLast {p : G.Walk u v} : p.dropLast.edges = p.edges.dropLast := by + simp [dropLast, edges_take, List.dropLast_eq_take] + @[simp] lemma dropLast_concat {t u v} (p : G.Walk u v) (h : G.Adj v t) : (p.concat h).dropLast = p.copy rfl (by simp) := by @@ -741,9 +770,13 @@ lemma concat_dropLast {p : G.Walk u v} (hp : G.Adj p.penultimate v) : p.dropLast | nil => rfl | _ => simp [hind] -@[simp] lemma cons_support_tail {p : G.Walk u v} (hp : ¬p.Nil) : - u :: p.tail.support = p.support := by - rw [← support_cons (p.adj_snd hp), cons_tail_eq _ hp] +@[simp] +lemma support_tail_of_not_nil (p : G.Walk u v) (hp : ¬ p.Nil) : + p.tail.support = p.support.tail := by + simp [← p.cons_tail_eq hp] + +lemma cons_support_tail {p : G.Walk u v} (hp : ¬p.Nil) : u :: p.tail.support = p.support := by + simp [hp] theorem support_dropLast_concat {p : G.Walk u v} (hp : ¬p.Nil) : p.dropLast.support ++ [v] = p.support := by @@ -754,7 +787,11 @@ theorem support_dropLast {p : G.Walk u v} (hp : ¬p.Nil) : p.dropLast.support = p.support.dropLast := by simp [← support_dropLast_concat hp] -@[simp] lemma length_tail_add_one {p : G.Walk u v} (hp : ¬ p.Nil) : +@[simp] +theorem length_tail (p : G.Walk u v) : p.tail.length = p.length - 1 := by + cases p <;> simp + +lemma length_tail_add_one {p : G.Walk u v} (hp : ¬ p.Nil) : p.tail.length + 1 = p.length := by rw [← length_cons (p.adj_snd hp), cons_tail_eq _ hp] @@ -766,6 +803,29 @@ lemma length_dropLast_add_one {p : G.Walk u v} (hp : ¬p.Nil) : lemma length_dropLast (p : G.Walk u v) : p.dropLast.length = p.length - 1 := by cases p <;> simp [← length_dropLast_add_one not_nil_cons] +theorem getVert_dropLast {n} {p : G.Walk u v} (h : n < p.length) : + p.dropLast.getVert n = p.getVert n := by + grind [getVert_eq_support_getElem, length_dropLast, support_dropLast] + +@[simp] +theorem reverse_tail (p : G.Walk u v) : + p.tail.reverse = p.reverse.dropLast.copy rfl p.penultimate_reverse := by + match p with + | nil => simp + | cons hadj p => + apply ext_support + rw [support_copy] + simp [-reverse_cons] + +@[simp] +theorem reverse_dropLast (p : G.Walk u v) : + p.dropLast.reverse = p.reverse.tail.copy p.snd_reverse rfl := by + match p with + | nil => simp + | cons hadj p => + apply ext_support + simp [-reverse_cons, List.dropLast_cons_of_ne_nil p.support_ne_nil] + protected lemma Nil.tail {p : G.Walk v w} (hp : p.Nil) : p.tail.Nil := by cases p <;> simp at hp ⊢ @@ -786,10 +846,6 @@ lemma drop_of_length_le {u v n} {p : G.Walk u v} (h : p.length ≤ n) : p.drop n = nil.copy rfl (p.getVert_of_length_le h) := (nil_drop_of_length_le h).eq_copy_nil -lemma support_tail_of_not_nil (p : G.Walk u v) (hp : ¬ p.Nil) : - p.tail.support = p.support.tail := by - rw [← cons_support_tail hp, List.tail_cons] - @[simp] lemma getVert_copy {u v w x : V} (p : G.Walk u v) (i : ℕ) (h : u = w) (h' : v = x) : (p.copy h h').getVert i = p.getVert i := by subst_vars diff --git a/Mathlib/Data/ENNReal/Basic.lean b/Mathlib/Data/ENNReal/Basic.lean index 218392836d..1a0a1261a3 100644 --- a/Mathlib/Data/ENNReal/Basic.lean +++ b/Mathlib/Data/ENNReal/Basic.lean @@ -369,17 +369,13 @@ theorem toReal_ofReal_eq_iff {a : ℝ} : (ENNReal.ofReal a).toReal = a ↔ 0 ≤ @[simp] theorem zero_lt_top : 0 < ∞ := coe_lt_top -@[simp, norm_cast] theorem coe_le_coe : (↑r : ℝ≥0∞) ≤ ↑q ↔ r ≤ q := WithTop.coe_le_coe +@[simp, norm_cast, gcongr] theorem coe_le_coe : (↑r : ℝ≥0∞) ≤ ↑q ↔ r ≤ q := WithTop.coe_le_coe -@[simp, norm_cast] theorem coe_lt_coe : (↑r : ℝ≥0∞) < ↑q ↔ r < q := WithTop.coe_lt_coe +@[simp, norm_cast, gcongr] theorem coe_lt_coe : (↑r : ℝ≥0∞) < ↑q ↔ r < q := WithTop.coe_lt_coe --- Needed until `@[gcongr]` accepts iff statements -alias ⟨_, coe_le_coe_of_le⟩ := coe_le_coe -attribute [gcongr] ENNReal.coe_le_coe_of_le +@[deprecated (since := "2026-08-04")] alias ⟨_, coe_le_coe_of_le⟩ := coe_le_coe --- Needed until `@[gcongr]` accepts iff statements -alias ⟨_, coe_lt_coe_of_lt⟩ := coe_lt_coe -attribute [gcongr] ENNReal.coe_lt_coe_of_lt +@[deprecated (since := "2026-08-04")] alias ⟨_, coe_lt_coe_of_lt⟩ := coe_lt_coe theorem coe_mono : Monotone ofNNReal := fun _ _ => coe_le_coe.2 diff --git a/Mathlib/Data/List/ModifyLast.lean b/Mathlib/Data/List/ModifyLast.lean index b19f1307d2..ca3533feac 100644 --- a/Mathlib/Data/List/ModifyLast.lean +++ b/Mathlib/Data/List/ModifyLast.lean @@ -6,9 +6,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M module public import Batteries.Data.List.Basic -public import Batteries.Tactic.Alias public import Mathlib.Init -import all Init.Data.Array.Basic /-! ### List.modifyLast -/ @@ -22,7 +20,7 @@ private theorem modifyLast.go_concat (f : α → α) (a : α) (tl : List α) (r modifyLast.go f (tl ++ [a]) r = (r.toListAppend <| modifyLast.go f (tl ++ [a]) #[]) := by cases tl with | nil => - simp only [nil_append, modifyLast.go]; rfl + simp only [nil_append, modifyLast.go]; simp | cons hd tl => simp only [cons_append] rw [modifyLast.go, modifyLast.go] @@ -50,7 +48,9 @@ theorem modifyLast_append_of_right_ne_nil (f : α → α) (l₁ l₂ : List α) | nil => contradiction | cons hd tl => cases tl with - | nil => exact modifyLast_concat _ hd _ + | nil => + simp only [modifyLast, modifyLast.go, Array.toListAppend_eq, nil_append] + exact modifyLast_concat _ hd _ | cons hd' tl' => rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append, modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _, diff --git a/Mathlib/Data/List/Sort.lean b/Mathlib/Data/List/Sort.lean index 1ad915e253..a7c527dfe7 100644 --- a/Mathlib/Data/List/Sort.lean +++ b/Mathlib/Data/List/Sort.lean @@ -10,7 +10,6 @@ public import Batteries.Data.List.Perm public import Mathlib.Data.List.OfFn public import Mathlib.Data.List.Nodup public import Mathlib.Order.Fin.Basic -import all Init.Data.List.Sort.Basic -- for exposing `mergeSort` /-! # Sorting algorithms on lists @@ -289,9 +288,9 @@ which rather than using explicit hypotheses for transitivity and totality, use Mathlib order typeclasses instead. -/ -example : - mergeSort [5, 27, 221, 95, 17, 43, 7, 2, 98, 567, 23, 12] (fun m n => m / 10 ≤ n / 10) = - [5, 7, 2, 17, 12, 27, 23, 43, 95, 98, 221, 567] := by simp [mergeSort] +set_option linter.hashCommand false in +#guard mergeSort [5, 27, 221, 95, 17, 43, 7, 2, 98, 567, 23, 12] (fun m n => m / 10 ≤ n / 10) = + [5, 7, 2, 17, 12, 27, 23, 43, 95, 98, 221, 567] section MergeSort diff --git a/Mathlib/Data/Set/NAry.lean b/Mathlib/Data/Set/NAry.lean index 0dc5b5f0fd..6cac5450f6 100644 --- a/Mathlib/Data/Set/NAry.lean +++ b/Mathlib/Data/Set/NAry.lean @@ -316,21 +316,16 @@ lemma image2_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b = theorem image2_inter_union_subset_union : image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t' := by rw [image2_union_right] - exact - union_subset_union (image2_subset_right inter_subset_left) - (image2_subset_right inter_subset_right) + nth_grw 1 [inter_subset_left, inter_subset_right] theorem image2_union_inter_subset_union : image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t' := by rw [image2_union_left] - exact - union_subset_union (image2_subset_left inter_subset_left) - (image2_subset_left inter_subset_right) + nth_grw 1 [inter_subset_left, inter_subset_right] theorem image2_inter_union_subset {f : α → α → β} {s t : Set α} (hf : ∀ a b, f a b = f b a) : image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t := by - rw [inter_comm] - exact image2_inter_union_subset_union.trans (union_subset (image2_comm hf).subset Subset.rfl) + grw [inter_comm, image2_inter_union_subset_union, image2_comm hf, union_self] theorem image2_union_inter_subset {f : α → α → β} {s t : Set α} (hf : ∀ a b, f a b = f b a) : image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t := by diff --git a/Mathlib/Dynamics/OmegaLimit.lean b/Mathlib/Dynamics/OmegaLimit.lean index 870d7fcb88..3867037115 100644 --- a/Mathlib/Dynamics/OmegaLimit.lean +++ b/Mathlib/Dynamics/OmegaLimit.lean @@ -291,9 +291,7 @@ theorem nonempty_omegaLimit_of_isCompact_absorbing [NeBot f] {c : Set β} (hc₁ exact hn.mono subset_closure · intro apply hc₁.of_isClosed_subset isClosed_closure - calc - _ ⊆ closure (image2 ϕ v s) := closure_mono (image2_subset inter_subset_right Subset.rfl) - _ ⊆ c := hv₂ + grw [inter_subset_right, hv₂] · exact fun _ ↦ isClosed_closure theorem nonempty_omegaLimit [CompactSpace β] [NeBot f] (hs : s.Nonempty) : (ω f ϕ s).Nonempty := diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean index 54b6df4337..a67a10b439 100644 --- a/Mathlib/Geometry/Manifold/ChartedSpace.lean +++ b/Mathlib/Geometry/Manifold/ChartedSpace.lean @@ -276,8 +276,9 @@ theorem ChartedSpace.locallyPathConnectedSpace [LocallyPathConnectedSpace H] : apply e.symm.image_mem_nhds (by simp [e]) exact pathComponentIn_mem_nhds <| e.image_mem_nhds (mem_chart_source _ _) ht · refine (isPathConnected_pathComponentIn <| mem_image_of_mem e (mem_of_mem_nhds ht)).image' ?_ - refine e.continuousOn_symm.mono <| subset_trans ?_ e.image_source_subset - exact (pathComponentIn_mono <| image_mono inter_subset_right).trans pathComponentIn_subset + refine e.continuousOn_symm.mono ?_ + unfold t + grw [pathComponentIn_subset, inter_subset_right, e.image_source_subset] · exact (image_mono pathComponentIn_subset).trans (PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).subset diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean index f22688a597..4d153c2f02 100644 --- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean +++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean @@ -689,7 +689,7 @@ theorem eLpNorm_one_smul_measure {f : α → ε} (c : ℝ≥0∞) : theorem eLpNorm_le_of_measure_le_smul {c : ℝ≥0∞} {μ μ' : Measure α} (h : μ' ≤ c • μ) {f : α → ε} {p : ℝ≥0∞} : eLpNorm f p μ' ≤ c ^ (1 / p).toReal • eLpNorm f p μ := by - grw [eLpNorm_mono_measure f h, eLpNorm_smul_measure_le] + grw [h, eLpNorm_smul_measure_le] theorem MemLp.of_measure_le_smul {μ' : Measure α} {c : ℝ≥0∞} (hc : c ≠ ∞) (hμ'_le : μ' ≤ c • μ) {f : α → ε} (hf : MemLp f p μ) : MemLp f p μ' := by @@ -708,12 +708,12 @@ theorem eLpNorm_one_add_measure (f : α → ε) (μ ν : Measure α) : rw [lintegral_add_measure _ μ ν] theorem eLpNorm_le_add_measure_right (f : α → ε) (μ ν : Measure α) {p : ℝ≥0∞} : - eLpNorm f p μ ≤ eLpNorm f p (μ + ν) := - eLpNorm_mono_measure f <| Measure.le_add_right <| le_refl _ + eLpNorm f p μ ≤ eLpNorm f p (μ + ν) := by + grw [← Measure.le_add_right le_rfl] theorem eLpNorm_le_add_measure_left (f : α → ε) (μ ν : Measure α) {p : ℝ≥0∞} : - eLpNorm f p ν ≤ eLpNorm f p (μ + ν) := - eLpNorm_mono_measure f <| Measure.le_add_left <| le_refl _ + eLpNorm f p ν ≤ eLpNorm f p (μ + ν) := by + grw [← Measure.le_add_left le_rfl] variable {ε : Type*} [ENorm ε] in lemma eLpNormEssSup_eq_iSup (hμ : ∀ a, μ {a} ≠ 0) (f : α → ε) : eLpNormEssSup f μ = ⨆ a, ‖f a‖ₑ := diff --git a/Mathlib/MeasureTheory/Measure/Stieltjes.lean b/Mathlib/MeasureTheory/Measure/Stieltjes.lean index abbd8b02fc..98fb38f686 100644 --- a/Mathlib/MeasureTheory/Measure/Stieltjes.lean +++ b/Mathlib/MeasureTheory/Measure/Stieltjes.lean @@ -131,6 +131,7 @@ initialize_simps_projections StieltjesFunction (toFun → apply) variable (f : StieltjesFunction R) +@[gcongr] theorem mono : Monotone f := f.mono' @@ -296,13 +297,14 @@ theorem length_Ioc (a b : R) : f.length (Ioc a b) = ofReal (f b - f a) := by apply zero_le simp only [Ioc_sdiff_botSet] at h obtain ⟨h₁, h₂⟩ := (Ioc_subset_Ioc_iff ab).1 h - exact Real.toNNReal_le_toNNReal (sub_le_sub (f.mono h₁) (f.mono h₂)) + grw [h₁, h₂] +@[gcongr] theorem length_mono {s₁ s₂ : Set R} (h : s₁ ⊆ s₂) : f.length s₁ ≤ f.length s₂ := by rcases isEmpty_or_nonempty R with hR | hR · simp [length_eq_of_isEmpty] simp only [length_eq] - exact iInf_mono fun a => biInf_mono fun b h' => (sdiff_subset_sdiff_left h).trans h' + exact iInf_mono fun a => biInf_mono fun b => by gcongr theorem length_sdiff_botSet {s : Set R} : f.length (s \ botSet) = f.length s := by rcases isEmpty_or_nonempty R with hR | hR @@ -355,9 +357,8 @@ theorem length_subadditive_Icc_Ioo {a b : R} {c d : ℕ → R} (ss : Icc a b ⊆ rw [Finset.sum_insert (Finset.notMem_erase _ _)] replace bcd : b ∈ Ioc (c i) (d i) := Iotop_subset_Ioc bcd grw [← IH _ (Finset.erase_ssubset is) (c i), ← ENNReal.ofReal_add_le] - · gcongr - rw [sub_add_sub_cancel] - exact sub_le_sub_right (f.mono bcd.2) _ + · rw [sub_add_sub_cancel] + grw [bcd.2] · rintro x ⟨h₁, h₂⟩ apply (cv ⟨h₁, le_trans h₂ (le_of_lt bcd.1)⟩).resolve_left (fun h ↦ ?_) order [(Iotop_subset_Ioc h).1] @@ -450,10 +451,7 @@ theorem measurableSet_Ioi {c : R} : MeasurableSet[f.outer.caratheodory] (Ioi c) simp only [← length_eq] rw [← length_sdiff_botSet, inter_sdiff_right_comm, ← length_sdiff_botSet (s := t \ Ioi c), sdiff_sdiff_comm] - refine - le_trans - (add_le_add (f.length_mono <| inter_subset_inter_left _ h) - (f.length_mono <| sdiff_subset_sdiff_left h)) ?_ + grw [h] rcases le_total a c with hac | hac <;> rcases le_total b c with hbc | hbc · simp only [Ioc_inter_Ioi, f.length_Ioc, hac, hbc, le_refl, Ioc_eq_empty, max_eq_right, min_eq_left, Ioc_sdiff_Ioi, f.length_empty, zero_add, not_lt] diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean index b52330580a..e6ec621e48 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean +++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean @@ -211,7 +211,8 @@ lemma variation_transpose_eq_smul [Nontrivial E] {C : ℝ≥0} simp only [flip_apply, hB] at this rw [mul_right_comm, mul_le_mul_iff_left₀ (by simpa), ← le_div_iff₀' (by positivity), div_eq_inv_mul] at this - exact ENNReal.coe_le_coe_of_le this + change ENNReal.ofNNReal _ ≤ ENNReal.ofNNReal _ + gcongr grw [this, enorm_measure_le_variation, Measure.smul_apply] lemma variation_transpose_eq [Nontrivial E] (hB : ∀ x y, ‖B x y‖₊ = ‖x‖₊ * ‖y‖₊) : diff --git a/Mathlib/RingTheory/Algebraic/Denominator.lean b/Mathlib/RingTheory/Algebraic/Denominator.lean new file mode 100644 index 0000000000..b044cd9d04 --- /dev/null +++ b/Mathlib/RingTheory/Algebraic/Denominator.lean @@ -0,0 +1,100 @@ +/- +Copyright (c) 2026 Michail Karatarakis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michail Karatarakis +-/ +module + +public import Mathlib.RingTheory.Algebraic.Integral +public import Mathlib.RingTheory.Ideal.Colon + +/-! +# Denominators of elements of an algebra + +For an element `x` of an `R`-algebra `S`, with `R` a principal ideal ring, the **denominator** +`Algebra.denominator R x` is a generator of the colon ideal `(integralClosure R S).colon {x}`, +that is, of the ideal of scalars `r : R` clearing the denominators of `x`, in the sense that +`r • x` is integral over `R`. When `R = ℤ`, its absolute value is the natural-number denominator +`Algebra.natDenominator x`. + +The definition needs no hypothesis on `x`, but it is only meaningful for `x` algebraic over `R`: +`IsAlgebraic.denominator_ne_zero` shows the denominator is then nonzero, whereas no nonzero +multiple of a transcendental element is integral, so that the colon ideal is trivial and the +denominator is `0`. See the `example` below, taking `x` to be the variable in `ℤ[X]`. + +## Main definitions + +* `Algebra.denominator`: the denominator of an element, over a principal ideal ring +* `Algebra.natDenominator`: the natural-number denominator of an element, over `ℤ` + +## Main results + +* `Algebra.denominator_dvd_iff`: `denominator R x` divides exactly the `r : R` with `r • x` + integral over `R` +* `IsAlgebraic.denominator_ne_zero`: the denominator of an algebraic element is nonzero +-/ + +public section + +variable (R : Type*) {S : Type*} [CommRing R] +variable [IsPrincipalIdealRing R] [CommRing S] [Algebra R S] +namespace Algebra + +/-- The denominator of an element `x` of an `R`-algebra: a generator of the ideal of scalars +`r : R` such that `r • x` is integral over `R`. It is nonzero as soon as `x` is algebraic over +`R`; see `IsAlgebraic.denominator_ne_zero`. -/ +noncomputable def denominator (x : S) : R := + Submodule.IsPrincipal.generator ((integralClosure R S).toSubmodule.colon {x}) + +lemma denominator_def (x : S) : + denominator R x = + Submodule.IsPrincipal.generator ((integralClosure R S).toSubmodule.colon {x}) := by + rfl + +variable {R} + +theorem denominator_dvd_iff {r : R} {x : S} : + denominator R x ∣ r ↔ IsIntegral R (r • x) := by + rw [denominator_def, ← Submodule.IsPrincipal.mem_iff_generator_dvd, + Submodule.mem_colon_singleton, Subalgebra.mem_toSubmodule, mem_integralClosure_iff] + +theorem isIntegral_denominator_smul (x : S) : IsIntegral R (denominator R x • x) := + denominator_dvd_iff.mp dvd_rfl + +/-- The natural-number denominator of an element `x` of a ring: it is the absolute value of the +denominator of `x` over `ℤ`. -/ +noncomputable def natDenominator (x : S) : ℕ := + (denominator ℤ x).natAbs + +theorem natDenominator_def (x : S) : natDenominator x = (denominator ℤ x).natAbs := by + rfl + +theorem natDenominator_dvd_iff {n : ℕ} {x : S} : + natDenominator x ∣ n ↔ IsIntegral ℤ (n • x) := by + rw [natDenominator_def, ← Int.ofNat_dvd_right, denominator_dvd_iff, natCast_zsmul] + +theorem isIntegral_natDenominator_smul (x : S) : IsIntegral ℤ (natDenominator x • x) := + natDenominator_dvd_iff.mp dvd_rfl + +end Algebra + +namespace IsAlgebraic + +theorem denominator_ne_zero {x : S} (hx : IsAlgebraic R x) : Algebra.denominator R x ≠ 0 := by + obtain ⟨r, hr0, hr⟩ := hx.exists_integral_multiple + exact ne_zero_of_dvd_ne_zero hr0 (Algebra.denominator_dvd_iff.mpr hr) + +theorem natDenominator_ne_zero {x : S} (hx : IsAlgebraic ℤ x) : Algebra.natDenominator x ≠ 0 := by + rw [Algebra.natDenominator_def, Int.natAbs_ne_zero] + exact hx.denominator_ne_zero + +end IsAlgebraic + +/- The algebraicity hypothesis in `IsAlgebraic.denominator_ne_zero` cannot be dropped: the +variable `X` of `ℤ[X]` is transcendental over `ℤ`, so no nonzero multiple of it is integral and +its denominator vanishes. -/ +example : Algebra.denominator ℤ (Polynomial.X : Polynomial ℤ) = 0 := by + by_contra h + exact Polynomial.transcendental_X ℤ + ((Algebra.isIntegral_denominator_smul _).isAlgebraic.of_smul + (mem_nonZeroDivisors_of_ne_zero h)) diff --git a/Mathlib/RingTheory/Coalgebra/Equiv.lean b/Mathlib/RingTheory/Coalgebra/Equiv.lean index 660c33828b..c8e5ddacfb 100644 --- a/Mathlib/RingTheory/Coalgebra/Equiv.lean +++ b/Mathlib/RingTheory/Coalgebra/Equiv.lean @@ -174,7 +174,7 @@ def symm (e : A ≃ₗc[R] B) : B ≃ₗc[R] A := = comul ∘ₗ (e : A ≃ₗ[R] B).symm rw [LinearEquiv.toLinearMap_symm_comp_eq] simp only [TensorProduct.congr, toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, - LinearEquiv.ofLinear_toLinearMap, ← LinearMap.comp_assoc, CoalgHomClass.map_comp_comul] + LinearEquiv.toLinearMap_ofLinearMap, ← LinearMap.comp_assoc, CoalgHomClass.map_comp_comul] rw [← toLinearEquiv_toLinearMap, LinearEquiv.comp_symm_cancel_right] } /-- See Note [custom simps projection] -/ diff --git a/Mathlib/RingTheory/IsGaloisGroup/Basic.lean b/Mathlib/RingTheory/IsGaloisGroup/Basic.lean index 8dd8974d9f..97c8d4a5c2 100644 --- a/Mathlib/RingTheory/IsGaloisGroup/Basic.lean +++ b/Mathlib/RingTheory/IsGaloisGroup/Basic.lean @@ -232,10 +232,8 @@ instance isScalarTower_mulSemiringActionQuotient [MulSemiringAction G B] [SMulDi ⟨fun g q b ↦ Quotient.inductionOn' q fun h ↦ by simp [mul_smul, mulSemiringActionQuotient_smul_def]⟩ -set_option linter.defProp false in /-- If `G` acts on `C` commuting with `A`, then the action of `G ⧸ N` on `B` commutes with `A`. -/ -@[implicit_reducible] -def smulCommClassQuotient [N.Normal] [Algebra A B] [IsScalarTower A B C] [SMulCommClass G A C] +theorem smulCommClassQuotient [N.Normal] [Algebra A B] [IsScalarTower A B C] [SMulCommClass G A C] [MulSemiringAction G B] [MulAction (G ⧸ N) B] [SMulDistribClass G B C] [IsScalarTower G (G ⧸ N) B] : SMulCommClass (G ⧸ N) A B := diff --git a/Mathlib/Topology/Algebra/GroupCompletion.lean b/Mathlib/Topology/Algebra/GroupCompletion.lean index 82cc3cda79..0ead91986c 100644 --- a/Mathlib/Topology/Algebra/GroupCompletion.lean +++ b/Mathlib/Topology/Algebra/GroupCompletion.lean @@ -228,7 +228,7 @@ theorem AddMonoidHom.extension_coe [CompleteSpace β] [T0Space β] (f : α →+ (hf : Continuous f) (a : α) : f.extension hf a = f a := UniformSpace.Completion.extension_coe (uniformContinuous_addMonoidHom_of_continuous hf) a -@[continuity] +@[continuity, fun_prop] theorem AddMonoidHom.continuous_extension [CompleteSpace β] [T0Space β] (f : α →+ β) (hf : Continuous f) : Continuous (f.extension hf) := UniformSpace.Completion.continuous_extension diff --git a/Mathlib/Topology/Algebra/LinearMapCompletion.lean b/Mathlib/Topology/Algebra/LinearMapCompletion.lean index fd01363aa3..87254b8eee 100644 --- a/Mathlib/Topology/Algebra/LinearMapCompletion.lean +++ b/Mathlib/Topology/Algebra/LinearMapCompletion.lean @@ -17,7 +17,9 @@ lifted to a continuous semilinear map between the completions of those modules. ## Main declarations: * `ContinuousLinearMap.completion`: promotes a continuous semilinear map - from `G` to `H` to a continuous semilinear map from `Completion G` to `Completion H`. + from `α` to `β` to a continuous semilinear map from `Completion α` to `Completion β`. +* `ContinuousLinearMap.fromCompletion`: promotes a continuous semilinear map + from `α` to `β` to a continuous semilinear map from `Completion α` to `β`. -/ @[expose] public section @@ -31,6 +33,8 @@ variable {α β : Type*} {R₁ R₂ : Type*} [UniformSpace α] [AddCommGroup α] [AddCommGroup β] [IsUniformAddGroup β] [Module R₂ β] [UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂} +section completion + set_option backward.isDefEq.respectTransparency false in /-- Lift a continuous semilinear map to a continuous semilinear map between the @@ -57,4 +61,36 @@ lemma coe_completion (f : α →SL[σ] β) : theorem completion_apply_coe (f : α →SL[σ] β) (a : α) : f.completion a = f a := by simp [coe_completion, map_coe] +end completion + +section fromCompletion + +variable [T0Space β] [CompleteSpace β] + +/-- Extension of a linear function to a linear function over the completion. This is the continuous +linear version of `UniformSpace.Completion.extension`. -/ +noncomputable def fromCompletion (f : α →SL[σ] β) : + Completion α →SL[σ] β where + __ := f.toAddMonoidHom.extension f.continuous + map_smul' c a := induction_on a + (isClosed_eq (continuous_extension.comp (continuous_const_smul c)) (by dsimp; fun_prop)) <| by + simp [← Completion.coe_smul, AddMonoidHom.extension_coe f.toAddMonoidHom f.continuous] + +@[simp] +lemma toAddMonoidHom_fromCompletion (f : α →SL[σ] β) : + f.fromCompletion.toAddMonoidHom = f.toAddMonoidHom.extension f.continuous := rfl + +lemma coe_fromCompletion (f : α →SL[σ] β) : + f.fromCompletion = Completion.extension f := rfl + +@[simp] +lemma fromCompletion_apply_coe (f : α →SL[σ] β) (e : α) : + f.fromCompletion e = f e := by simp [coe_fromCompletion, extension_coe] + +lemma fromCompletion_unique (f : α →SL[σ] β) (g : Completion α →SL[σ] β) + (h : ∀ (e : α), f e = g e) : f.fromCompletion = g := by + ext; simp [coe_fromCompletion, extension_unique f.uniformContinuous g.uniformContinuous h] + +end fromCompletion + end ContinuousLinearMap diff --git a/Mathlib/Topology/MetricSpace/Bounded.lean b/Mathlib/Topology/MetricSpace/Bounded.lean index b8c98c6936..21b9c3843d 100644 --- a/Mathlib/Topology/MetricSpace/Bounded.lean +++ b/Mathlib/Topology/MetricSpace/Bounded.lean @@ -9,7 +9,7 @@ public import Mathlib.Topology.Order.Bornology public import Mathlib.Topology.Order.Compact public import Mathlib.Topology.MetricSpace.ProperSpace public import Mathlib.Topology.MetricSpace.Cauchy -public import Mathlib.Topology.MetricSpace.Defs +public import Mathlib.Topology.MetricSpace.Basic public import Mathlib.Topology.EMetricSpace.Diam /-! @@ -329,11 +329,10 @@ theorem _root_.Bornology.IsBounded.isCompact_closure [ProperSpace α] (h : IsBou IsCompact (closure s) := isCompact_of_isClosed_isBounded isClosed_closure h.closure --- TODO: assume `[MetricSpace α]` instead of `[PseudoMetricSpace α] [T2Space α]` /-- The **Heine–Borel theorem**: -In a proper Hausdorff space, a set is compact if and only if it is closed and bounded. -/ +In a proper metric space, a set is compact if and only if it is closed and bounded. -/ @[wikidata Q253214] -theorem isCompact_iff_isClosed_bounded [T2Space α] [ProperSpace α] : +theorem isCompact_iff_isClosed_bounded {α : Type*} {s : Set α} [MetricSpace α] [ProperSpace α] : IsCompact s ↔ IsClosed s ∧ IsBounded s := ⟨fun h => ⟨h.isClosed, h.isBounded⟩, fun h => isCompact_of_isClosed_isBounded h.1 h.2⟩ diff --git a/upstream_sha b/upstream_sha index 45cc2a9c8e..60f4ea8900 100644 --- a/upstream_sha +++ b/upstream_sha @@ -1 +1 @@ -9fb10993c11c9e7abfa291e86fb499b6e1f4da82 +060b244276aa46de92c8a706b5236b3f8349657a