From 4b28fd7c07daa4ca1a4af2c1807bd586b0111d3d Mon Sep 17 00:00:00 2001 From: sgouezel Date: Tue, 24 Sep 2024 06:06:02 +0000 Subject: [PATCH] feat: define `HasSummableGeomSeries` to unify results between normed field and complete normed algebras (#17002) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Currently, several analogous results are proved separately in complete normed algebras, and in normed fields. For instance, the fact that inversion is differentiable is called `differentiableAt_inv'` in the former, and `differentiableAt_inv` in the latter, with similar proofs relying on the convergence of geometric series, due to completeness in the former and to the existence of the inverse in the latter. We unify these results by defining a typeclass `HasSummableGeomSeries` saying that `βˆ‘ x ^ n` converges for all `x` with norm `< 1`. We show that this is satisfied both in complete normed rings and in normed fields. And we show that many results follow solely from this assumption, deduplicating statements and proofs. Along the way, we show that inversion is analytic on rings with summable geometric series, and deduce in particular that it is strictly differentiable, clearing an existing TODO. This adds a few imports (importing analytic functions in files where they were not needed before), but with the upcoming refactor of smooth functions, analytic functions will in any case need to be imported earlier on, so this doesn't look like a real issue to me. --- Mathlib/Analysis/Analytic/Constructions.lean | 102 ++++-- Mathlib/Analysis/Calculus/Deriv/Inv.lean | 35 +-- Mathlib/Analysis/Calculus/DiffContOnCl.lean | 3 +- Mathlib/Analysis/Calculus/Dslope.lean | 4 +- .../Analysis/Calculus/FDeriv/Analytic.lean | 6 + Mathlib/Analysis/Calculus/FDeriv/Mul.lean | 75 +++-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean | 4 +- Mathlib/Analysis/Normed/Ring/Units.lean | 59 ++-- .../NormedSpace/Multilinear/Basic.lean | 6 + Mathlib/Analysis/SpecificLimits/Normed.lean | 291 +++++++++++------- .../NumberTheory/LSeries/AbstractFuncEq.lean | 2 +- Mathlib/Tactic/FunProp/Differentiable.lean | 3 - 12 files changed, 357 insertions(+), 233 deletions(-) diff --git a/Mathlib/Analysis/Analytic/Constructions.lean b/Mathlib/Analysis/Analytic/Constructions.lean index fb1f04b56cf27..5b268c5b5d826 100644 --- a/Mathlib/Analysis/Analytic/Constructions.lean +++ b/Mathlib/Analysis/Analytic/Constructions.lean @@ -6,6 +6,7 @@ Authors: David Loeffler, Geoffrey Irving import Mathlib.Analysis.Analytic.Composition import Mathlib.Analysis.Analytic.Linear import Mathlib.Analysis.NormedSpace.OperatorNorm.Mul +import Mathlib.Analysis.Normed.Ring.Units /-! # Various ways to combine analytic functions @@ -603,19 +604,36 @@ lemma AnalyticOn.pow {f : E β†’ A} {s : Set E} (hf : AnalyticOn π•œ f s) (n : section Geometric variable (π•œ A : Type*) [NontriviallyNormedField π•œ] [NormedRing A] [NormedAlgebra π•œ A] - [NormOneClass A] /-- The geometric series `1 + x + x ^ 2 + ...` as a `FormalMultilinearSeries`. -/ def formalMultilinearSeries_geometric : FormalMultilinearSeries π•œ A A := fun n ↦ ContinuousMultilinearMap.mkPiAlgebraFin π•œ n A -lemma formalMultilinearSeries_geometric_apply_norm (n : β„•) : +lemma formalMultilinearSeries_geometric_apply_norm_le (n : β„•) : + β€–formalMultilinearSeries_geometric π•œ A nβ€– ≀ max 1 β€–(1 : A)β€– := + ContinuousMultilinearMap.norm_mkPiAlgebraFin_le + +lemma formalMultilinearSeries_geometric_apply_norm [NormOneClass A] (n : β„•) : β€–formalMultilinearSeries_geometric π•œ A nβ€– = 1 := ContinuousMultilinearMap.norm_mkPiAlgebraFin end Geometric -lemma formalMultilinearSeries_geometric_radius (π•œ) [NontriviallyNormedField π•œ] +lemma one_le_formalMultilinearSeries_geometric_radius (π•œ : Type*) [NontriviallyNormedField π•œ] + (A : Type*) [NormedRing A] [NormedAlgebra π•œ A] : + 1 ≀ (formalMultilinearSeries_geometric π•œ A).radius := by + refine le_of_forall_nnreal_lt (fun r hr ↦ ?_) + rw [← Nat.cast_one, ENNReal.coe_lt_natCast, Nat.cast_one] at hr + apply FormalMultilinearSeries.le_radius_of_isBigO + apply isBigO_of_le' (c := max 1 β€–(1 : A)β€–) atTop (fun n ↦ ?_) + simp only [norm_mul, norm_norm, norm_pow, Real.norm_eq_abs, NNReal.abs_eq, norm_one, mul_one, + abs_norm] + apply le_trans ?_ (formalMultilinearSeries_geometric_apply_norm_le π•œ A n) + conv_rhs => rw [← mul_one (β€–formalMultilinearSeries_geometric π•œ A nβ€–)] + gcongr + exact pow_le_one _ (coe_nonneg r) hr.le + +lemma formalMultilinearSeries_geometric_radius (π•œ : Type*) [NontriviallyNormedField π•œ] (A : Type*) [NormedRing A] [NormOneClass A] [NormedAlgebra π•œ A] : (formalMultilinearSeries_geometric π•œ A).radius = 1 := by apply le_antisymm @@ -641,20 +659,61 @@ lemma formalMultilinearSeries_geometric_radius (π•œ) [NontriviallyNormedField rw [norm_one, Real.norm_of_nonneg (pow_nonneg (coe_nonneg r) _)] exact pow_le_one _ (coe_nonneg r) hr.le -lemma hasFPowerSeriesOnBall_inv_one_sub - (π•œ 𝕝 : Type*) [NontriviallyNormedField π•œ] [NontriviallyNormedField 𝕝] [NormedAlgebra π•œ 𝕝] : - HasFPowerSeriesOnBall (fun x : 𝕝 ↦ (1 - x)⁻¹) (formalMultilinearSeries_geometric π•œ 𝕝) 0 1 := by +lemma hasFPowerSeriesOnBall_inverse_one_sub + (π•œ : Type*) [NontriviallyNormedField π•œ] + (A : Type*) [NormedRing A] [NormedAlgebra π•œ A] [HasSummableGeomSeries A] : + HasFPowerSeriesOnBall (fun x : A ↦ Ring.inverse (1 - x)) + (formalMultilinearSeries_geometric π•œ A) 0 1 := by constructor - Β· exact le_of_eq (formalMultilinearSeries_geometric_radius π•œ 𝕝).symm + Β· exact one_le_formalMultilinearSeries_geometric_radius π•œ A Β· exact one_pos Β· intro y hy - simp_rw [zero_add, formalMultilinearSeries_geometric, - ContinuousMultilinearMap.mkPiAlgebraFin_apply, - List.prod_ofFn, Finset.prod_const, - Finset.card_univ, Fintype.card_fin] - apply hasSum_geometric_of_norm_lt_one - simpa only [← ofReal_one, Metric.emetric_ball, Metric.ball, - dist_eq_norm, sub_zero] using hy + simp only [EMetric.mem_ball, edist_dist, dist_zero_right, ofReal_lt_one] at hy + simp only [zero_add, NormedRing.inverse_one_sub _ hy, Units.oneSub, Units.inv_mk, + formalMultilinearSeries_geometric, ContinuousMultilinearMap.mkPiAlgebraFin_apply, + List.ofFn_const, List.prod_replicate] + exact (summable_geometric_of_norm_lt_one hy).hasSum + +lemma analyticAt_inverse_one_sub (π•œ : Type*) [NontriviallyNormedField π•œ] + (A : Type*) [NormedRing A] [NormedAlgebra π•œ A] [HasSummableGeomSeries A] : + AnalyticAt π•œ (fun x : A ↦ Ring.inverse (1 - x)) 0 := + ⟨_, ⟨_, hasFPowerSeriesOnBall_inverse_one_sub π•œ A⟩⟩ + +/-- If `A` is a normed algebra over `π•œ` with summable geometric series, then inversion on `A` is +analytic at any unit. -/ +lemma analyticAt_inverse {π•œ : Type*} [NontriviallyNormedField π•œ] + {A : Type*} [NormedRing A] [NormedAlgebra π•œ A] [HasSummableGeomSeries A] (z : AΛ£) : + AnalyticAt π•œ Ring.inverse (z : A) := by + rcases subsingleton_or_nontrivial A with hA|hA + Β· convert analyticAt_const (v := (0 : A)) + Β· let f1 : A β†’ A := fun a ↦ a * z.inv + let f2 : A β†’ A := fun b ↦ Ring.inverse (1 - b) + let f3 : A β†’ A := fun c ↦ 1 - z.inv * c + have feq : βˆ€αΆ  y in 𝓝 (z : A), (f1 ∘ f2 ∘ f3) y = Ring.inverse y := by + have : Metric.ball (z : A) (β€–(↑z⁻¹ : A)‖⁻¹) ∈ 𝓝 (z : A) := by + apply Metric.ball_mem_nhds + simp + filter_upwards [this] with y hy + simp only [Metric.mem_ball, dist_eq_norm] at hy + have : y = Units.ofNearby z y hy := rfl + rw [this, Eq.comm] + simp only [Ring.inverse_unit, Function.comp_apply] + simp [Units.ofNearby, f1, f2, f3, Units.add, _root_.mul_sub] + rw [← Ring.inverse_unit] + congr + simp + apply AnalyticAt.congr _ feq + apply (analyticAt_id.mul analyticAt_const).comp + apply AnalyticAt.comp + Β· simp only [Units.inv_eq_val_inv, Units.inv_mul, sub_self, f2, f3] + exact analyticAt_inverse_one_sub π•œ A + Β· exact analyticAt_const.sub (analyticAt_const.mul analyticAt_id) + +lemma hasFPowerSeriesOnBall_inv_one_sub + (π•œ 𝕝 : Type*) [NontriviallyNormedField π•œ] [NontriviallyNormedField 𝕝] [NormedAlgebra π•œ 𝕝] : + HasFPowerSeriesOnBall (fun x : 𝕝 ↦ (1 - x)⁻¹) (formalMultilinearSeries_geometric π•œ 𝕝) 0 1 := by + convert hasFPowerSeriesOnBall_inverse_one_sub π•œ 𝕝 + exact Ring.inverse_eq_inv'.symm lemma analyticAt_inv_one_sub (𝕝 : Type*) [NontriviallyNormedField 𝕝] [NormedAlgebra π•œ 𝕝] : AnalyticAt π•œ (fun x : 𝕝 ↦ (1 - x)⁻¹) 0 := @@ -663,19 +722,8 @@ lemma analyticAt_inv_one_sub (𝕝 : Type*) [NontriviallyNormedField 𝕝] [Norm /-- If `𝕝` is a normed field extension of `π•œ`, then the inverse map `𝕝 β†’ 𝕝` is `π•œ`-analytic away from 0. -/ lemma analyticAt_inv {z : 𝕝} (hz : z β‰  0) : AnalyticAt π•œ Inv.inv z := by - let f1 : 𝕝 β†’ 𝕝 := fun a ↦ 1 / z * a - let f2 : 𝕝 β†’ 𝕝 := fun b ↦ (1 - b)⁻¹ - let f3 : 𝕝 β†’ 𝕝 := fun c ↦ 1 - c / z - have feq : f1 ∘ f2 ∘ f3 = Inv.inv := by - ext1 x - dsimp only [f1, f2, f3, Function.comp_apply] - field_simp - have f3val : f3 z = 0 := by simp only [f3, div_self hz, sub_self] - have f3an : AnalyticAt π•œ f3 z := by - apply analyticAt_const.sub - simpa only [div_eq_inv_mul] using analyticAt_const.mul analyticAt_id - exact feq β–Έ (analyticAt_const.mul analyticAt_id).comp - ((f3val.symm β–Έ analyticAt_inv_one_sub 𝕝).comp f3an) + convert analyticAt_inverse (π•œ := π•œ) (Units.mk0 _ hz) + exact Ring.inverse_eq_inv'.symm /-- `x⁻¹` is analytic away from zero -/ lemma analyticOn_inv : AnalyticOn π•œ (fun z ↦ z⁻¹) {z : 𝕝 | z β‰  0} := by diff --git a/Mathlib/Analysis/Calculus/Deriv/Inv.lean b/Mathlib/Analysis/Calculus/Deriv/Inv.lean index ffa6762826f8e..8687b3af9373d 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Inv.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Inv.lean @@ -63,20 +63,13 @@ theorem hasDerivWithinAt_inv (x_ne_zero : x β‰  0) (s : Set π•œ) : HasDerivWithinAt (fun x => x⁻¹) (-(x ^ 2)⁻¹) s x := (hasDerivAt_inv x_ne_zero).hasDerivWithinAt -theorem differentiableAt_inv : DifferentiableAt π•œ (fun x => x⁻¹) x ↔ x β‰  0 := +theorem differentiableAt_inv_iff : DifferentiableAt π•œ (fun x => x⁻¹) x ↔ x β‰  0 := ⟨fun H => NormedField.continuousAt_inv.1 H.continuousAt, fun H => (hasDerivAt_inv H).differentiableAt⟩ -theorem differentiableWithinAt_inv (x_ne_zero : x β‰  0) : - DifferentiableWithinAt π•œ (fun x => x⁻¹) s x := - (differentiableAt_inv.2 x_ne_zero).differentiableWithinAt - -theorem differentiableOn_inv : DifferentiableOn π•œ (fun x : π•œ => x⁻¹) { x | x β‰  0 } := fun _x hx => - differentiableWithinAt_inv hx - theorem deriv_inv : deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹ := by rcases eq_or_ne x 0 with (rfl | hne) - Β· simp [deriv_zero_of_not_differentiableAt (mt differentiableAt_inv.1 (not_not.2 rfl))] + Β· simp [deriv_zero_of_not_differentiableAt (mt differentiableAt_inv_iff.1 (not_not.2 rfl))] Β· exact (hasDerivAt_inv hne).deriv @[simp] @@ -85,13 +78,17 @@ theorem deriv_inv' : (deriv fun x : π•œ => x⁻¹) = fun x => -(x ^ 2)⁻¹ := theorem derivWithin_inv (x_ne_zero : x β‰  0) (hxs : UniqueDiffWithinAt π•œ s x) : derivWithin (fun x => x⁻¹) s x = -(x ^ 2)⁻¹ := by - rw [DifferentiableAt.derivWithin (differentiableAt_inv.2 x_ne_zero) hxs] + rw [DifferentiableAt.derivWithin (differentiableAt_inv x_ne_zero) hxs] exact deriv_inv theorem hasFDerivAt_inv (x_ne_zero : x β‰  0) : HasFDerivAt (fun x => x⁻¹) (smulRight (1 : π•œ β†’L[π•œ] π•œ) (-(x ^ 2)⁻¹) : π•œ β†’L[π•œ] π•œ) x := hasDerivAt_inv x_ne_zero +theorem hasStrictFDerivAt_inv (x_ne_zero : x β‰  0) : + HasStrictFDerivAt (fun x => x⁻¹) (smulRight (1 : π•œ β†’L[π•œ] π•œ) (-(x ^ 2)⁻¹) : π•œ β†’L[π•œ] π•œ) x := + hasStrictDerivAt_inv x_ne_zero + theorem hasFDerivWithinAt_inv (x_ne_zero : x β‰  0) : HasFDerivWithinAt (fun x => x⁻¹) (smulRight (1 : π•œ β†’L[π•œ] π•œ) (-(x ^ 2)⁻¹) : π•œ β†’L[π•œ] π•œ) s x := (hasFDerivAt_inv x_ne_zero).hasFDerivWithinAt @@ -101,7 +98,7 @@ theorem fderiv_inv : fderiv π•œ (fun x => x⁻¹) x = smulRight (1 : π•œ β†’L[ theorem fderivWithin_inv (x_ne_zero : x β‰  0) (hxs : UniqueDiffWithinAt π•œ s x) : fderivWithin π•œ (fun x => x⁻¹) s x = smulRight (1 : π•œ β†’L[π•œ] π•œ) (-(x ^ 2)⁻¹) := by - rw [DifferentiableAt.fderivWithin (differentiableAt_inv.2 x_ne_zero) hxs] + rw [DifferentiableAt.fderivWithin (differentiableAt_inv x_ne_zero) hxs] exact fderiv_inv variable {c : π•œ β†’ π•œ} {h : E β†’ π•œ} {c' : π•œ} {z : E} {S : Set E} @@ -116,22 +113,6 @@ theorem HasDerivAt.inv (hc : HasDerivAt c c' x) (hx : c x β‰  0) : rw [← hasDerivWithinAt_univ] at * exact hc.inv hx -theorem DifferentiableWithinAt.inv (hf : DifferentiableWithinAt π•œ h S z) (hz : h z β‰  0) : - DifferentiableWithinAt π•œ (fun x => (h x)⁻¹) S z := - (differentiableAt_inv.mpr hz).comp_differentiableWithinAt z hf - -@[simp] -theorem DifferentiableAt.inv (hf : DifferentiableAt π•œ h z) (hz : h z β‰  0) : - DifferentiableAt π•œ (fun x => (h x)⁻¹) z := - (differentiableAt_inv.mpr hz).comp z hf - -theorem DifferentiableOn.inv (hf : DifferentiableOn π•œ h S) (hz : βˆ€ x ∈ S, h x β‰  0) : - DifferentiableOn π•œ (fun x => (h x)⁻¹) S := fun x h => (hf x h).inv (hz x h) - -@[simp] -theorem Differentiable.inv (hf : Differentiable π•œ h) (hz : βˆ€ x, h x β‰  0) : - Differentiable π•œ fun x => (h x)⁻¹ := fun x => (hf x).inv (hz x) - theorem derivWithin_inv' (hc : DifferentiableWithinAt π•œ c s x) (hx : c x β‰  0) (hxs : UniqueDiffWithinAt π•œ s x) : derivWithin (fun x => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2 := diff --git a/Mathlib/Analysis/Calculus/DiffContOnCl.lean b/Mathlib/Analysis/Calculus/DiffContOnCl.lean index 10a6fd3b0a289..03f7ad0b9609c 100644 --- a/Mathlib/Analysis/Calculus/DiffContOnCl.lean +++ b/Mathlib/Analysis/Calculus/DiffContOnCl.lean @@ -3,8 +3,9 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury Kudryashov -/ -import Mathlib.Analysis.Calculus.Deriv.Inv import Mathlib.Analysis.NormedSpace.Real +import Mathlib.Analysis.Calculus.FDeriv.Add +import Mathlib.Analysis.Calculus.FDeriv.Mul /-! # Functions differentiable on a domain and continuous on its closure diff --git a/Mathlib/Analysis/Calculus/Dslope.lean b/Mathlib/Analysis/Calculus/Dslope.lean index a35fb76d7fa45..df304274fc2ac 100644 --- a/Mathlib/Analysis/Calculus/Dslope.lean +++ b/Mathlib/Analysis/Calculus/Dslope.lean @@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury Kudryashov -/ import Mathlib.Analysis.Calculus.Deriv.Slope -import Mathlib.Analysis.Calculus.Deriv.Inv +import Mathlib.Analysis.Calculus.Deriv.Comp +import Mathlib.Analysis.Calculus.FDeriv.Add +import Mathlib.Analysis.Calculus.FDeriv.Mul /-! # Slope of a differentiable function diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean index 328fdab8161af..ef38ec6312a71 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean @@ -58,6 +58,12 @@ theorem HasFPowerSeriesAt.fderiv_eq (h : HasFPowerSeriesAt f p x) : fderiv π•œ f x = continuousMultilinearCurryFin1 π•œ E F (p 1) := h.hasFDerivAt.fderiv +theorem AnalyticAt.hasStrictFDerivAt (h : AnalyticAt π•œ f x) : + HasStrictFDerivAt f (fderiv π•œ f x) x := by + rcases h with ⟨p, hp⟩ + rw [hp.fderiv_eq] + exact hp.hasStrictFDerivAt + theorem HasFPowerSeriesOnBall.differentiableOn [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) : DifferentiableOn π•œ f (EMetric.ball x r) := fun _ hy => (h.analyticAt_of_mem hy).differentiableWithinAt diff --git a/Mathlib/Analysis/Calculus/FDeriv/Mul.lean b/Mathlib/Analysis/Calculus/FDeriv/Mul.lean index 47dd475da18fc..d867ef086d9c7 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Mul.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Mul.lean @@ -3,6 +3,8 @@ Copyright (c) 2019 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, SΓ©bastien GouΓ«zel, Yury Kudryashov -/ +import Mathlib.Analysis.Analytic.Constructions +import Mathlib.Analysis.Calculus.FDeriv.Analytic import Mathlib.Analysis.Calculus.FDeriv.Bilinear /-! @@ -775,16 +777,15 @@ end Prod section AlgebraInverse -variable {R : Type*} [NormedRing R] [NormedAlgebra π•œ R] [CompleteSpace R] +variable {R : Type*} [NormedRing R] [HasSummableGeomSeries R] [NormedAlgebra π•œ R] open NormedRing ContinuousLinearMap Ring /-- At an invertible element `x` of a normed algebra `R`, the FrΓ©chet derivative of the inversion operation is the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`. -TODO: prove that `Ring.inverse` is analytic and use it to prove a `HasStrictFDerivAt` lemma. -TODO (low prio): prove a version without assumption `[CompleteSpace R]` but within the set of -units. -/ +TODO (low prio): prove a version without assumption `[HasSummableGeomSeries R]` but within the set +of units. -/ @[fun_prop] theorem hasFDerivAt_ring_inverse (x : RΛ£) : HasFDerivAt Ring.inverse (-mulLeftRight π•œ R ↑x⁻¹ ↑x⁻¹) x := @@ -809,6 +810,11 @@ theorem differentiableOn_inverse : DifferentiableOn π•œ (@Ring.inverse R _) {x theorem fderiv_inverse (x : RΛ£) : fderiv π•œ (@Ring.inverse R _) x = -mulLeftRight π•œ R ↑x⁻¹ ↑x⁻¹ := (hasFDerivAt_ring_inverse x).fderiv +theorem hasStrictFDerivAt_ring_inverse (x : RΛ£) : + HasStrictFDerivAt Ring.inverse (-mulLeftRight π•œ R ↑x⁻¹ ↑x⁻¹) x := by + convert (analyticAt_inverse (π•œ := π•œ) x).hasStrictFDerivAt + exact (fderiv_inverse x).symm + variable {h : E β†’ R} {z : E} {S : Set E} @[fun_prop] @@ -833,35 +839,51 @@ end AlgebraInverse /-! ### Derivative of the inverse in a division ring -Note these lemmas are primed as they need `CompleteSpace R`, whereas the other lemmas in -`Mathlib/Analysis/Calculus/Deriv/Inv.lean` do not, but instead need `NontriviallyNormedField R`. +Note that some lemmas are primed as they are expressed without commutativity, whereas their +counterparts in commutative fields involve simpler expressions, and are given in +`Mathlib/Analysis/Calculus/Deriv/Inv.lean`. -/ section DivisionRingInverse -variable {R : Type*} [NormedDivisionRing R] [NormedAlgebra π•œ R] [CompleteSpace R] +variable {R : Type*} [NormedDivisionRing R] [NormedAlgebra π•œ R] open NormedRing ContinuousLinearMap Ring +/-- At an invertible element `x` of a normed division algebra `R`, the inversion is strictly +differentiable, with derivative the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`. For a nicer formula in +the commutative case, see `hasStrictFDerivAt_inv`. -/ +theorem hasStrictFDerivAt_inv' {x : R} (hx : x β‰  0) : + HasStrictFDerivAt Inv.inv (-mulLeftRight π•œ R x⁻¹ x⁻¹) x := by + simpa using hasStrictFDerivAt_ring_inverse (Units.mk0 _ hx) + /-- At an invertible element `x` of a normed division algebra `R`, the FrΓ©chet derivative of the -inversion operation is the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`. -/ +inversion operation is the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`. For a nicer formula in the +commutative case, see `hasFDerivAt_inv`. -/ @[fun_prop] theorem hasFDerivAt_inv' {x : R} (hx : x β‰  0) : HasFDerivAt Inv.inv (-mulLeftRight π•œ R x⁻¹ x⁻¹) x := by simpa using hasFDerivAt_ring_inverse (Units.mk0 _ hx) @[fun_prop] -theorem differentiableAt_inv' {x : R} (hx : x β‰  0) : DifferentiableAt π•œ Inv.inv x := +theorem differentiableAt_inv {x : R} (hx : x β‰  0) : DifferentiableAt π•œ Inv.inv x := (hasFDerivAt_inv' hx).differentiableAt +@[deprecated (since := "2024-09-21")] alias differentiableAt_inv' := differentiableAt_inv + @[fun_prop] -theorem differentiableWithinAt_inv' {x : R} (hx : x β‰  0) (s : Set R) : +theorem differentiableWithinAt_inv {x : R} (hx : x β‰  0) (s : Set R) : DifferentiableWithinAt π•œ (fun x => x⁻¹) s x := - (differentiableAt_inv' hx).differentiableWithinAt + (differentiableAt_inv hx).differentiableWithinAt + +@[deprecated (since := "2024-09-21")] +alias differentiableWithinAt_inv' := differentiableWithinAt_inv @[fun_prop] -theorem differentiableOn_inv' : DifferentiableOn π•œ (fun x : R => x⁻¹) {x | x β‰  0} := fun _x hx => - differentiableWithinAt_inv' hx _ +theorem differentiableOn_inv : DifferentiableOn π•œ (fun x : R => x⁻¹) {x | x β‰  0} := fun _x hx => + differentiableWithinAt_inv hx _ + +@[deprecated (since := "2024-09-21")] alias differentiableOn_inv' := differentiableOn_inv /-- Non-commutative version of `fderiv_inv` -/ theorem fderiv_inv' {x : R} (hx : x β‰  0) : fderiv π•œ Inv.inv x = -mulLeftRight π•œ R x⁻¹ x⁻¹ := @@ -870,28 +892,37 @@ theorem fderiv_inv' {x : R} (hx : x β‰  0) : fderiv π•œ Inv.inv x = -mulLeftRig /-- Non-commutative version of `fderivWithin_inv` -/ theorem fderivWithin_inv' {s : Set R} {x : R} (hx : x β‰  0) (hxs : UniqueDiffWithinAt π•œ s x) : fderivWithin π•œ (fun x => x⁻¹) s x = -mulLeftRight π•œ R x⁻¹ x⁻¹ := by - rw [DifferentiableAt.fderivWithin (differentiableAt_inv' hx) hxs] + rw [DifferentiableAt.fderivWithin (differentiableAt_inv hx) hxs] exact fderiv_inv' hx variable {h : E β†’ R} {z : E} {S : Set E} @[fun_prop] -theorem DifferentiableWithinAt.inv' (hf : DifferentiableWithinAt π•œ h S z) (hz : h z β‰  0) : +theorem DifferentiableWithinAt.inv (hf : DifferentiableWithinAt π•œ h S z) (hz : h z β‰  0) : DifferentiableWithinAt π•œ (fun x => (h x)⁻¹) S z := - (differentiableAt_inv' hz).comp_differentiableWithinAt z hf + (differentiableAt_inv hz).comp_differentiableWithinAt z hf + +@[deprecated (since := "2024-09-21")] +alias DifferentiableWithinAt.inv' := DifferentiableWithinAt.inv @[simp, fun_prop] -theorem DifferentiableAt.inv' (hf : DifferentiableAt π•œ h z) (hz : h z β‰  0) : +theorem DifferentiableAt.inv (hf : DifferentiableAt π•œ h z) (hz : h z β‰  0) : DifferentiableAt π•œ (fun x => (h x)⁻¹) z := - (differentiableAt_inv' hz).comp z hf + (differentiableAt_inv hz).comp z hf + +@[deprecated (since := "2024-09-21")] alias DifferentiableAt.inv' := DifferentiableAt.inv @[fun_prop] -theorem DifferentiableOn.inv' (hf : DifferentiableOn π•œ h S) (hz : βˆ€ x ∈ S, h x β‰  0) : - DifferentiableOn π•œ (fun x => (h x)⁻¹) S := fun x h => (hf x h).inv' (hz x h) +theorem DifferentiableOn.inv (hf : DifferentiableOn π•œ h S) (hz : βˆ€ x ∈ S, h x β‰  0) : + DifferentiableOn π•œ (fun x => (h x)⁻¹) S := fun x h => (hf x h).inv (hz x h) + +@[deprecated (since := "2024-09-21")] alias DifferentiableOn.inv' := DifferentiableOn.inv @[simp, fun_prop] -theorem Differentiable.inv' (hf : Differentiable π•œ h) (hz : βˆ€ x, h x β‰  0) : - Differentiable π•œ fun x => (h x)⁻¹ := fun x => (hf x).inv' (hz x) +theorem Differentiable.inv (hf : Differentiable π•œ h) (hz : βˆ€ x, h x β‰  0) : + Differentiable π•œ fun x => (h x)⁻¹ := fun x => (hf x).inv (hz x) + +@[deprecated (since := "2024-09-21")] alias Differentiable.inv' := Differentiable.inv end DivisionRingInverse diff --git a/Mathlib/Analysis/Normed/Algebra/Spectrum.lean b/Mathlib/Analysis/Normed/Algebra/Spectrum.lean index 6bdbec8adca03..f967929332fbd 100644 --- a/Mathlib/Analysis/Normed/Algebra/Spectrum.lean +++ b/Mathlib/Analysis/Normed/Algebra/Spectrum.lean @@ -272,7 +272,7 @@ variable (π•œ) /-- In a Banach algebra `A` over a nontrivially normed field `π•œ`, for any `a : A` the power series with coefficients `a ^ n` represents the function `(1 - z β€’ a)⁻¹` in a disk of radius `β€–aβ€–β‚Šβ»ΒΉ`. -/ -theorem hasFPowerSeriesOnBall_inverse_one_sub_smul [CompleteSpace A] (a : A) : +theorem hasFPowerSeriesOnBall_inverse_one_sub_smul [HasSummableGeomSeries A] (a : A) : HasFPowerSeriesOnBall (fun z : π•œ => Ring.inverse (1 - z β€’ a)) (fun n => ContinuousMultilinearMap.mkPiRing π•œ (Fin n) (a ^ n)) 0 β€–aβ€–β‚Šβ»ΒΉ := { r_le := by @@ -297,7 +297,7 @@ theorem hasFPowerSeriesOnBall_inverse_one_sub_smul [CompleteSpace A] (a : A) : simpa only [← coe_inv h, mem_ball_zero_iff, Metric.emetric_ball_nnreal] using hy rwa [← coe_nnnorm, ← Real.lt_toNNReal_iff_coe_lt, Real.toNNReal_one, nnnorm_smul, ← NNReal.lt_inv_iff_mul_lt h] - simpa [← smul_pow, (NormedRing.summable_geometric_of_norm_lt_one _ norm_lt).hasSum_iff] using + simpa [← smul_pow, (summable_geometric_of_norm_lt_one norm_lt).hasSum_iff] using (NormedRing.inverse_one_sub _ norm_lt).symm } variable {π•œ} diff --git a/Mathlib/Analysis/Normed/Ring/Units.lean b/Mathlib/Analysis/Normed/Ring/Units.lean index a99777748c99d..6a9faca97ff80 100644 --- a/Mathlib/Analysis/Normed/Ring/Units.lean +++ b/Mathlib/Analysis/Normed/Ring/Units.lean @@ -14,12 +14,12 @@ normed ring (Banach algebras being a notable special case). ## Main results -The constructions `Units.oneSub`, `Units.add`, and `Units.ofNearby` state, in varying forms, that -perturbations of a unit are units. The latter two are not stated in their optimal form; more precise -versions would use the spectral radius. +The constructions `Units.add` and `Units.ofNearby` (based on `Units.oneSub` defined elsewhere) +state, in varying forms, that perturbations of a unit are units. They are not stated +in their optimal form; more precise versions would use the spectral radius. -The first main result is `Units.isOpen`: the group of units of a complete normed ring is an open -subset of the ring. +The first main result is `Units.isOpen`: the group of units of a normed ring with summable +geometric series is an open subset of the ring. The function `Ring.inverse` (defined elsewhere), for a ring `R`, sends `a : R` to `a⁻¹` if `a` is a unit and `0` if not. The other major results of this file (notably `NormedRing.inverse_add`, @@ -31,21 +31,13 @@ noncomputable section open Topology -variable {R : Type*} [NormedRing R] [CompleteSpace R] +variable {R : Type*} [NormedRing R] [HasSummableGeomSeries R] namespace Units -/-- In a complete normed ring, a perturbation of `1` by an element `t` of distance less than `1` -from `1` is a unit. Here we construct its `Units` structure. -/ -@[simps val] -def oneSub (t : R) (h : β€–tβ€– < 1) : RΛ£ where - val := 1 - t - inv := βˆ‘' n : β„•, t ^ n - val_inv := mul_neg_geom_series t h - inv_val := geom_series_mul_neg t h - -/-- In a complete normed ring, a perturbation of a unit `x` by an element `t` of distance less than -`β€–x⁻¹‖⁻¹` from `x` is a unit. Here we construct its `Units` structure. -/ +/-- In a normed ring with summable geometric series, a perturbation of a unit `x` by an +element `t` of distance less than `β€–x⁻¹‖⁻¹` from `x` is a unit. +Here we construct its `Units` structure. -/ @[simps! val] def add (x : RΛ£) (t : R) (h : β€–tβ€– < β€–(↑x⁻¹ : R)‖⁻¹) : RΛ£ := Units.copy -- to make `add_val` true definitionally, for convenience @@ -59,13 +51,14 @@ def add (x : RΛ£) (t : R) (h : β€–tβ€– < β€–(↑x⁻¹ : R)‖⁻¹) : RΛ£ := _ = 1 := mul_inv_cancelβ‚€ (ne_of_gt hpos))) (x + t) (by simp [mul_add]) _ rfl -/-- In a complete normed ring, an element `y` of distance less than `β€–x⁻¹‖⁻¹` from `x` is a unit. -Here we construct its `Units` structure. -/ +/-- In a normed ring with summable geometric series, an element `y` of distance less +than `β€–x⁻¹‖⁻¹` from `x` is a unit. Here we construct its `Units` structure. -/ @[simps! val] def ofNearby (x : RΛ£) (y : R) (h : β€–y - xβ€– < β€–(↑x⁻¹ : R)‖⁻¹) : RΛ£ := (x.add (y - x : R) h).copy y (by simp) _ rfl -/-- The group of units of a complete normed ring is an open subset of the ring. -/ +/-- The group of units of a normed ring with summable geometric series is an open subset +of the ring. -/ protected theorem isOpen : IsOpen { x : R | IsUnit x } := by nontriviality R rw [Metric.isOpen_iff] @@ -81,12 +74,12 @@ end Units namespace nonunits -/-- The `nonunits` in a complete normed ring are contained in the complement of the ball of radius -`1` centered at `1 : R`. -/ +/-- The `nonunits` in a normed ring with summable geometric series are contained in the +complement of the ball of radius `1` centered at `1 : R`. -/ theorem subset_compl_ball : nonunits R βŠ† (Metric.ball (1 : R) 1)ᢜ := fun x hx h₁ ↦ hx <| sub_sub_self 1 x β–Έ (Units.oneSub (1 - x) (by rwa [mem_ball_iff_norm'] at h₁)).isUnit --- The `nonunits` in a complete normed ring are a closed set +-- The `nonunits` in a normed ring with summable geometric series are a closed set protected theorem isClosed : IsClosed (nonunits R) := Units.isOpen.isClosed_compl @@ -114,7 +107,7 @@ theorem inverse_add (x : RΛ£) : theorem inverse_one_sub_nth_order' (n : β„•) {t : R} (ht : β€–tβ€– < 1) : inverse ((1 : R) - t) = (βˆ‘ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t) := - have := NormedRing.summable_geometric_of_norm_lt_one t ht + have := _root_.summable_geometric_of_norm_lt_one ht calc inverse (1 - t) = βˆ‘' i : β„•, t ^ i := inverse_one_sub t ht _ = βˆ‘ i ∈ range n, t ^ i + βˆ‘' i : β„•, t ^ (i + n) := (sum_add_tsum_nat_add _ this).symm _ = (βˆ‘ i ∈ range n, t ^ i) + t ^ n * inverse (1 - t) := by @@ -149,7 +142,7 @@ theorem inverse_one_sub_norm : (fun t : R => inverse (1 - t)) =O[𝓝 0] (fun _t linarith simp only [inverse_one_sub t ht', norm_one, mul_one, Set.mem_setOf_eq] change β€–βˆ‘' n : β„•, t ^ nβ€– ≀ _ - have := NormedRing.tsum_geometric_of_norm_lt_one t ht' + have := tsum_geometric_le_of_norm_lt_one t ht' have : (1 - β€–tβ€–)⁻¹ ≀ 2 := by rw [← inv_inv (2 : ℝ)] refine inv_le_inv_of_le (by norm_num) ?_ @@ -205,15 +198,15 @@ namespace Units open MulOpposite Filter NormedRing -/-- In a normed ring, the coercion from `RΛ£` (equipped with the induced topology from the -embedding in `R Γ— R`) to `R` is an open embedding. -/ +/-- In a normed ring with summable geometric series, the coercion from `RΛ£` (equipped with the +induced topology from the embedding in `R Γ— R`) to `R` is an open embedding. -/ theorem openEmbedding_val : OpenEmbedding (val : RΛ£ β†’ R) where toEmbedding := embedding_val_mk' (fun _ ⟨u, hu⟩ ↦ hu β–Έ (inverse_continuousAt u).continuousWithinAt) Ring.inverse_unit isOpen_range := Units.isOpen -/-- In a normed ring, the coercion from `RΛ£` (equipped with the induced topology from the -embedding in `R Γ— R`) to `R` is an open map. -/ +/-- In a normed ring with summable geometric series, the coercion from `RΛ£` (equipped with the +induced topology from the embedding in `R Γ— R`) to `R` is an open map. -/ theorem isOpenMap_val : IsOpenMap (val : RΛ£ β†’ R) := openEmbedding_val.isOpenMap @@ -227,16 +220,18 @@ theorem eq_top_of_norm_lt_one (I : Ideal R) {x : R} (hxI : x ∈ I) (hx : β€–1 - I.eq_top_iff_one.mpr <| by simpa only [show u.inv * x = 1 by simp [u]] using I.mul_mem_left u.inv hxI -/-- The `Ideal.closure` of a proper ideal in a complete normed ring is proper. -/ +/-- The `Ideal.closure` of a proper ideal in a normed ring with summable +geometric series is proper. -/ theorem closure_ne_top (I : Ideal R) (hI : I β‰  ⊀) : I.closure β‰  ⊀ := by have h := closure_minimal (coe_subset_nonunits hI) nonunits.isClosed simpa only [I.closure.eq_top_iff_one, Ne] using mt (@h 1) one_not_mem_nonunits -/-- The `Ideal.closure` of a maximal ideal in a complete normed ring is the ideal itself. -/ +/-- The `Ideal.closure` of a maximal ideal in a normed ring with summable +geometric series is the ideal itself. -/ theorem IsMaximal.closure_eq {I : Ideal R} (hI : I.IsMaximal) : I.closure = I := (hI.eq_of_le (I.closure_ne_top hI.ne_top) subset_closure).symm -/-- Maximal ideals in complete normed rings are closed. -/ +/-- Maximal ideals in normed rings with summable geometric series are closed. -/ instance IsMaximal.isClosed {I : Ideal R} [hI : I.IsMaximal] : IsClosed (I : Set R) := isClosed_of_closure_subset <| Eq.subset <| congr_arg ((↑) : Ideal R β†’ Set R) hI.closure_eq diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean index 1cc64031c7c79..8c50769ed4fbd 100644 --- a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean +++ b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean @@ -763,6 +763,12 @@ theorem norm_mkPiAlgebraFin_zero : β€–ContinuousMultilinearMap.mkPiAlgebraFin Β· convert ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin π•œ 0 A) fun _ => (1 : A) simp +theorem norm_mkPiAlgebraFin_le : + β€–ContinuousMultilinearMap.mkPiAlgebraFin π•œ n Aβ€– ≀ max 1 β€–(1 : A)β€– := by + cases n + Β· exact norm_mkPiAlgebraFin_zero.le.trans (le_max_right _ _) + Β· exact (norm_mkPiAlgebraFin_le_of_pos (Nat.zero_lt_succ _)).trans (le_max_left _ _) + @[simp] theorem norm_mkPiAlgebraFin [NormOneClass A] : β€–ContinuousMultilinearMap.mkPiAlgebraFin π•œ n Aβ€– = 1 := by diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index d15e75afada5e..a84b941a538ea 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -20,19 +20,13 @@ import Mathlib.Tactic.NoncommRing This file contains important specific limit computations in (semi-)normed groups/rings/spaces, as well as such computations in `ℝ` when the natural proof passes through a fact about normed spaces. - -/ - noncomputable section -open scoped Classical -open Set Function Filter Finset Metric Asymptotics +open Set Function Filter Finset Metric Asymptotics Topology Nat NNReal ENNReal -open scoped Classical -open Topology Nat uniformity NNReal ENNReal - -variable {Ξ± : Type*} {Ξ² : Type*} {ΞΉ : Type*} +variable {Ξ± Ξ² ΞΉ : Type*} theorem tendsto_norm_atTop_atTop : Tendsto (norm : ℝ β†’ ℝ) atTop atTop := tendsto_abs_atTop_atTop @@ -255,6 +249,113 @@ alias tendsto_pow_atTop_nhds_0_of_abs_lt_1 := tendsto_pow_atTop_nhds_zero_of_abs /-! ### Geometric series -/ +/-- A normed ring has summable geometric series if, for all `ΞΎ` of norm `< 1`, the geometric series +`βˆ‘ ΞΎ ^ n` converges. This holds both in complete normed rings and in normed fields, providing a +convenient abstraction of these two classes to avoid repeating the same proofs. -/ +class HasSummableGeomSeries (K : Type*) [NormedRing K] : Prop := + summable_geometric_of_norm_lt_one : βˆ€ (ΞΎ : K), β€–ΞΎβ€– < 1 β†’ Summable (fun n ↦ ΞΎ ^ n) + +lemma summable_geometric_of_norm_lt_one {K : Type*} [NormedRing K] [HasSummableGeomSeries K] + {x : K} (h : β€–xβ€– < 1) : Summable (fun n ↦ x ^ n) := + HasSummableGeomSeries.summable_geometric_of_norm_lt_one x h + +instance {R : Type*} [NormedRing R] [CompleteSpace R] : HasSummableGeomSeries R := by + constructor + intro x hx + have h1 : Summable fun n : β„• ↦ β€–xβ€– ^ n := summable_geometric_of_lt_one (norm_nonneg _) hx + exact h1.of_norm_bounded_eventually_nat _ (eventually_norm_pow_le x) + +section HasSummableGeometricSeries + +variable {R : Type*} [NormedRing R] + +open NormedSpace + +/-- Bound for the sum of a geometric series in a normed ring. This formula does not assume that the +normed ring satisfies the axiom `β€–1β€– = 1`. -/ +theorem tsum_geometric_le_of_norm_lt_one (x : R) (h : β€–xβ€– < 1) : + β€–βˆ‘' n : β„•, x ^ nβ€– ≀ β€–(1 : R)β€– - 1 + (1 - β€–xβ€–)⁻¹ := by + by_cases hx : Summable (fun n ↦ x ^ n) + Β· rw [tsum_eq_zero_add hx] + simp only [_root_.pow_zero] + refine le_trans (norm_add_le _ _) ?_ + have : β€–βˆ‘' b : β„•, (fun n ↦ x ^ (n + 1)) bβ€– ≀ (1 - β€–xβ€–)⁻¹ - 1 := by + refine tsum_of_norm_bounded ?_ fun b ↦ norm_pow_le' _ (Nat.succ_pos b) + convert (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h) + simp + linarith + Β· simp [tsum_eq_zero_of_not_summable hx] + nontriviality R + have : 1 ≀ β€–(1 : R)β€– := one_le_norm_one R + have : 0 ≀ (1 - β€–xβ€–) ⁻¹ := inv_nonneg.2 (by linarith) + linarith + +variable [HasSummableGeomSeries R] + +@[deprecated (since := "2024-01-31")] +alias NormedRing.tsum_geometric_of_norm_lt_1 := tsum_geometric_le_of_norm_lt_one + +@[deprecated (since := "2024-07-27")] +alias NormedRing.tsum_geometric_of_norm_lt_one := tsum_geometric_le_of_norm_lt_one + +theorem geom_series_mul_neg (x : R) (h : β€–xβ€– < 1) : (βˆ‘' i : β„•, x ^ i) * (1 - x) = 1 := by + have := (summable_geometric_of_norm_lt_one h).hasSum.mul_right (1 - x) + refine tendsto_nhds_unique this.tendsto_sum_nat ?_ + have : Tendsto (fun n : β„• ↦ 1 - x ^ n) atTop (𝓝 1) := by + simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h) + convert← this + rw [← geom_sum_mul_neg, Finset.sum_mul] + +theorem mul_neg_geom_series (x : R) (h : β€–xβ€– < 1) : (1 - x) * βˆ‘' i : β„•, x ^ i = 1 := by + have := (summable_geometric_of_norm_lt_one h).hasSum.mul_left (1 - x) + refine tendsto_nhds_unique this.tendsto_sum_nat ?_ + have : Tendsto (fun n : β„• ↦ 1 - x ^ n) atTop (𝓝 1) := by + simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h) + convert← this + rw [← mul_neg_geom_sum, Finset.mul_sum] + +theorem geom_series_succ (x : R) (h : β€–xβ€– < 1) : βˆ‘' i : β„•, x ^ (i + 1) = βˆ‘' i : β„•, x ^ i - 1 := by + rw [eq_sub_iff_add_eq, tsum_eq_zero_add (summable_geometric_of_norm_lt_one h), + pow_zero, add_comm] + +theorem geom_series_mul_shift (x : R) (h : β€–xβ€– < 1) : + x * βˆ‘' i : β„•, x ^ i = βˆ‘' i : β„•, x ^ (i + 1) := by + simp_rw [← (summable_geometric_of_norm_lt_one h).tsum_mul_left, ← _root_.pow_succ'] + +theorem geom_series_mul_one_add (x : R) (h : β€–xβ€– < 1) : + (1 + x) * βˆ‘' i : β„•, x ^ i = 2 * βˆ‘' i : β„•, x ^ i - 1 := by + rw [add_mul, one_mul, geom_series_mul_shift x h, geom_series_succ x h, two_mul, add_sub_assoc] + +/-- In a normed ring with summable geometric series, a perturbation of `1` by an element `t` +of distance less than `1` from `1` is a unit. Here we construct its `Units` structure. -/ +@[simps val] +def Units.oneSub (t : R) (h : β€–tβ€– < 1) : RΛ£ where + val := 1 - t + inv := βˆ‘' n : β„•, t ^ n + val_inv := mul_neg_geom_series t h + inv_val := geom_series_mul_neg t h + +theorem geom_series_eq_inverse (x : R) (h : β€–xβ€– < 1) : + βˆ‘' i, x ^ i = Ring.inverse (1 - x) := by + change (Units.oneSub x h) ⁻¹ = Ring.inverse (1 - x) + rw [← Ring.inverse_unit] + rfl + +theorem hasSum_geom_series_inverse (x : R) (h : β€–xβ€– < 1) : + HasSum (fun i ↦ x ^ i) (Ring.inverse (1 - x)) := by + convert (summable_geometric_of_norm_lt_one h).hasSum + exact (geom_series_eq_inverse x h).symm + +lemma isUnit_one_sub_of_norm_lt_one {x : R} (h : β€–xβ€– < 1) : IsUnit (1 - x) := + ⟨Units.oneSub x h, rfl⟩ + +end HasSummableGeometricSeries + +@[deprecated (since := "2024-01-31")] +alias NormedRing.summable_geometric_of_norm_lt_1 := summable_geometric_of_norm_lt_one + +@[deprecated (since := "2024-07-27")] +alias NormedRing.summable_geometric_of_norm_lt_one := summable_geometric_of_norm_lt_one section Geometric @@ -273,8 +374,8 @@ theorem hasSum_geometric_of_norm_lt_one (h : β€–ΞΎβ€– < 1) : HasSum (fun n : β„• @[deprecated (since := "2024-01-31")] alias hasSum_geometric_of_norm_lt_1 := hasSum_geometric_of_norm_lt_one -theorem summable_geometric_of_norm_lt_one (h : β€–ΞΎβ€– < 1) : Summable fun n : β„• ↦ ΞΎ ^ n := - ⟨_, hasSum_geometric_of_norm_lt_one h⟩ +instance : HasSummableGeomSeries K := + ⟨fun _ h ↦ (hasSum_geometric_of_norm_lt_one h).summable⟩ @[deprecated (since := "2024-01-31")] alias summable_geometric_of_norm_lt_1 := summable_geometric_of_norm_lt_one @@ -322,7 +423,9 @@ end Geometric section MulGeometric -theorem summable_norm_mul_geometric_of_norm_lt_one {R : Type*} [NormedRing R] {k : β„•} {r : R} +variable {R : Type*} [NormedRing R] {π•œ : Type*} [NormedDivisionRing π•œ] + +theorem summable_norm_mul_geometric_of_norm_lt_one {k : β„•} {r : R} (hr : β€–rβ€– < 1) {u : β„• β†’ β„•} (hu : (fun n ↦ (u n : ℝ)) =O[atTop] (fun n ↦ (↑(n ^ k) : ℝ))) : Summable fun n : β„• ↦ β€–(u n * r ^ n : R)β€– := by rcases exists_between hr with ⟨r', hrr', h⟩ @@ -337,35 +440,29 @@ theorem summable_norm_mul_geometric_of_norm_lt_one {R : Type*} [NormedRing R] {k apply (norm_mul_le _ _).trans have : β€–(u n : R)β€– * β€–r ^ nβ€– ≀ (u n * β€–(1 : R)β€–) * β€–rβ€– ^ n := by gcongr; exact norm_cast_le (u n) - exact this.trans_eq (by ring) + exact this.trans (le_of_eq (by ring)) _ =O[atTop] fun n ↦ ↑(n ^ k) * β€–rβ€– ^ n := hu.mul (isBigO_refl _ _) _ =O[atTop] fun n ↦ r' ^ n := by simp only [cast_pow] exact (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO -theorem summable_norm_pow_mul_geometric_of_norm_lt_one {R : Type*} [NormedRing R] (k : β„•) {r : R} +theorem summable_norm_pow_mul_geometric_of_norm_lt_one (k : β„•) {r : R} (hr : β€–rβ€– < 1) : Summable fun n : β„• ↦ β€–((n : R) ^ k * r ^ n : R)β€– := by simp only [← cast_pow] exact summable_norm_mul_geometric_of_norm_lt_one (k := k) (u := fun n ↦ n ^ k) hr (isBigO_refl _ _) -theorem summable_norm_geometric_of_norm_lt_one {R : Type*} [NormedRing R] {r : R} +theorem summable_norm_geometric_of_norm_lt_one {r : R} (hr : β€–rβ€– < 1) : Summable fun n : β„• ↦ β€–(r ^ n : R)β€– := by simpa using summable_norm_pow_mul_geometric_of_norm_lt_one 0 hr -@[deprecated (since := "2024-01-31")] -alias summable_norm_pow_mul_geometric_of_norm_lt_1 := summable_norm_pow_mul_geometric_of_norm_lt_one - -variable {π•œ : Type*} [NormedDivisionRing π•œ] +variable [HasSummableGeomSeries R] -/-- The sum of `(n+k).choose k * r^n` is `1/(1-r)^{k+1}`. -See also `PowerSeries.invOneSubPow_val_eq_mk_choose_add` for the corresponding statement in formal -power series, without summability arguments. -/ -lemma hasSum_choose_mul_geometric_of_norm_lt_one - (k : β„•) {r : π•œ} (hr : β€–rβ€– < 1) : - HasSum (fun n ↦ (n + k).choose k * r ^ n) (1 / (1 - r) ^ (k + 1)) := by +lemma hasSum_choose_mul_geometric_of_norm_lt_one' + (k : β„•) {r : R} (hr : β€–rβ€– < 1) : + HasSum (fun n ↦ (n + k).choose k * r ^ n) (Ring.inverse (1 - r) ^ (k + 1)) := by induction k with - | zero => simpa using hasSum_geometric_of_norm_lt_one hr + | zero => simpa using hasSum_geom_series_inverse r hr | succ k ih => have I1 : Summable (fun (n : β„•) ↦ β€–(n + k).choose k * r ^ nβ€–) := by apply summable_norm_mul_geometric_of_norm_lt_one (k := k) hr @@ -378,34 +475,42 @@ lemma hasSum_choose_mul_geometric_of_norm_lt_one _ ≀ (2 * n) ^ k := Nat.choose_le_pow _ _ _ = 2 ^ k * n ^ k := Nat.mul_pow 2 n k convert hasSum_sum_range_mul_of_summable_norm' I1 ih.summable - (summable_norm_geometric_of_norm_lt_one hr) (summable_geometric_of_norm_lt_one hr) using 1 - Β· ext n - have : βˆ‘ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) = + (summable_norm_geometric_of_norm_lt_one hr) (summable_geometric_of_norm_lt_one hr) with n + Β· have : βˆ‘ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) = βˆ‘ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ n := by apply Finset.sum_congr rfl (fun i hi ↦ ?_) simp only [Finset.mem_range] at hi rw [mul_assoc, ← pow_add, show i + (n - i) = n by omega] - simp_rw [this, ← sum_mul, ← Nat.cast_sum, sum_range_add_choose n k, add_assoc] - Β· rw [ih.tsum_eq, (hasSum_geometric_of_norm_lt_one hr).tsum_eq, pow_succ] - simp only [one_div, ← mul_inv_rev, ← pow_succ, ← _root_.pow_succ'] + simp [this, ← sum_mul, ← Nat.cast_sum, sum_range_add_choose n k, add_assoc] + Β· rw [ih.tsum_eq, (hasSum_geom_series_inverse r hr).tsum_eq, pow_succ] -lemma summable_choose_mul_geometric_of_norm_lt_one (k : β„•) {r : π•œ} (hr : β€–rβ€– < 1) : +lemma summable_choose_mul_geometric_of_norm_lt_one (k : β„•) {r : R} (hr : β€–rβ€– < 1) : Summable (fun n ↦ (n + k).choose k * r ^ n) := - (hasSum_choose_mul_geometric_of_norm_lt_one k hr).summable + (hasSum_choose_mul_geometric_of_norm_lt_one' k hr).summable + +lemma tsum_choose_mul_geometric_of_norm_lt_one' (k : β„•) {r : R} (hr : β€–rβ€– < 1) : + βˆ‘' n, (n + k).choose k * r ^ n = (Ring.inverse (1 - r)) ^ (k + 1) := + (hasSum_choose_mul_geometric_of_norm_lt_one' k hr).tsum_eq + +lemma hasSum_choose_mul_geometric_of_norm_lt_one + (k : β„•) {r : π•œ} (hr : β€–rβ€– < 1) : + HasSum (fun n ↦ (n + k).choose k * r ^ n) (1 / (1 - r) ^ (k + 1)) := by + convert hasSum_choose_mul_geometric_of_norm_lt_one' k hr + simp lemma tsum_choose_mul_geometric_of_norm_lt_one (k : β„•) {r : π•œ} (hr : β€–rβ€– < 1) : - βˆ‘' n, (n + k).choose k * r ^ n = 1 / (1 - r) ^ (k + 1) := + βˆ‘' n, (n + k).choose k * r ^ n = 1/ (1 - r) ^ (k + 1) := (hasSum_choose_mul_geometric_of_norm_lt_one k hr).tsum_eq -lemma summable_descFactorial_mul_geometric_of_norm_lt_one (k : β„•) {r : π•œ} (hr : β€–rβ€– < 1) : +lemma summable_descFactorial_mul_geometric_of_norm_lt_one (k : β„•) {r : R} (hr : β€–rβ€– < 1) : Summable (fun n ↦ (n + k).descFactorial k * r ^ n) := by - convert (summable_choose_mul_geometric_of_norm_lt_one k hr).mul_left (k.factorial : π•œ) + convert (summable_choose_mul_geometric_of_norm_lt_one k hr).mul_left (k.factorial : R) using 2 with n simp [← mul_assoc, descFactorial_eq_factorial_mul_choose (n + k) k] open Polynomial in -theorem summable_pow_mul_geometric_of_norm_lt_one (k : β„•) {r : π•œ} (hr : β€–rβ€– < 1) : - Summable (fun n ↦ (n : π•œ) ^ k * r ^ n : β„• β†’ π•œ) := by +theorem summable_pow_mul_geometric_of_norm_lt_one (k : β„•) {r : R} (hr : β€–rβ€– < 1) : + Summable (fun n ↦ (n : R) ^ k * r ^ n : β„• β†’ R) := by refine Nat.strong_induction_on k fun k hk => ?_ obtain ⟨a, ha⟩ : βˆƒ (a : β„• β†’ β„•), βˆ€ n, (n + k).descFactorial k = n ^ k + βˆ‘ i ∈ range k, a i * n ^ i := by @@ -430,37 +535,50 @@ theorem summable_pow_mul_geometric_of_norm_lt_one (k : β„•) {r : π•œ} (hr : β€– ext n simp [ha n, add_mul, sum_mul] +@[deprecated (since := "2024-01-31")] +alias summable_norm_pow_mul_geometric_of_norm_lt_1 := summable_norm_pow_mul_geometric_of_norm_lt_one + @[deprecated (since := "2024-01-31")] alias summable_pow_mul_geometric_of_norm_lt_1 := summable_pow_mul_geometric_of_norm_lt_one -/-- If `β€–rβ€– < 1`, then `βˆ‘' n : β„•, n * r ^ n = r / (1 - r) ^ 2`, `HasSum` version. -/ -theorem hasSum_coe_mul_geometric_of_norm_lt_one - {r : π•œ} (hr : β€–rβ€– < 1) : HasSum (fun n ↦ n * r ^ n : β„• β†’ π•œ) (r / (1 - r) ^ 2) := by - have A : HasSum (fun (n : β„•) ↦ (n + 1) * r ^ n) (1 / (1 - r) ^ 2) := by - convert hasSum_choose_mul_geometric_of_norm_lt_one 1 hr with n +/-- If `β€–rβ€– < 1`, then `βˆ‘' n : β„•, n * r ^ n = r / (1 - r) ^ 2`, `HasSum` version in a general ring +with summable geometric series. For a version in a field, using division instead of `Ring.inverse`, +see `hasSum_coe_mul_geometric_of_norm_lt_one`. -/ +theorem hasSum_coe_mul_geometric_of_norm_lt_one' + {x : R} (h : β€–xβ€– < 1) : + HasSum (fun n ↦ n * x ^ n : β„• β†’ R) (x * (Ring.inverse (1 - x)) ^ 2) := by + have A : HasSum (fun (n : β„•) ↦ (n + 1) * x ^ n) (Ring.inverse (1 - x) ^ 2) := by + convert hasSum_choose_mul_geometric_of_norm_lt_one' 1 h with n simp - have B : HasSum (fun (n : β„•) ↦ r ^ n) ((1 - r) ⁻¹) := hasSum_geometric_of_norm_lt_one hr + have B : HasSum (fun (n : β„•) ↦ x ^ n) (Ring.inverse (1 - x)) := hasSum_geom_series_inverse x h convert A.sub B using 1 Β· ext n simp [add_mul] Β· symm - calc 1 / (1 - r) ^ 2 - (1 - r) ⁻¹ - _ = 1 / (1 - r) ^ 2 - ((1 - r) * (1 - r) ⁻¹) * (1 - r) ⁻¹ := by - rw [mul_inv_cancelβ‚€, one_mul] - intro h - simp only [sub_eq_zero] at h - simp [← h] at hr - _ = r / (1 - r) ^ 2 := by - simp only [one_div, mul_assoc, ← mul_inv_rev] - rw [inv_eq_one_div, inv_eq_one_div, ← pow_two, _root_.sub_mul, one_mul, mul_div, mul_one] - abel + calc Ring.inverse (1 - x) ^ 2 - Ring.inverse (1 - x) + _ = Ring.inverse (1 - x) ^ 2 - ((1 - x) * Ring.inverse (1 - x)) * Ring.inverse (1 - x) := by + simp [Ring.mul_inverse_cancel (1 - x) (isUnit_one_sub_of_norm_lt_one h)] + _ = x * Ring.inverse (1 - x) ^ 2 := by noncomm_ring + +/-- If `β€–rβ€– < 1`, then `βˆ‘' n : β„•, n * r ^ n = r / (1 - r) ^ 2`, version in a general ring with +summable geometric series. For a version in a field, using division instead of `Ring.inverse`, +see `tsum_coe_mul_geometric_of_norm_lt_one`. -/ +theorem tsum_coe_mul_geometric_of_norm_lt_one' + {r : π•œ} (hr : β€–rβ€– < 1) : (βˆ‘' n : β„•, n * r ^ n : π•œ) = r * Ring.inverse (1 - r) ^ 2 := + (hasSum_coe_mul_geometric_of_norm_lt_one' hr).tsum_eq + +/-- If `β€–rβ€– < 1`, then `βˆ‘' n : β„•, n * r ^ n = r / (1 - r) ^ 2`, `HasSum` version. -/ +theorem hasSum_coe_mul_geometric_of_norm_lt_one {r : π•œ} (hr : β€–rβ€– < 1) : + HasSum (fun n ↦ n * r ^ n : β„• β†’ π•œ) (r / (1 - r) ^ 2) := by + convert hasSum_coe_mul_geometric_of_norm_lt_one' hr using 1 + simp [div_eq_mul_inv] @[deprecated (since := "2024-01-31")] alias hasSum_coe_mul_geometric_of_norm_lt_1 := hasSum_coe_mul_geometric_of_norm_lt_one /-- If `β€–rβ€– < 1`, then `βˆ‘' n : β„•, n * r ^ n = r / (1 - r) ^ 2`. -/ -theorem tsum_coe_mul_geometric_of_norm_lt_one - {r : π•œ} (hr : β€–rβ€– < 1) : (βˆ‘' n : β„•, n * r ^ n : π•œ) = r / (1 - r) ^ 2 := +theorem tsum_coe_mul_geometric_of_norm_lt_one {r : π•œ} (hr : β€–rβ€– < 1) : + (βˆ‘' n : β„•, n * r ^ n : π•œ) = r / (1 - r) ^ 2 := (hasSum_coe_mul_geometric_of_norm_lt_one hr).tsum_eq @[deprecated (since := "2024-01-31")] @@ -544,67 +662,6 @@ lemma exists_norm_le_of_cauchySeq (h : CauchySeq fun n ↦ βˆ‘ k ∈ range n, f end SummableLeGeometric -section NormedRingGeometric - -variable {R : Type*} [NormedRing R] [CompleteSpace R] - -open NormedSpace - -/-- A geometric series in a complete normed ring is summable. -Proved above (same name, different namespace) for not-necessarily-complete normed fields. -/ -theorem NormedRing.summable_geometric_of_norm_lt_one (x : R) (h : β€–xβ€– < 1) : - Summable fun n : β„• ↦ x ^ n := - have h1 : Summable fun n : β„• ↦ β€–xβ€– ^ n := summable_geometric_of_lt_one (norm_nonneg _) h - h1.of_norm_bounded_eventually_nat _ (eventually_norm_pow_le x) -@[deprecated (since := "2024-01-31")] -alias NormedRing.summable_geometric_of_norm_lt_1 := NormedRing.summable_geometric_of_norm_lt_one - -/-- Bound for the sum of a geometric series in a normed ring. This formula does not assume that the -normed ring satisfies the axiom `β€–1β€– = 1`. -/ -theorem NormedRing.tsum_geometric_of_norm_lt_one (x : R) (h : β€–xβ€– < 1) : - β€–βˆ‘' n : β„•, x ^ nβ€– ≀ β€–(1 : R)β€– - 1 + (1 - β€–xβ€–)⁻¹ := by - rw [tsum_eq_zero_add (summable_geometric_of_norm_lt_one x h)] - simp only [_root_.pow_zero] - refine le_trans (norm_add_le _ _) ?_ - have : β€–βˆ‘' b : β„•, (fun n ↦ x ^ (n + 1)) bβ€– ≀ (1 - β€–xβ€–)⁻¹ - 1 := by - refine tsum_of_norm_bounded ?_ fun b ↦ norm_pow_le' _ (Nat.succ_pos b) - convert (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h) - simp - linarith - -@[deprecated (since := "2024-01-31")] -alias NormedRing.tsum_geometric_of_norm_lt_1 := NormedRing.tsum_geometric_of_norm_lt_one - -theorem geom_series_mul_neg (x : R) (h : β€–xβ€– < 1) : (βˆ‘' i : β„•, x ^ i) * (1 - x) = 1 := by - have := (NormedRing.summable_geometric_of_norm_lt_one x h).hasSum.mul_right (1 - x) - refine tendsto_nhds_unique this.tendsto_sum_nat ?_ - have : Tendsto (fun n : β„• ↦ 1 - x ^ n) atTop (𝓝 1) := by - simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h) - convert← this - rw [← geom_sum_mul_neg, Finset.sum_mul] - -theorem mul_neg_geom_series (x : R) (h : β€–xβ€– < 1) : ((1 - x) * βˆ‘' i : β„•, x ^ i) = 1 := by - have := (NormedRing.summable_geometric_of_norm_lt_one x h).hasSum.mul_left (1 - x) - refine tendsto_nhds_unique this.tendsto_sum_nat ?_ - have : Tendsto (fun n : β„• ↦ 1 - x ^ n) atTop (𝓝 1) := by - simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h) - convert← this - rw [← mul_neg_geom_sum, Finset.mul_sum] - -theorem geom_series_succ (x : R) (h : β€–xβ€– < 1) : βˆ‘' i : β„•, x ^ (i + 1) = βˆ‘' i : β„•, x ^ i - 1 := by - rw [eq_sub_iff_add_eq, tsum_eq_zero_add (NormedRing.summable_geometric_of_norm_lt_one x h), - pow_zero, add_comm] - -theorem geom_series_mul_shift (x : R) (h : β€–xβ€– < 1) : - x * βˆ‘' i : β„•, x ^ i = βˆ‘' i : β„•, x ^ (i + 1) := by - simp_rw [← (NormedRing.summable_geometric_of_norm_lt_one _ h).tsum_mul_left, ← _root_.pow_succ'] - -theorem geom_series_mul_one_add (x : R) (h : β€–xβ€– < 1) : - (1 + x) * βˆ‘' i : β„•, x ^ i = 2 * βˆ‘' i : β„•, x ^ i - 1 := by - rw [add_mul, one_mul, geom_series_mul_shift x h, geom_series_succ x h, two_mul, add_sub_assoc] - -end NormedRingGeometric - /-! ### Summability tests based on comparison with geometric series -/ theorem summable_of_ratio_norm_eventually_le {Ξ± : Type*} [SeminormedAddCommGroup Ξ±] diff --git a/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean b/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean index 9395e10f0cc6f..df6dd1f46c15f 100644 --- a/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean +++ b/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean @@ -397,7 +397,7 @@ theorem differentiableAt_Ξ› {s : β„‚} (hs : s β‰  0 ∨ P.fβ‚€ = 0) (hs' : s β‰  DifferentiableAt β„‚ P.Ξ› s := by refine ((P.differentiable_Ξ›β‚€ s).sub ?_).sub ?_ Β· rcases hs with hs | hs - Β· simpa only [one_div] using (differentiableAt_inv' hs).smul_const P.fβ‚€ + Β· simpa only [one_div] using (differentiableAt_inv hs).smul_const P.fβ‚€ Β· simpa only [hs, smul_zero] using differentiableAt_const (0 : E) Β· rcases hs' with hs' | hs' Β· apply DifferentiableAt.smul_const diff --git a/Mathlib/Tactic/FunProp/Differentiable.lean b/Mathlib/Tactic/FunProp/Differentiable.lean index 5e20116dd53ac..1d81eec7d76f2 100644 --- a/Mathlib/Tactic/FunProp/Differentiable.lean +++ b/Mathlib/Tactic/FunProp/Differentiable.lean @@ -104,7 +104,6 @@ attribute [fun_prop] Differentiable.mul Differentiable.smul Differentiable.div - Differentiable.inv' Differentiable.inv DifferentiableAt.add @@ -113,7 +112,6 @@ attribute [fun_prop] DifferentiableAt.mul DifferentiableAt.smul DifferentiableAt.div - DifferentiableAt.inv' DifferentiableAt.inv DifferentiableOn.add @@ -122,7 +120,6 @@ attribute [fun_prop] DifferentiableOn.mul DifferentiableOn.smul DifferentiableOn.div - DifferentiableOn.inv' DifferentiableOn.inv