From 5267b9d04b777c225d30806ddcebefb379f695b8 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Tue, 6 Jun 2023 11:20:36 +0800 Subject: [PATCH 1/4] feat: port Analysis.SpecialFunctions.Exponential From c6e1aefe7a22a1a97737c1afa5d5c85bd040bfb8 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Tue, 6 Jun 2023 11:20:36 +0800 Subject: [PATCH 2/4] Initial file copy from mathport --- .../SpecialFunctions/Exponential.lean | 451 ++++++++++++++++++ 1 file changed, 451 insertions(+) create mode 100644 Mathlib/Analysis/SpecialFunctions/Exponential.lean diff --git a/Mathlib/Analysis/SpecialFunctions/Exponential.lean b/Mathlib/Analysis/SpecialFunctions/Exponential.lean new file mode 100644 index 0000000000000..33eb795b3fd2e --- /dev/null +++ b/Mathlib/Analysis/SpecialFunctions/Exponential.lean @@ -0,0 +1,451 @@ +/- +Copyright (c) 2021 Anatole Dedecker. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anatole Dedecker, Eric Wieser + +! This file was ported from Lean 3 source module analysis.special_functions.exponential +! leanprover-community/mathlib commit e1a18cad9cd462973d760af7de36b05776b8811c +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.Analysis.NormedSpace.Exponential +import Mathbin.Analysis.Calculus.FderivAnalytic +import Mathbin.Topology.MetricSpace.CauSeqFilter + +/-! +# Calculus results on exponential in a Banach algebra + +In this file, we prove basic properties about the derivative of the exponential map `exp 𝕂` +in a Banach algebra `𝔸` over a field `𝕂`. We keep them separate from the main file +`analysis/normed_space/exponential` in order to minimize dependencies. + +## Main results + +We prove most result for an arbitrary field `𝕂`, and then specialize to `𝕂 = ℝ` or `𝕂 = β„‚`. + +### General case + +- `has_strict_fderiv_at_exp_zero_of_radius_pos` : `exp 𝕂` has strict FrΓ©chet-derivative + `1 : 𝔸 β†’L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero + (see also `has_strict_deriv_at_exp_zero_of_radius_pos` for the case `𝔸 = 𝕂`) +- `has_strict_fderiv_at_exp_of_lt_radius` : if `𝕂` has characteristic zero and `𝔸` is commutative, + then given a point `x` in the disk of convergence, `exp 𝕂` has strict FrΓ©chet-derivative + `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at x (see also `has_strict_deriv_at_exp_of_lt_radius` for the case + `𝔸 = 𝕂`) +- `has_strict_fderiv_at_exp_smul_const_of_mem_ball`: even when `𝔸` is non-commutative, if we have + an intermediate algebra `π•Š` which is commutative, then the function `(u : π•Š) ↦ exp 𝕂 (u β€’ x)`, + still has strict FrΓ©chet-derivative `exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x` at `t` if + `t β€’ x` is in the radius of convergence. + +### `𝕂 = ℝ` or `𝕂 = β„‚` + +- `has_strict_fderiv_at_exp_zero` : `exp 𝕂` has strict FrΓ©chet-derivative `1 : 𝔸 β†’L[𝕂] 𝔸` at zero + (see also `has_strict_deriv_at_exp_zero` for the case `𝔸 = 𝕂`) +- `has_strict_fderiv_at_exp` : if `𝔸` is commutative, then given any point `x`, `exp 𝕂` has strict + FrΓ©chet-derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at x (see also `has_strict_deriv_at_exp` for the + case `𝔸 = 𝕂`) +- `has_strict_fderiv_at_exp_smul_const`: even when `𝔸` is non-commutative, if we have + an intermediate algebra `π•Š` which is commutative, then the function `(u : π•Š) ↦ exp 𝕂 (u β€’ x)` + still has strict FrΓ©chet-derivative `exp 𝕂 (t β€’ x) β€’ (1 : 𝔸 β†’L[𝕂] 𝔸).smul_right x` at `t`. + +### Compatibilty with `real.exp` and `complex.exp` + +- `complex.exp_eq_exp_β„‚` : `complex.exp = exp β„‚ β„‚` +- `real.exp_eq_exp_ℝ` : `real.exp = exp ℝ ℝ` + +-/ + + +open Filter IsROrC ContinuousMultilinearMap NormedField Asymptotics + +open scoped Nat Topology BigOperators ENNReal + +section AnyFieldAnyAlgebra + +variable {𝕂 𝔸 : Type _} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] + [CompleteSpace 𝔸] + +/-- The exponential in a Banach-algebra `𝔸` over a normed field `𝕂` has strict FrΓ©chet-derivative +`1 : 𝔸 β†’L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero. -/ +theorem hasStrictFDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝔸).radius) : + HasStrictFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) 0 := + by + convert (hasFPowerSeriesAt_exp_zero_of_radius_pos h).HasStrictFDerivAt + ext x + change x = expSeries 𝕂 𝔸 1 fun _ => x + simp [expSeries_apply_eq] +#align has_strict_fderiv_at_exp_zero_of_radius_pos hasStrictFDerivAt_exp_zero_of_radius_pos + +/-- The exponential in a Banach-algebra `𝔸` over a normed field `𝕂` has FrΓ©chet-derivative +`1 : 𝔸 β†’L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero. -/ +theorem hasFDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝔸).radius) : + HasFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) 0 := + (hasStrictFDerivAt_exp_zero_of_radius_pos h).HasFDerivAt +#align has_fderiv_at_exp_zero_of_radius_pos hasFDerivAt_exp_zero_of_radius_pos + +end AnyFieldAnyAlgebra + +section AnyFieldCommAlgebra + +variable {𝕂 𝔸 : Type _} [NontriviallyNormedField 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] + [CompleteSpace 𝔸] + +/-- The exponential map in a commutative Banach-algebra `𝔸` over a normed field `𝕂` of +characteristic zero has FrΓ©chet-derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at any point `x` in the +disk of convergence. -/ +theorem hasFDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸} + (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : + HasFDerivAt (exp 𝕂) (exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸) x := + by + have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt hx + rw [hasFDerivAt_iff_isLittleO_nhds_zero] + suffices + (fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - ContinuousLinearMap.id 𝕂 𝔸 h)) =αΆ [𝓝 0] fun h => + exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x β€’ ContinuousLinearMap.id 𝕂 𝔸 h + by + refine' (is_o.const_mul_left _ _).congr' this (eventually_eq.refl _ _) + rw [← hasFDerivAt_iff_isLittleO_nhds_zero] + exact hasFDerivAt_exp_zero_of_radius_pos hpos + have : βˆ€αΆ  h in 𝓝 (0 : 𝔸), h ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := + EMetric.ball_mem_nhds _ hpos + filter_upwards [this] with _ hh + rw [exp_add_of_mem_ball hx hh, exp_zero, zero_add, ContinuousLinearMap.id_apply, smul_eq_mul] + ring +#align has_fderiv_at_exp_of_mem_ball hasFDerivAt_exp_of_mem_ball + +/-- The exponential map in a commutative Banach-algebra `𝔸` over a normed field `𝕂` of +characteristic zero has strict FrΓ©chet-derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at any point `x` in +the disk of convergence. -/ +theorem hasStrictFDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸} + (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : + HasStrictFDerivAt (exp 𝕂) (exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸) x := + let ⟨p, hp⟩ := analyticAt_exp_of_mem_ball x hx + hp.HasFDerivAt.unique (hasFDerivAt_exp_of_mem_ball hx) β–Έ hp.HasStrictFDerivAt +#align has_strict_fderiv_at_exp_of_mem_ball hasStrictFDerivAt_exp_of_mem_ball + +end AnyFieldCommAlgebra + +section deriv + +variable {𝕂 : Type _} [NontriviallyNormedField 𝕂] [CompleteSpace 𝕂] + +/-- The exponential map in a complete normed field `𝕂` of characteristic zero has strict derivative +`exp 𝕂 x` at any point `x` in the disk of convergence. -/ +theorem hasStrictDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝕂} + (hx : x ∈ EMetric.ball (0 : 𝕂) (expSeries 𝕂 𝕂).radius) : HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x := + by simpa using (hasStrictFDerivAt_exp_of_mem_ball hx).HasStrictDerivAt +#align has_strict_deriv_at_exp_of_mem_ball hasStrictDerivAt_exp_of_mem_ball + +/-- The exponential map in a complete normed field `𝕂` of characteristic zero has derivative +`exp 𝕂 x` at any point `x` in the disk of convergence. -/ +theorem hasDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝕂} + (hx : x ∈ EMetric.ball (0 : 𝕂) (expSeries 𝕂 𝕂).radius) : HasDerivAt (exp 𝕂) (exp 𝕂 x) x := + (hasStrictDerivAt_exp_of_mem_ball hx).HasDerivAt +#align has_deriv_at_exp_of_mem_ball hasDerivAt_exp_of_mem_ball + +/-- The exponential map in a complete normed field `𝕂` of characteristic zero has strict derivative +`1` at zero, as long as it converges on a neighborhood of zero. -/ +theorem hasStrictDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝕂).radius) : + HasStrictDerivAt (exp 𝕂) (1 : 𝕂) 0 := + (hasStrictFDerivAt_exp_zero_of_radius_pos h).HasStrictDerivAt +#align has_strict_deriv_at_exp_zero_of_radius_pos hasStrictDerivAt_exp_zero_of_radius_pos + +/-- The exponential map in a complete normed field `𝕂` of characteristic zero has derivative +`1` at zero, as long as it converges on a neighborhood of zero. -/ +theorem hasDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝕂).radius) : + HasDerivAt (exp 𝕂) (1 : 𝕂) 0 := + (hasStrictDerivAt_exp_zero_of_radius_pos h).HasDerivAt +#align has_deriv_at_exp_zero_of_radius_pos hasDerivAt_exp_zero_of_radius_pos + +end deriv + +section IsROrCAnyAlgebra + +variable {𝕂 𝔸 : Type _} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] + +/-- The exponential in a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = β„‚` has strict FrΓ©chet-derivative +`1 : 𝔸 β†’L[𝕂] 𝔸` at zero. -/ +theorem hasStrictFDerivAt_exp_zero : HasStrictFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) 0 := + hasStrictFDerivAt_exp_zero_of_radius_pos (expSeries_radius_pos 𝕂 𝔸) +#align has_strict_fderiv_at_exp_zero hasStrictFDerivAt_exp_zero + +/-- The exponential in a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = β„‚` has FrΓ©chet-derivative +`1 : 𝔸 β†’L[𝕂] 𝔸` at zero. -/ +theorem hasFDerivAt_exp_zero : HasFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) 0 := + hasStrictFDerivAt_exp_zero.HasFDerivAt +#align has_fderiv_at_exp_zero hasFDerivAt_exp_zero + +end IsROrCAnyAlgebra + +section IsROrCCommAlgebra + +variable {𝕂 𝔸 : Type _} [IsROrC 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] + +/-- The exponential map in a commutative Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = β„‚` has strict +FrΓ©chet-derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at any point `x`. -/ +theorem hasStrictFDerivAt_exp {x : 𝔸} : HasStrictFDerivAt (exp 𝕂) (exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸) x := + hasStrictFDerivAt_exp_of_mem_ball ((expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _) +#align has_strict_fderiv_at_exp hasStrictFDerivAt_exp + +/-- The exponential map in a commutative Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = β„‚` has +FrΓ©chet-derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at any point `x`. -/ +theorem hasFDerivAt_exp {x : 𝔸} : HasFDerivAt (exp 𝕂) (exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸) x := + hasStrictFDerivAt_exp.HasFDerivAt +#align has_fderiv_at_exp hasFDerivAt_exp + +end IsROrCCommAlgebra + +section DerivROrC + +variable {𝕂 : Type _} [IsROrC 𝕂] + +/-- The exponential map in `𝕂 = ℝ` or `𝕂 = β„‚` has strict derivative `exp 𝕂 x` at any point +`x`. -/ +theorem hasStrictDerivAt_exp {x : 𝕂} : HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x := + hasStrictDerivAt_exp_of_mem_ball ((expSeries_radius_eq_top 𝕂 𝕂).symm β–Έ edist_lt_top _ _) +#align has_strict_deriv_at_exp hasStrictDerivAt_exp + +/-- The exponential map in `𝕂 = ℝ` or `𝕂 = β„‚` has derivative `exp 𝕂 x` at any point `x`. -/ +theorem hasDerivAt_exp {x : 𝕂} : HasDerivAt (exp 𝕂) (exp 𝕂 x) x := + hasStrictDerivAt_exp.HasDerivAt +#align has_deriv_at_exp hasDerivAt_exp + +/-- The exponential map in `𝕂 = ℝ` or `𝕂 = β„‚` has strict derivative `1` at zero. -/ +theorem hasStrictDerivAt_exp_zero : HasStrictDerivAt (exp 𝕂) (1 : 𝕂) 0 := + hasStrictDerivAt_exp_zero_of_radius_pos (expSeries_radius_pos 𝕂 𝕂) +#align has_strict_deriv_at_exp_zero hasStrictDerivAt_exp_zero + +/-- The exponential map in `𝕂 = ℝ` or `𝕂 = β„‚` has derivative `1` at zero. -/ +theorem hasDerivAt_exp_zero : HasDerivAt (exp 𝕂) (1 : 𝕂) 0 := + hasStrictDerivAt_exp_zero.HasDerivAt +#align has_deriv_at_exp_zero hasDerivAt_exp_zero + +end DerivROrC + +theorem Complex.exp_eq_exp_β„‚ : Complex.exp = exp β„‚ := + by + refine' funext fun x => _ + rw [Complex.exp, exp_eq_tsum_div] + exact tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable ℝ x).HasSum.tendsto_sum_nat +#align complex.exp_eq_exp_β„‚ Complex.exp_eq_exp_β„‚ + +theorem Real.exp_eq_exp_ℝ : Real.exp = exp ℝ := by ext x; + exact_mod_cast congr_fun Complex.exp_eq_exp_β„‚ x +#align real.exp_eq_exp_ℝ Real.exp_eq_exp_ℝ + +/-! ### Derivative of $\exp (ux)$ by $u$ + +Note that since for `x : 𝔸` we have `normed_ring 𝔸` not `normed_comm_ring 𝔸`, we cannot deduce +these results from `has_fderiv_at_exp_of_mem_ball` applied to the algebra `𝔸`. + +One possible solution for that would be to apply `has_fderiv_at_exp_of_mem_ball` to the +commutative algebra `algebra.elemental_algebra π•Š x`. Unfortunately we don't have all the required +API, so we leave that to a future refactor (see leanprover-community/mathlib#19062 for discussion). + +We could also go the other way around and deduce `has_fderiv_at_exp_of_mem_ball` from +`has_fderiv_at_exp_smul_const_of_mem_ball` applied to `π•Š := 𝔸`, `x := (1 : 𝔸)`, and `t := x`. +However, doing so would make the aformentioned `elemental_algebra` refactor harder, so for now we +just prove these two lemmas independently. + +A last strategy would be to deduce everything from the more general non-commutative case, +$$\frac{d}{dt}e^{x(t)} = \int_0^1 e^{sx(t)} \left(\frac{d}{dt}e^{x(t)}\right) e^{(1-s)x(t)} ds$$ +but this is harder to prove, and typically is shown by going via these results first. + +TODO: prove this result too! +-/ + + +section exp_smul + +variable {𝕂 π•Š 𝔸 : Type _} + +variable (𝕂) + +open scoped Topology + +open Asymptotics Filter + +section MemBall + +variable [NontriviallyNormedField 𝕂] [CharZero 𝕂] + +variable [NormedCommRing π•Š] [NormedRing 𝔸] + +variable [NormedSpace 𝕂 π•Š] [NormedAlgebra 𝕂 𝔸] [Algebra π•Š 𝔸] [ContinuousSMul π•Š 𝔸] + +variable [IsScalarTower 𝕂 π•Š 𝔸] + +variable [CompleteSpace 𝔸] + +theorem hasFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : π•Š) + (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : + HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) t := + by + -- TODO: prove this via `has_fderiv_at_exp_of_mem_ball` using the commutative ring + -- `algebra.elemental_algebra π•Š x`. See leanprover-community/mathlib#19062 for discussion. + have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt htx + rw [hasFDerivAt_iff_isLittleO_nhds_zero] + suffices + (fun h => + exp 𝕂 (t β€’ x) * + (exp 𝕂 ((0 + h) β€’ x) - exp 𝕂 ((0 : π•Š) β€’ x) - ((1 : π•Š β†’L[𝕂] π•Š).smul_right x) h)) =αΆ [𝓝 0] + fun h => + exp 𝕂 ((t + h) β€’ x) - exp 𝕂 (t β€’ x) - (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) h + by + refine' (is_o.const_mul_left _ _).congr' this (eventually_eq.refl _ _) + rw [← + @hasFDerivAt_iff_isLittleO_nhds_zero _ _ _ _ _ _ _ _ (fun u => exp 𝕂 (u β€’ x)) + ((1 : π•Š β†’L[𝕂] π•Š).smul_right x) 0] + have : HasFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) ((1 : π•Š β†’L[𝕂] π•Š).smul_right x 0) := + by + rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul] + exact hasFDerivAt_exp_zero_of_radius_pos hpos + exact this.comp 0 ((1 : π•Š β†’L[𝕂] π•Š).smul_right x).HasFDerivAt + have : tendsto (fun h : π•Š => h β€’ x) (𝓝 0) (𝓝 0) := + by + rw [← zero_smul π•Š x] + exact tendsto_id.smul_const x + have : βˆ€αΆ  h in 𝓝 (0 : π•Š), h β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := + this.eventually (EMetric.ball_mem_nhds _ hpos) + filter_upwards [this] + intro h hh + have : Commute (t β€’ x) (h β€’ x) := ((Commute.refl x).smul_left t).smul_right h + rw [add_smul t h, exp_add_of_commute_of_mem_ball this htx hh, zero_add, zero_smul, exp_zero, + ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, + ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply, + ContinuousLinearMap.one_apply, smul_eq_mul, mul_sub_left_distrib, mul_sub_left_distrib, mul_one] +#align has_fderiv_at_exp_smul_const_of_mem_ball hasFDerivAt_exp_smul_const_of_mem_ball + +theorem hasFDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : π•Š) + (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : + HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) + (((1 : π•Š β†’L[𝕂] π•Š).smul_right x).smul_right (exp 𝕂 (t β€’ x))) t := + by + convert hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1 + ext t' + show Commute (t' β€’ x) (exp 𝕂 (t β€’ x)) + exact (((Commute.refl x).smul_left t').smul_right t).exp_right 𝕂 +#align has_fderiv_at_exp_smul_const_of_mem_ball' hasFDerivAt_exp_smul_const_of_mem_ball' + +theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : π•Š) + (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : + HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) + t := + let ⟨p, hp⟩ := analyticAt_exp_of_mem_ball (t β€’ x) htx + have deriv₁ : HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) _ t := + hp.HasStrictFDerivAt.comp t ((ContinuousLinearMap.id 𝕂 π•Š).smul_right x).HasStrictFDerivAt + have derivβ‚‚ : HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) _ t := + hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx + deriv₁.HasFDerivAt.unique derivβ‚‚ β–Έ deriv₁ +#align has_strict_fderiv_at_exp_smul_const_of_mem_ball hasStrictFDerivAt_exp_smul_const_of_mem_ball + +theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : π•Š) + (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : + HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) + (((1 : π•Š β†’L[𝕂] π•Š).smul_right x).smul_right (exp 𝕂 (t β€’ x))) t := + by + let ⟨p, hp⟩ := analyticAt_exp_of_mem_ball (t β€’ x) htx + convert hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1 + ext t' + show Commute (t' β€’ x) (exp 𝕂 (t β€’ x)) + exact (((Commute.refl x).smul_left t').smul_right t).exp_right 𝕂 +#align has_strict_fderiv_at_exp_smul_const_of_mem_ball' hasStrictFDerivAt_exp_smul_const_of_mem_ball' + +variable {𝕂} + +theorem hasStrictDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕂) + (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : + HasStrictDerivAt (fun u : 𝕂 => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) * x) t := by + simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx).HasStrictDerivAt +#align has_strict_deriv_at_exp_smul_const_of_mem_ball hasStrictDerivAt_exp_smul_const_of_mem_ball + +theorem hasStrictDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : 𝕂) + (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : + HasStrictDerivAt (fun u : 𝕂 => exp 𝕂 (u β€’ x)) (x * exp 𝕂 (t β€’ x)) t := by + simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball' 𝕂 x t htx).HasStrictDerivAt +#align has_strict_deriv_at_exp_smul_const_of_mem_ball' hasStrictDerivAt_exp_smul_const_of_mem_ball' + +theorem hasDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕂) + (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : + HasDerivAt (fun u : 𝕂 => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) * x) t := + (hasStrictDerivAt_exp_smul_const_of_mem_ball x t htx).HasDerivAt +#align has_deriv_at_exp_smul_const_of_mem_ball hasDerivAt_exp_smul_const_of_mem_ball + +theorem hasDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : 𝕂) + (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : + HasDerivAt (fun u : 𝕂 => exp 𝕂 (u β€’ x)) (x * exp 𝕂 (t β€’ x)) t := + (hasStrictDerivAt_exp_smul_const_of_mem_ball' x t htx).HasDerivAt +#align has_deriv_at_exp_smul_const_of_mem_ball' hasDerivAt_exp_smul_const_of_mem_ball' + +end MemBall + +section IsROrC + +variable [IsROrC 𝕂] + +variable [NormedCommRing π•Š] [NormedRing 𝔸] + +variable [NormedAlgebra 𝕂 π•Š] [NormedAlgebra 𝕂 𝔸] [Algebra π•Š 𝔸] [ContinuousSMul π•Š 𝔸] + +variable [IsScalarTower 𝕂 π•Š 𝔸] + +variable [CompleteSpace 𝔸] + +variable (𝕂) + +theorem hasFDerivAt_exp_smul_const (x : 𝔸) (t : π•Š) : + HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) t := + hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ <| + (expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _ +#align has_fderiv_at_exp_smul_const hasFDerivAt_exp_smul_const + +theorem hasFDerivAt_exp_smul_const' (x : 𝔸) (t : π•Š) : + HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) + (((1 : π•Š β†’L[𝕂] π•Š).smul_right x).smul_right (exp 𝕂 (t β€’ x))) t := + hasFDerivAt_exp_smul_const_of_mem_ball' 𝕂 _ _ <| + (expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _ +#align has_fderiv_at_exp_smul_const' hasFDerivAt_exp_smul_const' + +theorem hasStrictFDerivAt_exp_smul_const (x : 𝔸) (t : π•Š) : + HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) + t := + hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ <| + (expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _ +#align has_strict_fderiv_at_exp_smul_const hasStrictFDerivAt_exp_smul_const + +theorem hasStrictFDerivAt_exp_smul_const' (x : 𝔸) (t : π•Š) : + HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) + (((1 : π•Š β†’L[𝕂] π•Š).smul_right x).smul_right (exp 𝕂 (t β€’ x))) t := + hasStrictFDerivAt_exp_smul_const_of_mem_ball' 𝕂 _ _ <| + (expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _ +#align has_strict_fderiv_at_exp_smul_const' hasStrictFDerivAt_exp_smul_const' + +variable {𝕂} + +theorem hasStrictDerivAt_exp_smul_const (x : 𝔸) (t : 𝕂) : + HasStrictDerivAt (fun u : 𝕂 => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) * x) t := + hasStrictDerivAt_exp_smul_const_of_mem_ball _ _ <| + (expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _ +#align has_strict_deriv_at_exp_smul_const hasStrictDerivAt_exp_smul_const + +theorem hasStrictDerivAt_exp_smul_const' (x : 𝔸) (t : 𝕂) : + HasStrictDerivAt (fun u : 𝕂 => exp 𝕂 (u β€’ x)) (x * exp 𝕂 (t β€’ x)) t := + hasStrictDerivAt_exp_smul_const_of_mem_ball' _ _ <| + (expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _ +#align has_strict_deriv_at_exp_smul_const' hasStrictDerivAt_exp_smul_const' + +theorem hasDerivAt_exp_smul_const (x : 𝔸) (t : 𝕂) : + HasDerivAt (fun u : 𝕂 => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) * x) t := + hasDerivAt_exp_smul_const_of_mem_ball _ _ <| (expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _ +#align has_deriv_at_exp_smul_const hasDerivAt_exp_smul_const + +theorem hasDerivAt_exp_smul_const' (x : 𝔸) (t : 𝕂) : + HasDerivAt (fun u : 𝕂 => exp 𝕂 (u β€’ x)) (x * exp 𝕂 (t β€’ x)) t := + hasDerivAt_exp_smul_const_of_mem_ball' _ _ <| + (expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _ +#align has_deriv_at_exp_smul_const' hasDerivAt_exp_smul_const' + +end IsROrC + +end exp_smul + From d0bfe18adef09517f60bbe1ff7fc521fbba58e95 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Tue, 6 Jun 2023 11:20:36 +0800 Subject: [PATCH 3/4] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + .../SpecialFunctions/Exponential.lean | 36 +++++++------------ 2 files changed, 14 insertions(+), 23 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index f42ea82e5ff3a..4d6ae6b02ca66 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -630,6 +630,7 @@ import Mathlib.Analysis.SpecialFunctions.Complex.Log import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv import Mathlib.Analysis.SpecialFunctions.Exp import Mathlib.Analysis.SpecialFunctions.ExpDeriv +import Mathlib.Analysis.SpecialFunctions.Exponential import Mathlib.Analysis.SpecialFunctions.Log.Base import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Analysis.SpecialFunctions.Log.Deriv diff --git a/Mathlib/Analysis/SpecialFunctions/Exponential.lean b/Mathlib/Analysis/SpecialFunctions/Exponential.lean index 33eb795b3fd2e..ea8808fc7229d 100644 --- a/Mathlib/Analysis/SpecialFunctions/Exponential.lean +++ b/Mathlib/Analysis/SpecialFunctions/Exponential.lean @@ -8,9 +8,9 @@ Authors: Anatole Dedecker, Eric Wieser ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.Analysis.NormedSpace.Exponential -import Mathbin.Analysis.Calculus.FderivAnalytic -import Mathbin.Topology.MetricSpace.CauSeqFilter +import Mathlib.Analysis.NormedSpace.Exponential +import Mathlib.Analysis.Calculus.FderivAnalytic +import Mathlib.Topology.MetricSpace.CauSeqFilter /-! # Calculus results on exponential in a Banach algebra @@ -68,8 +68,7 @@ variable {𝕂 𝔸 : Type _} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [ /-- The exponential in a Banach-algebra `𝔸` over a normed field `𝕂` has strict FrΓ©chet-derivative `1 : 𝔸 β†’L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero. -/ theorem hasStrictFDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝔸).radius) : - HasStrictFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) 0 := - by + HasStrictFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) 0 := by convert (hasFPowerSeriesAt_exp_zero_of_radius_pos h).HasStrictFDerivAt ext x change x = expSeries 𝕂 𝔸 1 fun _ => x @@ -95,14 +94,12 @@ characteristic zero has FrΓ©chet-derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] disk of convergence. -/ theorem hasFDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸} (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : - HasFDerivAt (exp 𝕂) (exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸) x := - by + HasFDerivAt (exp 𝕂) (exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸) x := by have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt hx rw [hasFDerivAt_iff_isLittleO_nhds_zero] suffices (fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - ContinuousLinearMap.id 𝕂 𝔸 h)) =αΆ [𝓝 0] fun h => - exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x β€’ ContinuousLinearMap.id 𝕂 𝔸 h - by + exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x β€’ ContinuousLinearMap.id 𝕂 𝔸 h by refine' (is_o.const_mul_left _ _).congr' this (eventually_eq.refl _ _) rw [← hasFDerivAt_iff_isLittleO_nhds_zero] exact hasFDerivAt_exp_zero_of_radius_pos hpos @@ -222,8 +219,7 @@ theorem hasDerivAt_exp_zero : HasDerivAt (exp 𝕂) (1 : 𝕂) 0 := end DerivROrC -theorem Complex.exp_eq_exp_β„‚ : Complex.exp = exp β„‚ := - by +theorem Complex.exp_eq_exp_β„‚ : Complex.exp = exp β„‚ := by refine' funext fun x => _ rw [Complex.exp, exp_eq_tsum_div] exact tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable ℝ x).HasSum.tendsto_sum_nat @@ -279,8 +275,7 @@ variable [CompleteSpace 𝔸] theorem hasFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : π•Š) (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : - HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) t := - by + HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) t := by -- TODO: prove this via `has_fderiv_at_exp_of_mem_ball` using the commutative ring -- `algebra.elemental_algebra π•Š x`. See leanprover-community/mathlib#19062 for discussion. have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt htx @@ -290,19 +285,16 @@ theorem hasFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : π•Š) exp 𝕂 (t β€’ x) * (exp 𝕂 ((0 + h) β€’ x) - exp 𝕂 ((0 : π•Š) β€’ x) - ((1 : π•Š β†’L[𝕂] π•Š).smul_right x) h)) =αΆ [𝓝 0] fun h => - exp 𝕂 ((t + h) β€’ x) - exp 𝕂 (t β€’ x) - (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) h - by + exp 𝕂 ((t + h) β€’ x) - exp 𝕂 (t β€’ x) - (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) h by refine' (is_o.const_mul_left _ _).congr' this (eventually_eq.refl _ _) rw [← @hasFDerivAt_iff_isLittleO_nhds_zero _ _ _ _ _ _ _ _ (fun u => exp 𝕂 (u β€’ x)) ((1 : π•Š β†’L[𝕂] π•Š).smul_right x) 0] - have : HasFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) ((1 : π•Š β†’L[𝕂] π•Š).smul_right x 0) := - by + have : HasFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) ((1 : π•Š β†’L[𝕂] π•Š).smul_right x 0) := by rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul] exact hasFDerivAt_exp_zero_of_radius_pos hpos exact this.comp 0 ((1 : π•Š β†’L[𝕂] π•Š).smul_right x).HasFDerivAt - have : tendsto (fun h : π•Š => h β€’ x) (𝓝 0) (𝓝 0) := - by + have : tendsto (fun h : π•Š => h β€’ x) (𝓝 0) (𝓝 0) := by rw [← zero_smul π•Š x] exact tendsto_id.smul_const x have : βˆ€αΆ  h in 𝓝 (0 : π•Š), h β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := @@ -319,8 +311,7 @@ theorem hasFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : π•Š) theorem hasFDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : π•Š) (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) - (((1 : π•Š β†’L[𝕂] π•Š).smul_right x).smul_right (exp 𝕂 (t β€’ x))) t := - by + (((1 : π•Š β†’L[𝕂] π•Š).smul_right x).smul_right (exp 𝕂 (t β€’ x))) t := by convert hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1 ext t' show Commute (t' β€’ x) (exp 𝕂 (t β€’ x)) @@ -342,8 +333,7 @@ theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : π•Š) theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : π•Š) (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) - (((1 : π•Š β†’L[𝕂] π•Š).smul_right x).smul_right (exp 𝕂 (t β€’ x))) t := - by + (((1 : π•Š β†’L[𝕂] π•Š).smul_right x).smul_right (exp 𝕂 (t β€’ x))) t := by let ⟨p, hp⟩ := analyticAt_exp_of_mem_ball (t β€’ x) htx convert hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1 ext t' From 9bd75150054acecc1b3c45291ffcb0154cec6052 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Tue, 6 Jun 2023 12:21:53 +0800 Subject: [PATCH 4/4] Fix errors --- .../SpecialFunctions/Exponential.lean | 188 +++++++++--------- Mathlib/Data/Complex/Basic.lean | 2 +- 2 files changed, 92 insertions(+), 98 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Exponential.lean b/Mathlib/Analysis/SpecialFunctions/Exponential.lean index ea8808fc7229d..b96afa7b55f19 100644 --- a/Mathlib/Analysis/SpecialFunctions/Exponential.lean +++ b/Mathlib/Analysis/SpecialFunctions/Exponential.lean @@ -9,7 +9,7 @@ Authors: Anatole Dedecker, Eric Wieser ! if you have ported upstream changes. -/ import Mathlib.Analysis.NormedSpace.Exponential -import Mathlib.Analysis.Calculus.FderivAnalytic +import Mathlib.Analysis.Calculus.FDerivAnalytic import Mathlib.Topology.MetricSpace.CauSeqFilter /-! @@ -17,41 +17,41 @@ import Mathlib.Topology.MetricSpace.CauSeqFilter In this file, we prove basic properties about the derivative of the exponential map `exp 𝕂` in a Banach algebra `𝔸` over a field `𝕂`. We keep them separate from the main file -`analysis/normed_space/exponential` in order to minimize dependencies. +`Analysis/NormedSpace/Exponential` in order to minimize dependencies. ## Main results -We prove most result for an arbitrary field `𝕂`, and then specialize to `𝕂 = ℝ` or `𝕂 = β„‚`. +We prove most results for an arbitrary field `𝕂`, and then specialize to `𝕂 = ℝ` or `𝕂 = β„‚`. ### General case -- `has_strict_fderiv_at_exp_zero_of_radius_pos` : `exp 𝕂` has strict FrΓ©chet-derivative +- `hasStrictFDerivAt_exp_zero_of_radius_pos` : `exp 𝕂` has strict FrΓ©chet derivative `1 : 𝔸 β†’L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero - (see also `has_strict_deriv_at_exp_zero_of_radius_pos` for the case `𝔸 = 𝕂`) -- `has_strict_fderiv_at_exp_of_lt_radius` : if `𝕂` has characteristic zero and `𝔸` is commutative, - then given a point `x` in the disk of convergence, `exp 𝕂` has strict FrΓ©chet-derivative - `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at x (see also `has_strict_deriv_at_exp_of_lt_radius` for the case + (see also `hasStrictDerivAt_exp_zero_of_radius_pos` for the case `𝔸 = 𝕂`) +- `hasStrictFDerivAt_exp_of_lt_radius` : if `𝕂` has characteristic zero and `𝔸` is commutative, + then given a point `x` in the disk of convergence, `exp 𝕂` has strict FrΓ©chet derivative + `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at x (see also `hasStrictDerivAt_exp_of_lt_radius` for the case `𝔸 = 𝕂`) -- `has_strict_fderiv_at_exp_smul_const_of_mem_ball`: even when `𝔸` is non-commutative, if we have +- `hasStrictFDerivAt_exp_smul_const_of_mem_ball`: even when `𝔸` is non-commutative, if we have an intermediate algebra `π•Š` which is commutative, then the function `(u : π•Š) ↦ exp 𝕂 (u β€’ x)`, - still has strict FrΓ©chet-derivative `exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x` at `t` if + still has strict FrΓ©chet derivative `exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smulRight x` at `t` if `t β€’ x` is in the radius of convergence. ### `𝕂 = ℝ` or `𝕂 = β„‚` -- `has_strict_fderiv_at_exp_zero` : `exp 𝕂` has strict FrΓ©chet-derivative `1 : 𝔸 β†’L[𝕂] 𝔸` at zero - (see also `has_strict_deriv_at_exp_zero` for the case `𝔸 = 𝕂`) -- `has_strict_fderiv_at_exp` : if `𝔸` is commutative, then given any point `x`, `exp 𝕂` has strict - FrΓ©chet-derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at x (see also `has_strict_deriv_at_exp` for the +- `hasStrictFDerivAt_exp_zero` : `exp 𝕂` has strict FrΓ©chet derivative `1 : 𝔸 β†’L[𝕂] 𝔸` at zero + (see also `hasStrictDerivAt_exp_zero` for the case `𝔸 = 𝕂`) +- `hasStrictFDerivAt_exp` : if `𝔸` is commutative, then given any point `x`, `exp 𝕂` has strict + FrΓ©chet derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at x (see also `hasStrictDerivAt_exp` for the case `𝔸 = 𝕂`) -- `has_strict_fderiv_at_exp_smul_const`: even when `𝔸` is non-commutative, if we have +- `hasStrictFDerivAt_exp_smul_const`: even when `𝔸` is non-commutative, if we have an intermediate algebra `π•Š` which is commutative, then the function `(u : π•Š) ↦ exp 𝕂 (u β€’ x)` - still has strict FrΓ©chet-derivative `exp 𝕂 (t β€’ x) β€’ (1 : 𝔸 β†’L[𝕂] 𝔸).smul_right x` at `t`. + still has strict FrΓ©chet derivative `exp 𝕂 (t β€’ x) β€’ (1 : 𝔸 β†’L[𝕂] 𝔸).smulRight x` at `t`. -### Compatibilty with `real.exp` and `complex.exp` +### Compatibilty with `Real.exp` and `Complex.exp` -- `complex.exp_eq_exp_β„‚` : `complex.exp = exp β„‚ β„‚` -- `real.exp_eq_exp_ℝ` : `real.exp = exp ℝ ℝ` +- `Complex.exp_eq_exp_β„‚` : `Complex.exp = exp β„‚ β„‚` +- `Real.exp_eq_exp_ℝ` : `Real.exp = exp ℝ ℝ` -/ @@ -65,21 +65,21 @@ section AnyFieldAnyAlgebra variable {𝕂 𝔸 : Type _} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] -/-- The exponential in a Banach-algebra `𝔸` over a normed field `𝕂` has strict FrΓ©chet-derivative +/-- The exponential in a Banach algebra `𝔸` over a normed field `𝕂` has strict FrΓ©chet derivative `1 : 𝔸 β†’L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero. -/ theorem hasStrictFDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝔸).radius) : HasStrictFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) 0 := by - convert (hasFPowerSeriesAt_exp_zero_of_radius_pos h).HasStrictFDerivAt + convert (hasFPowerSeriesAt_exp_zero_of_radius_pos h).hasStrictFDerivAt ext x change x = expSeries 𝕂 𝔸 1 fun _ => x simp [expSeries_apply_eq] #align has_strict_fderiv_at_exp_zero_of_radius_pos hasStrictFDerivAt_exp_zero_of_radius_pos -/-- The exponential in a Banach-algebra `𝔸` over a normed field `𝕂` has FrΓ©chet-derivative +/-- The exponential in a Banach algebra `𝔸` over a normed field `𝕂` has FrΓ©chet derivative `1 : 𝔸 β†’L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero. -/ theorem hasFDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝔸).radius) : HasFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) 0 := - (hasStrictFDerivAt_exp_zero_of_radius_pos h).HasFDerivAt + (hasStrictFDerivAt_exp_zero_of_radius_pos h).hasFDerivAt #align has_fderiv_at_exp_zero_of_radius_pos hasFDerivAt_exp_zero_of_radius_pos end AnyFieldAnyAlgebra @@ -89,18 +89,18 @@ section AnyFieldCommAlgebra variable {𝕂 𝔸 : Type _} [NontriviallyNormedField 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] -/-- The exponential map in a commutative Banach-algebra `𝔸` over a normed field `𝕂` of -characteristic zero has FrΓ©chet-derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at any point `x` in the +/-- The exponential map in a commutative Banach algebra `𝔸` over a normed field `𝕂` of +characteristic zero has FrΓ©chet derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at any point `x` in the disk of convergence. -/ theorem hasFDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸} (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : - HasFDerivAt (exp 𝕂) (exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸) x := by + HasFDerivAt (exp 𝕂) (exp 𝕂 x β€’ (1 : 𝔸 β†’L[𝕂] 𝔸)) x := by have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt hx rw [hasFDerivAt_iff_isLittleO_nhds_zero] suffices (fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - ContinuousLinearMap.id 𝕂 𝔸 h)) =αΆ [𝓝 0] fun h => exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x β€’ ContinuousLinearMap.id 𝕂 𝔸 h by - refine' (is_o.const_mul_left _ _).congr' this (eventually_eq.refl _ _) + refine' (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _) rw [← hasFDerivAt_iff_isLittleO_nhds_zero] exact hasFDerivAt_exp_zero_of_radius_pos hpos have : βˆ€αΆ  h in 𝓝 (0 : 𝔸), h ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := @@ -110,14 +110,14 @@ theorem hasFDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸} ring #align has_fderiv_at_exp_of_mem_ball hasFDerivAt_exp_of_mem_ball -/-- The exponential map in a commutative Banach-algebra `𝔸` over a normed field `𝕂` of -characteristic zero has strict FrΓ©chet-derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at any point `x` in +/-- The exponential map in a commutative Banach algebra `𝔸` over a normed field `𝕂` of +characteristic zero has strict FrΓ©chet derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at any point `x` in the disk of convergence. -/ theorem hasStrictFDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸} (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : - HasStrictFDerivAt (exp 𝕂) (exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸) x := - let ⟨p, hp⟩ := analyticAt_exp_of_mem_ball x hx - hp.HasFDerivAt.unique (hasFDerivAt_exp_of_mem_ball hx) β–Έ hp.HasStrictFDerivAt + HasStrictFDerivAt (exp 𝕂) (exp 𝕂 x β€’ (1 : 𝔸 β†’L[𝕂] 𝔸)) x := + let ⟨_, hp⟩ := analyticAt_exp_of_mem_ball x hx + hp.hasFDerivAt.unique (hasFDerivAt_exp_of_mem_ball hx) β–Έ hp.hasStrictFDerivAt #align has_strict_fderiv_at_exp_of_mem_ball hasStrictFDerivAt_exp_of_mem_ball end AnyFieldCommAlgebra @@ -130,28 +130,28 @@ variable {𝕂 : Type _} [NontriviallyNormedField 𝕂] [CompleteSpace 𝕂] `exp 𝕂 x` at any point `x` in the disk of convergence. -/ theorem hasStrictDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝕂} (hx : x ∈ EMetric.ball (0 : 𝕂) (expSeries 𝕂 𝕂).radius) : HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x := - by simpa using (hasStrictFDerivAt_exp_of_mem_ball hx).HasStrictDerivAt + by simpa using (hasStrictFDerivAt_exp_of_mem_ball hx).hasStrictDerivAt #align has_strict_deriv_at_exp_of_mem_ball hasStrictDerivAt_exp_of_mem_ball /-- The exponential map in a complete normed field `𝕂` of characteristic zero has derivative `exp 𝕂 x` at any point `x` in the disk of convergence. -/ theorem hasDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝕂} (hx : x ∈ EMetric.ball (0 : 𝕂) (expSeries 𝕂 𝕂).radius) : HasDerivAt (exp 𝕂) (exp 𝕂 x) x := - (hasStrictDerivAt_exp_of_mem_ball hx).HasDerivAt + (hasStrictDerivAt_exp_of_mem_ball hx).hasDerivAt #align has_deriv_at_exp_of_mem_ball hasDerivAt_exp_of_mem_ball /-- The exponential map in a complete normed field `𝕂` of characteristic zero has strict derivative `1` at zero, as long as it converges on a neighborhood of zero. -/ theorem hasStrictDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝕂).radius) : HasStrictDerivAt (exp 𝕂) (1 : 𝕂) 0 := - (hasStrictFDerivAt_exp_zero_of_radius_pos h).HasStrictDerivAt + (hasStrictFDerivAt_exp_zero_of_radius_pos h).hasStrictDerivAt #align has_strict_deriv_at_exp_zero_of_radius_pos hasStrictDerivAt_exp_zero_of_radius_pos /-- The exponential map in a complete normed field `𝕂` of characteristic zero has derivative `1` at zero, as long as it converges on a neighborhood of zero. -/ theorem hasDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝕂).radius) : HasDerivAt (exp 𝕂) (1 : 𝕂) 0 := - (hasStrictDerivAt_exp_zero_of_radius_pos h).HasDerivAt + (hasStrictDerivAt_exp_zero_of_radius_pos h).hasDerivAt #align has_deriv_at_exp_zero_of_radius_pos hasDerivAt_exp_zero_of_radius_pos end deriv @@ -160,16 +160,16 @@ section IsROrCAnyAlgebra variable {𝕂 𝔸 : Type _} [IsROrC 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] -/-- The exponential in a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = β„‚` has strict FrΓ©chet-derivative +/-- The exponential in a Banach algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = β„‚` has strict FrΓ©chet derivative `1 : 𝔸 β†’L[𝕂] 𝔸` at zero. -/ theorem hasStrictFDerivAt_exp_zero : HasStrictFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) 0 := hasStrictFDerivAt_exp_zero_of_radius_pos (expSeries_radius_pos 𝕂 𝔸) #align has_strict_fderiv_at_exp_zero hasStrictFDerivAt_exp_zero -/-- The exponential in a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = β„‚` has FrΓ©chet-derivative +/-- The exponential in a Banach algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = β„‚` has FrΓ©chet derivative `1 : 𝔸 β†’L[𝕂] 𝔸` at zero. -/ theorem hasFDerivAt_exp_zero : HasFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) 0 := - hasStrictFDerivAt_exp_zero.HasFDerivAt + hasStrictFDerivAt_exp_zero.hasFDerivAt #align has_fderiv_at_exp_zero hasFDerivAt_exp_zero end IsROrCAnyAlgebra @@ -178,16 +178,16 @@ section IsROrCCommAlgebra variable {𝕂 𝔸 : Type _} [IsROrC 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] -/-- The exponential map in a commutative Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = β„‚` has strict -FrΓ©chet-derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at any point `x`. -/ -theorem hasStrictFDerivAt_exp {x : 𝔸} : HasStrictFDerivAt (exp 𝕂) (exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸) x := +/-- The exponential map in a commutative Banach algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = β„‚` has strict +FrΓ©chet derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at any point `x`. -/ +theorem hasStrictFDerivAt_exp {x : 𝔸} : HasStrictFDerivAt (exp 𝕂) (exp 𝕂 x β€’ (1 : 𝔸 β†’L[𝕂] 𝔸)) x := hasStrictFDerivAt_exp_of_mem_ball ((expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _) #align has_strict_fderiv_at_exp hasStrictFDerivAt_exp -/-- The exponential map in a commutative Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = β„‚` has -FrΓ©chet-derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at any point `x`. -/ -theorem hasFDerivAt_exp {x : 𝔸} : HasFDerivAt (exp 𝕂) (exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸) x := - hasStrictFDerivAt_exp.HasFDerivAt +/-- The exponential map in a commutative Banach algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = β„‚` has +FrΓ©chet derivative `exp 𝕂 x β€’ 1 : 𝔸 β†’L[𝕂] 𝔸` at any point `x`. -/ +theorem hasFDerivAt_exp {x : 𝔸} : HasFDerivAt (exp 𝕂) (exp 𝕂 x β€’ (1 : 𝔸 β†’L[𝕂] 𝔸)) x := + hasStrictFDerivAt_exp.hasFDerivAt #align has_fderiv_at_exp hasFDerivAt_exp end IsROrCCommAlgebra @@ -204,7 +204,7 @@ theorem hasStrictDerivAt_exp {x : 𝕂} : HasStrictDerivAt (exp 𝕂) (exp 𝕂 /-- The exponential map in `𝕂 = ℝ` or `𝕂 = β„‚` has derivative `exp 𝕂 x` at any point `x`. -/ theorem hasDerivAt_exp {x : 𝕂} : HasDerivAt (exp 𝕂) (exp 𝕂 x) x := - hasStrictDerivAt_exp.HasDerivAt + hasStrictDerivAt_exp.hasDerivAt #align has_deriv_at_exp hasDerivAt_exp /-- The exponential map in `𝕂 = ℝ` or `𝕂 = β„‚` has strict derivative `1` at zero. -/ @@ -214,33 +214,34 @@ theorem hasStrictDerivAt_exp_zero : HasStrictDerivAt (exp 𝕂) (1 : 𝕂) 0 := /-- The exponential map in `𝕂 = ℝ` or `𝕂 = β„‚` has derivative `1` at zero. -/ theorem hasDerivAt_exp_zero : HasDerivAt (exp 𝕂) (1 : 𝕂) 0 := - hasStrictDerivAt_exp_zero.HasDerivAt + hasStrictDerivAt_exp_zero.hasDerivAt #align has_deriv_at_exp_zero hasDerivAt_exp_zero end DerivROrC -theorem Complex.exp_eq_exp_β„‚ : Complex.exp = exp β„‚ := by +theorem Complex.exp_eq_exp_β„‚ : Complex.exp = _root_.exp β„‚ := by refine' funext fun x => _ rw [Complex.exp, exp_eq_tsum_div] - exact tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable ℝ x).HasSum.tendsto_sum_nat + have : CauSeq.IsComplete β„‚ norm := Complex.instIsComplete + exact tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable ℝ x).hasSum.tendsto_sum_nat #align complex.exp_eq_exp_β„‚ Complex.exp_eq_exp_β„‚ -theorem Real.exp_eq_exp_ℝ : Real.exp = exp ℝ := by ext x; - exact_mod_cast congr_fun Complex.exp_eq_exp_β„‚ x +theorem Real.exp_eq_exp_ℝ : Real.exp = _root_.exp ℝ := by + ext x; exact_mod_cast congr_fun Complex.exp_eq_exp_β„‚ x #align real.exp_eq_exp_ℝ Real.exp_eq_exp_ℝ /-! ### Derivative of $\exp (ux)$ by $u$ -Note that since for `x : 𝔸` we have `normed_ring 𝔸` not `normed_comm_ring 𝔸`, we cannot deduce -these results from `has_fderiv_at_exp_of_mem_ball` applied to the algebra `𝔸`. +Note that since for `x : 𝔸` we have `NormedRing 𝔸` not `NormedCommRing 𝔸`, we cannot deduce +these results from `hasFDerivAt_exp_of_mem_ball` applied to the algebra `𝔸`. -One possible solution for that would be to apply `has_fderiv_at_exp_of_mem_ball` to the -commutative algebra `algebra.elemental_algebra π•Š x`. Unfortunately we don't have all the required +One possible solution for that would be to apply `hasFDerivAt_exp_of_mem_ball` to the +commutative algebra `Algebra.elementalAlgebra π•Š x`. Unfortunately we don't have all the required API, so we leave that to a future refactor (see leanprover-community/mathlib#19062 for discussion). -We could also go the other way around and deduce `has_fderiv_at_exp_of_mem_ball` from -`has_fderiv_at_exp_smul_const_of_mem_ball` applied to `π•Š := 𝔸`, `x := (1 : 𝔸)`, and `t := x`. -However, doing so would make the aformentioned `elemental_algebra` refactor harder, so for now we +We could also go the other way around and deduce `hasFDerivAt_exp_of_mem_ball` from +`hasFDerivAt_exp_smul_const_of_mem_ball` applied to `π•Š := 𝔸`, `x := (1 : 𝔸)`, and `t := x`. +However, doing so would make the aformentioned `elementalAlgebra` refactor harder, so for now we just prove these two lemmas independently. A last strategy would be to deduce everything from the more general non-commutative case, @@ -275,32 +276,28 @@ variable [CompleteSpace 𝔸] theorem hasFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : π•Š) (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : - HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) t := by - -- TODO: prove this via `has_fderiv_at_exp_of_mem_ball` using the commutative ring - -- `algebra.elemental_algebra π•Š x`. See leanprover-community/mathlib#19062 for discussion. + HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smulRight x) t := by + -- TODO: prove this via `hasFDerivAt_exp_of_mem_ball` using the commutative ring + -- `Algebra.elementalAlgebra π•Š x`. See leanprover-community/mathlib#19062 for discussion. have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt htx rw [hasFDerivAt_iff_isLittleO_nhds_zero] - suffices - (fun h => - exp 𝕂 (t β€’ x) * - (exp 𝕂 ((0 + h) β€’ x) - exp 𝕂 ((0 : π•Š) β€’ x) - ((1 : π•Š β†’L[𝕂] π•Š).smul_right x) h)) =αΆ [𝓝 0] - fun h => - exp 𝕂 ((t + h) β€’ x) - exp 𝕂 (t β€’ x) - (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) h by - refine' (is_o.const_mul_left _ _).congr' this (eventually_eq.refl _ _) - rw [← - @hasFDerivAt_iff_isLittleO_nhds_zero _ _ _ _ _ _ _ _ (fun u => exp 𝕂 (u β€’ x)) - ((1 : π•Š β†’L[𝕂] π•Š).smul_right x) 0] - have : HasFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) ((1 : π•Š β†’L[𝕂] π•Š).smul_right x 0) := by + suffices (fun (h : π•Š) => exp 𝕂 (t β€’ x) * + (exp 𝕂 ((0 + h) β€’ x) - exp 𝕂 ((0 : π•Š) β€’ x) - ((1 : π•Š β†’L[𝕂] π•Š).smulRight x) h)) =αΆ [𝓝 0] + fun h => + exp 𝕂 ((t + h) β€’ x) - exp 𝕂 (t β€’ x) - (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smulRight x) h by + apply (IsLittleO.const_mul_left _ _).congr' this (EventuallyEq.refl _ _) + rw [← @hasFDerivAt_iff_isLittleO_nhds_zero _ _ _ _ _ _ _ _ (fun u => exp 𝕂 (u β€’ x)) + ((1 : π•Š β†’L[𝕂] π•Š).smulRight x) 0] + have : HasFDerivAt (exp 𝕂) (1 : 𝔸 β†’L[𝕂] 𝔸) ((1 : π•Š β†’L[𝕂] π•Š).smulRight x 0) := by rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul] exact hasFDerivAt_exp_zero_of_radius_pos hpos - exact this.comp 0 ((1 : π•Š β†’L[𝕂] π•Š).smul_right x).HasFDerivAt - have : tendsto (fun h : π•Š => h β€’ x) (𝓝 0) (𝓝 0) := by + exact this.comp 0 ((1 : π•Š β†’L[𝕂] π•Š).smulRight x).hasFDerivAt + have : Tendsto (fun h : π•Š => h β€’ x) (𝓝 0) (𝓝 0) := by rw [← zero_smul π•Š x] exact tendsto_id.smul_const x have : βˆ€αΆ  h in 𝓝 (0 : π•Š), h β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := this.eventually (EMetric.ball_mem_nhds _ hpos) - filter_upwards [this] - intro h hh + filter_upwards [this] with h hh have : Commute (t β€’ x) (h β€’ x) := ((Commute.refl x).smul_left t).smul_right h rw [add_smul t h, exp_add_of_commute_of_mem_ball this htx hh, zero_add, zero_smul, exp_zero, ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, @@ -311,7 +308,7 @@ theorem hasFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : π•Š) theorem hasFDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : π•Š) (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) - (((1 : π•Š β†’L[𝕂] π•Š).smul_right x).smul_right (exp 𝕂 (t β€’ x))) t := by + (((1 : π•Š β†’L[𝕂] π•Š).smulRight x).smulRight (exp 𝕂 (t β€’ x))) t := by convert hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1 ext t' show Commute (t' β€’ x) (exp 𝕂 (t β€’ x)) @@ -320,21 +317,21 @@ theorem hasFDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : π•Š) theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : π•Š) (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : - HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) - t := - let ⟨p, hp⟩ := analyticAt_exp_of_mem_ball (t β€’ x) htx + HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) + (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smulRight x) t := + let ⟨_, hp⟩ := analyticAt_exp_of_mem_ball (t β€’ x) htx have deriv₁ : HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) _ t := - hp.HasStrictFDerivAt.comp t ((ContinuousLinearMap.id 𝕂 π•Š).smul_right x).HasStrictFDerivAt + hp.hasStrictFDerivAt.comp t ((ContinuousLinearMap.id 𝕂 π•Š).smulRight x).hasStrictFDerivAt have derivβ‚‚ : HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) _ t := hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx - deriv₁.HasFDerivAt.unique derivβ‚‚ β–Έ deriv₁ + deriv₁.hasFDerivAt.unique derivβ‚‚ β–Έ deriv₁ #align has_strict_fderiv_at_exp_smul_const_of_mem_ball hasStrictFDerivAt_exp_smul_const_of_mem_ball theorem hasStrictFDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : π•Š) (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) - (((1 : π•Š β†’L[𝕂] π•Š).smul_right x).smul_right (exp 𝕂 (t β€’ x))) t := by - let ⟨p, hp⟩ := analyticAt_exp_of_mem_ball (t β€’ x) htx + (((1 : π•Š β†’L[𝕂] π•Š).smulRight x).smulRight (exp 𝕂 (t β€’ x))) t := by + let ⟨_, _⟩ := analyticAt_exp_of_mem_ball (t β€’ x) htx convert hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1 ext t' show Commute (t' β€’ x) (exp 𝕂 (t β€’ x)) @@ -346,25 +343,25 @@ variable {𝕂} theorem hasStrictDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕂) (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : HasStrictDerivAt (fun u : 𝕂 => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) * x) t := by - simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx).HasStrictDerivAt + simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 x t htx).hasStrictDerivAt #align has_strict_deriv_at_exp_smul_const_of_mem_ball hasStrictDerivAt_exp_smul_const_of_mem_ball theorem hasStrictDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : 𝕂) (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : HasStrictDerivAt (fun u : 𝕂 => exp 𝕂 (u β€’ x)) (x * exp 𝕂 (t β€’ x)) t := by - simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball' 𝕂 x t htx).HasStrictDerivAt + simpa using (hasStrictFDerivAt_exp_smul_const_of_mem_ball' 𝕂 x t htx).hasStrictDerivAt #align has_strict_deriv_at_exp_smul_const_of_mem_ball' hasStrictDerivAt_exp_smul_const_of_mem_ball' theorem hasDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕂) (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : HasDerivAt (fun u : 𝕂 => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) * x) t := - (hasStrictDerivAt_exp_smul_const_of_mem_ball x t htx).HasDerivAt + (hasStrictDerivAt_exp_smul_const_of_mem_ball x t htx).hasDerivAt #align has_deriv_at_exp_smul_const_of_mem_ball hasDerivAt_exp_smul_const_of_mem_ball theorem hasDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : 𝕂) (htx : t β€’ x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : HasDerivAt (fun u : 𝕂 => exp 𝕂 (u β€’ x)) (x * exp 𝕂 (t β€’ x)) t := - (hasStrictDerivAt_exp_smul_const_of_mem_ball' x t htx).HasDerivAt + (hasStrictDerivAt_exp_smul_const_of_mem_ball' x t htx).hasDerivAt #align has_deriv_at_exp_smul_const_of_mem_ball' hasDerivAt_exp_smul_const_of_mem_ball' end MemBall @@ -381,31 +378,29 @@ variable [IsScalarTower 𝕂 π•Š 𝔸] variable [CompleteSpace 𝔸] -variable (𝕂) - theorem hasFDerivAt_exp_smul_const (x : 𝔸) (t : π•Š) : - HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) t := + HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smulRight x) t := hasFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ <| (expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _ #align has_fderiv_at_exp_smul_const hasFDerivAt_exp_smul_const theorem hasFDerivAt_exp_smul_const' (x : 𝔸) (t : π•Š) : HasFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) - (((1 : π•Š β†’L[𝕂] π•Š).smul_right x).smul_right (exp 𝕂 (t β€’ x))) t := + (((1 : π•Š β†’L[𝕂] π•Š).smulRight x).smulRight (exp 𝕂 (t β€’ x))) t := hasFDerivAt_exp_smul_const_of_mem_ball' 𝕂 _ _ <| (expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _ #align has_fderiv_at_exp_smul_const' hasFDerivAt_exp_smul_const' theorem hasStrictFDerivAt_exp_smul_const (x : 𝔸) (t : π•Š) : - HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smul_right x) - t := + HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) + (exp 𝕂 (t β€’ x) β€’ (1 : π•Š β†’L[𝕂] π•Š).smulRight x) t := hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ <| (expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _ #align has_strict_fderiv_at_exp_smul_const hasStrictFDerivAt_exp_smul_const theorem hasStrictFDerivAt_exp_smul_const' (x : 𝔸) (t : π•Š) : HasStrictFDerivAt (fun u : π•Š => exp 𝕂 (u β€’ x)) - (((1 : π•Š β†’L[𝕂] π•Š).smul_right x).smul_right (exp 𝕂 (t β€’ x))) t := + (((1 : π•Š β†’L[𝕂] π•Š).smulRight x).smulRight (exp 𝕂 (t β€’ x))) t := hasStrictFDerivAt_exp_smul_const_of_mem_ball' 𝕂 _ _ <| (expSeries_radius_eq_top 𝕂 𝔸).symm β–Έ edist_lt_top _ _ #align has_strict_fderiv_at_exp_smul_const' hasStrictFDerivAt_exp_smul_const' @@ -438,4 +433,3 @@ theorem hasDerivAt_exp_smul_const' (x : 𝔸) (t : 𝕂) : end IsROrC end exp_smul - diff --git a/Mathlib/Data/Complex/Basic.lean b/Mathlib/Data/Complex/Basic.lean index 95e02806e4f5f..2ea0bc1577a12 100644 --- a/Mathlib/Data/Complex/Basic.lean +++ b/Mathlib/Data/Complex/Basic.lean @@ -1281,7 +1281,7 @@ theorem equiv_limAux (f : CauSeq β„‚ Complex.abs) : rwa [add_halves] at this #align complex.equiv_lim_aux Complex.equiv_limAux -instance : CauSeq.IsComplete β„‚ Complex.abs := +instance instIsComplete : CauSeq.IsComplete β„‚ Complex.abs := ⟨fun f => ⟨limAux f, equiv_limAux f⟩⟩ open CauSeq