From 60e4a87afc0b5dbed16ad89a865475b3f8a20d00 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Tue, 17 Sep 2024 19:29:30 +0000 Subject: [PATCH] chore: split the `change origin` part from `Analytic.Basic` (#16891) Just moving things around, no mathematical change. --- Mathlib.lean | 1 + Mathlib/Analysis/Analytic/Basic.lean | 331 ----------------- Mathlib/Analysis/Analytic/CPolynomial.lean | 2 +- Mathlib/Analysis/Analytic/ChangeOrigin.lean | 346 ++++++++++++++++++ Mathlib/Analysis/Analytic/Uniqueness.lean | 1 + .../Analysis/Normed/Algebra/Exponential.lean | 2 +- 6 files changed, 350 insertions(+), 333 deletions(-) create mode 100644 Mathlib/Analysis/Analytic/ChangeOrigin.lean diff --git a/Mathlib.lean b/Mathlib.lean index ff8fd5cd76256..0fad7e2c8e664 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -913,6 +913,7 @@ import Mathlib.AlgebraicTopology.SplitSimplicialObject import Mathlib.AlgebraicTopology.TopologicalSimplex import Mathlib.Analysis.Analytic.Basic import Mathlib.Analysis.Analytic.CPolynomial +import Mathlib.Analysis.Analytic.ChangeOrigin import Mathlib.Analysis.Analytic.Composition import Mathlib.Analysis.Analytic.Constructions import Mathlib.Analysis.Analytic.Inverse diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean index 39a6415f0f341..a8d94d40086a9 100644 --- a/Mathlib/Analysis/Analytic/Basic.lean +++ b/Mathlib/Analysis/Analytic/Basic.lean @@ -1404,334 +1404,6 @@ theorem HasFPowerSeriesOnBall.r_eq_top_of_exists {f : π•œ β†’ E} {r : ℝβ‰₯0 end Uniqueness -/-! -### Changing origin in a power series - -If a function is analytic in a disk `D(x, R)`, then it is analytic in any disk contained in that -one. Indeed, one can write -$$ -f (x + y + z) = \sum_{n} p_n (y + z)^n = \sum_{n, k} \binom{n}{k} p_n y^{n-k} z^k -= \sum_{k} \Bigl(\sum_{n} \binom{n}{k} p_n y^{n-k}\Bigr) z^k. -$$ -The corresponding power series has thus a `k`-th coefficient equal to -$\sum_{n} \binom{n}{k} p_n y^{n-k}$. In the general case where `pβ‚™` is a multilinear map, this has -to be interpreted suitably: instead of having a binomial coefficient, one should sum over all -possible subsets `s` of `Fin n` of cardinality `k`, and attribute `z` to the indices in `s` and -`y` to the indices outside of `s`. - -In this paragraph, we implement this. The new power series is called `p.changeOrigin y`. Then, we -check its convergence and the fact that its sum coincides with the original sum. The outcome of this -discussion is that the set of points where a function is analytic is open. --/ - - -namespace FormalMultilinearSeries - -section - -variable (p : FormalMultilinearSeries π•œ E F) {x y : E} {r R : ℝβ‰₯0} - -/-- A term of `FormalMultilinearSeries.changeOriginSeries`. - -Given a formal multilinear series `p` and a point `x` in its ball of convergence, -`p.changeOrigin x` is a formal multilinear series such that -`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense. Each term of `p.changeOrigin x` -is itself an analytic function of `x` given by the series `p.changeOriginSeries`. Each term in -`changeOriginSeries` is the sum of `changeOriginSeriesTerm`'s over all `s` of cardinality `l`. -The definition is such that `p.changeOriginSeriesTerm k l s hs (fun _ ↦ x) (fun _ ↦ y) = -p (k + l) (s.piecewise (fun _ ↦ x) (fun _ ↦ y))` --/ -def changeOriginSeriesTerm (k l : β„•) (s : Finset (Fin (k + l))) (hs : s.card = l) : - E[Γ—l]β†’L[π•œ] E[Γ—k]β†’L[π•œ] F := - let a := ContinuousMultilinearMap.curryFinFinset π•œ E F hs - (by erw [Finset.card_compl, Fintype.card_fin, hs, add_tsub_cancel_right]) - a (p (k + l)) - -theorem changeOriginSeriesTerm_apply (k l : β„•) (s : Finset (Fin (k + l))) (hs : s.card = l) - (x y : E) : - (p.changeOriginSeriesTerm k l s hs (fun _ => x) fun _ => y) = - p (k + l) (s.piecewise (fun _ => x) fun _ => y) := - ContinuousMultilinearMap.curryFinFinset_apply_const _ _ _ _ _ - -@[simp] -theorem norm_changeOriginSeriesTerm (k l : β„•) (s : Finset (Fin (k + l))) (hs : s.card = l) : - β€–p.changeOriginSeriesTerm k l s hsβ€– = β€–p (k + l)β€– := by - simp only [changeOriginSeriesTerm, LinearIsometryEquiv.norm_map] - -@[simp] -theorem nnnorm_changeOriginSeriesTerm (k l : β„•) (s : Finset (Fin (k + l))) (hs : s.card = l) : - β€–p.changeOriginSeriesTerm k l s hsβ€–β‚Š = β€–p (k + l)β€–β‚Š := by - simp only [changeOriginSeriesTerm, LinearIsometryEquiv.nnnorm_map] - -theorem nnnorm_changeOriginSeriesTerm_apply_le (k l : β„•) (s : Finset (Fin (k + l))) - (hs : s.card = l) (x y : E) : - β€–p.changeOriginSeriesTerm k l s hs (fun _ => x) fun _ => yβ€–β‚Š ≀ - β€–p (k + l)β€–β‚Š * β€–xβ€–β‚Š ^ l * β€–yβ€–β‚Š ^ k := by - rw [← p.nnnorm_changeOriginSeriesTerm k l s hs, ← Fin.prod_const, ← Fin.prod_const] - apply ContinuousMultilinearMap.le_of_opNNNorm_le - apply ContinuousMultilinearMap.le_opNNNorm - -/-- The power series for `f.changeOrigin k`. - -Given a formal multilinear series `p` and a point `x` in its ball of convergence, -`p.changeOrigin x` is a formal multilinear series such that -`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense. Its `k`-th term is the sum of -the series `p.changeOriginSeries k`. -/ -def changeOriginSeries (k : β„•) : FormalMultilinearSeries π•œ E (E[Γ—k]β†’L[π•œ] F) := fun l => - βˆ‘ s : { s : Finset (Fin (k + l)) // Finset.card s = l }, p.changeOriginSeriesTerm k l s s.2 - -theorem nnnorm_changeOriginSeries_le_tsum (k l : β„•) : - β€–p.changeOriginSeries k lβ€–β‚Š ≀ - βˆ‘' _ : { s : Finset (Fin (k + l)) // s.card = l }, β€–p (k + l)β€–β‚Š := - (nnnorm_sum_le _ (fun t => changeOriginSeriesTerm p k l (Subtype.val t) t.prop)).trans_eq <| by - simp_rw [tsum_fintype, nnnorm_changeOriginSeriesTerm (p := p) (k := k) (l := l)] - -theorem nnnorm_changeOriginSeries_apply_le_tsum (k l : β„•) (x : E) : - β€–p.changeOriginSeries k l fun _ => xβ€–β‚Š ≀ - βˆ‘' _ : { s : Finset (Fin (k + l)) // s.card = l }, β€–p (k + l)β€–β‚Š * β€–xβ€–β‚Š ^ l := by - rw [NNReal.tsum_mul_right, ← Fin.prod_const] - exact (p.changeOriginSeries k l).le_of_opNNNorm_le _ (p.nnnorm_changeOriginSeries_le_tsum _ _) - -/-- Changing the origin of a formal multilinear series `p`, so that -`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense. --/ -def changeOrigin (x : E) : FormalMultilinearSeries π•œ E F := - fun k => (p.changeOriginSeries k).sum x - -/-- An auxiliary equivalence useful in the proofs about -`FormalMultilinearSeries.changeOriginSeries`: the set of triples `(k, l, s)`, where `s` is a -`Finset (Fin (k + l))` of cardinality `l` is equivalent to the set of pairs `(n, s)`, where `s` is a -`Finset (Fin n)`. - -The forward map sends `(k, l, s)` to `(k + l, s)` and the inverse map sends `(n, s)` to -`(n - Finset.card s, Finset.card s, s)`. The actual definition is less readable because of problems -with non-definitional equalities. -/ -@[simps] -def changeOriginIndexEquiv : - (Ξ£ k l : β„•, { s : Finset (Fin (k + l)) // s.card = l }) ≃ Ξ£ n : β„•, Finset (Fin n) where - toFun s := ⟨s.1 + s.2.1, s.2.2⟩ - invFun s := - ⟨s.1 - s.2.card, s.2.card, - ⟨s.2.map - (finCongr <| (tsub_add_cancel_of_le <| card_finset_fin_le s.2).symm).toEmbedding, - Finset.card_map _⟩⟩ - left_inv := by - rintro ⟨k, l, ⟨s : Finset (Fin <| k + l), hs : s.card = l⟩⟩ - dsimp only [Subtype.coe_mk] - -- Lean can't automatically generalize `k' = k + l - s.card`, `l' = s.card`, so we explicitly - -- formulate the generalized goal - suffices βˆ€ k' l', k' = k β†’ l' = l β†’ βˆ€ (hkl : k + l = k' + l') (hs'), - (⟨k', l', ⟨s.map (finCongr hkl).toEmbedding, hs'⟩⟩ : - Ξ£k l : β„•, { s : Finset (Fin (k + l)) // s.card = l }) = ⟨k, l, ⟨s, hs⟩⟩ by - apply this <;> simp only [hs, add_tsub_cancel_right] - rintro _ _ rfl rfl hkl hs' - simp only [Equiv.refl_toEmbedding, finCongr_refl, Finset.map_refl, eq_self_iff_true, - OrderIso.refl_toEquiv, and_self_iff, heq_iff_eq] - right_inv := by - rintro ⟨n, s⟩ - simp [tsub_add_cancel_of_le (card_finset_fin_le s), finCongr_eq_equivCast] - -lemma changeOriginSeriesTerm_changeOriginIndexEquiv_symm (n t) : - let s := changeOriginIndexEquiv.symm ⟨n, t⟩ - p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ ↦ x) (fun _ ↦ y) = - p n (t.piecewise (fun _ ↦ x) fun _ ↦ y) := by - have : βˆ€ (m) (hm : n = m), p n (t.piecewise (fun _ ↦ x) fun _ ↦ y) = - p m ((t.map (finCongr hm).toEmbedding).piecewise (fun _ ↦ x) fun _ ↦ y) := by - rintro m rfl - simp (config := { unfoldPartialApp := true }) [Finset.piecewise] - simp_rw [changeOriginSeriesTerm_apply, eq_comm]; apply this - -theorem changeOriginSeries_summable_aux₁ {r r' : ℝβ‰₯0} (hr : (r + r' : ℝβ‰₯0∞) < p.radius) : - Summable fun s : Ξ£k l : β„•, { s : Finset (Fin (k + l)) // s.card = l } => - β€–p (s.1 + s.2.1)β€–β‚Š * r ^ s.2.1 * r' ^ s.1 := by - rw [← changeOriginIndexEquiv.symm.summable_iff] - dsimp only [Function.comp_def, changeOriginIndexEquiv_symm_apply_fst, - changeOriginIndexEquiv_symm_apply_snd_fst] - have : βˆ€ n : β„•, - HasSum (fun s : Finset (Fin n) => β€–p (n - s.card + s.card)β€–β‚Š * r ^ s.card * r' ^ (n - s.card)) - (β€–p nβ€–β‚Š * (r + r') ^ n) := by - intro n - -- TODO: why `simp only [tsub_add_cancel_of_le (card_finset_fin_le _)]` fails? - convert_to HasSum (fun s : Finset (Fin n) => β€–p nβ€–β‚Š * (r ^ s.card * r' ^ (n - s.card))) _ - Β· ext1 s - rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc] - rw [← Fin.sum_pow_mul_eq_add_pow] - exact (hasSum_fintype _).mul_left _ - refine NNReal.summable_sigma.2 ⟨fun n => (this n).summable, ?_⟩ - simp only [(this _).tsum_eq] - exact p.summable_nnnorm_mul_pow hr - -theorem changeOriginSeries_summable_auxβ‚‚ (hr : (r : ℝβ‰₯0∞) < p.radius) (k : β„•) : - Summable fun s : Ξ£l : β„•, { s : Finset (Fin (k + l)) // s.card = l } => - β€–p (k + s.1)β€–β‚Š * r ^ s.1 := by - rcases ENNReal.lt_iff_exists_add_pos_lt.1 hr with ⟨r', h0, hr'⟩ - simpa only [mul_inv_cancel_rightβ‚€ (pow_pos h0 _).ne'] using - ((NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr')).1 k).mul_right (r' ^ k)⁻¹ - -theorem changeOriginSeries_summable_aux₃ {r : ℝβ‰₯0} (hr : ↑r < p.radius) (k : β„•) : - Summable fun l : β„• => β€–p.changeOriginSeries k lβ€–β‚Š * r ^ l := by - refine NNReal.summable_of_le - (fun n => ?_) (NNReal.summable_sigma.1 <| p.changeOriginSeries_summable_auxβ‚‚ hr k).2 - simp only [NNReal.tsum_mul_right] - exact mul_le_mul' (p.nnnorm_changeOriginSeries_le_tsum _ _) le_rfl - -theorem le_changeOriginSeries_radius (k : β„•) : p.radius ≀ (p.changeOriginSeries k).radius := - ENNReal.le_of_forall_nnreal_lt fun _r hr => - le_radius_of_summable_nnnorm _ (p.changeOriginSeries_summable_aux₃ hr k) - -theorem nnnorm_changeOrigin_le (k : β„•) (h : (β€–xβ€–β‚Š : ℝβ‰₯0∞) < p.radius) : - β€–p.changeOrigin x kβ€–β‚Š ≀ - βˆ‘' s : Ξ£l : β„•, { s : Finset (Fin (k + l)) // s.card = l }, β€–p (k + s.1)β€–β‚Š * β€–xβ€–β‚Š ^ s.1 := by - refine tsum_of_nnnorm_bounded ?_ fun l => p.nnnorm_changeOriginSeries_apply_le_tsum k l x - have := p.changeOriginSeries_summable_auxβ‚‚ h k - refine HasSum.sigma this.hasSum fun l => ?_ - exact ((NNReal.summable_sigma.1 this).1 l).hasSum - -/-- The radius of convergence of `p.changeOrigin x` is at least `p.radius - β€–xβ€–`. In other words, -`p.changeOrigin x` is well defined on the largest ball contained in the original ball of -convergence. -/ -theorem changeOrigin_radius : p.radius - β€–xβ€–β‚Š ≀ (p.changeOrigin x).radius := by - refine ENNReal.le_of_forall_pos_nnreal_lt fun r _h0 hr => ?_ - rw [lt_tsub_iff_right, add_comm] at hr - have hr' : (β€–xβ€–β‚Š : ℝβ‰₯0∞) < p.radius := (le_add_right le_rfl).trans_lt hr - apply le_radius_of_summable_nnnorm - have : βˆ€ k : β„•, - β€–p.changeOrigin x kβ€–β‚Š * r ^ k ≀ - (βˆ‘' s : Ξ£l : β„•, { s : Finset (Fin (k + l)) // s.card = l }, β€–p (k + s.1)β€–β‚Š * β€–xβ€–β‚Š ^ s.1) * - r ^ k := - fun k => mul_le_mul_right' (p.nnnorm_changeOrigin_le k hr') (r ^ k) - refine NNReal.summable_of_le this ?_ - simpa only [← NNReal.tsum_mul_right] using - (NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr)).2 - -/-- `derivSeries p` is a power series for `fderiv π•œ f` if `p` is a power series for `f`, -see `HasFPowerSeriesOnBall.fderiv`. -/ -def derivSeries : FormalMultilinearSeries π•œ E (E β†’L[π•œ] F) := - (continuousMultilinearCurryFin1 π•œ E F : (E[Γ—1]β†’L[π•œ] F) β†’L[π•œ] E β†’L[π•œ] F) - |>.compFormalMultilinearSeries (p.changeOriginSeries 1) - -end - --- From this point on, assume that the space is complete, to make sure that series that converge --- in norm also converge in `F`. -variable [CompleteSpace F] (p : FormalMultilinearSeries π•œ E F) {x y : E} {r R : ℝβ‰₯0} - -theorem hasFPowerSeriesOnBall_changeOrigin (k : β„•) (hr : 0 < p.radius) : - HasFPowerSeriesOnBall (fun x => p.changeOrigin x k) (p.changeOriginSeries k) 0 p.radius := - have := p.le_changeOriginSeries_radius k - ((p.changeOriginSeries k).hasFPowerSeriesOnBall (hr.trans_le this)).mono hr this - -/-- Summing the series `p.changeOrigin x` at a point `y` gives back `p (x + y)`. -/ -theorem changeOrigin_eval (h : (β€–xβ€–β‚Š + β€–yβ€–β‚Š : ℝβ‰₯0∞) < p.radius) : - (p.changeOrigin x).sum y = p.sum (x + y) := by - have radius_pos : 0 < p.radius := lt_of_le_of_lt (zero_le _) h - have x_mem_ball : x ∈ EMetric.ball (0 : E) p.radius := - mem_emetric_ball_zero_iff.2 ((le_add_right le_rfl).trans_lt h) - have y_mem_ball : y ∈ EMetric.ball (0 : E) (p.changeOrigin x).radius := by - refine mem_emetric_ball_zero_iff.2 (lt_of_lt_of_le ?_ p.changeOrigin_radius) - rwa [lt_tsub_iff_right, add_comm] - have x_add_y_mem_ball : x + y ∈ EMetric.ball (0 : E) p.radius := by - refine mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt ?_ h) - exact mod_cast nnnorm_add_le x y - set f : (Ξ£ k l : β„•, { s : Finset (Fin (k + l)) // s.card = l }) β†’ F := fun s => - p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ => x) fun _ => y - have hsf : Summable f := by - refine .of_nnnorm_bounded _ (p.changeOriginSeries_summable_aux₁ h) ?_ - rintro ⟨k, l, s, hs⟩ - dsimp only [Subtype.coe_mk] - exact p.nnnorm_changeOriginSeriesTerm_apply_le _ _ _ _ _ _ - have hf : HasSum f ((p.changeOrigin x).sum y) := by - refine HasSum.sigma_of_hasSum ((p.changeOrigin x).summable y_mem_ball).hasSum (fun k => ?_) hsf - Β· dsimp only [f] - refine ContinuousMultilinearMap.hasSum_eval ?_ _ - have := (p.hasFPowerSeriesOnBall_changeOrigin k radius_pos).hasSum x_mem_ball - rw [zero_add] at this - refine HasSum.sigma_of_hasSum this (fun l => ?_) ?_ - Β· simp only [changeOriginSeries, ContinuousMultilinearMap.sum_apply] - apply hasSum_fintype - Β· refine .of_nnnorm_bounded _ - (p.changeOriginSeries_summable_auxβ‚‚ (mem_emetric_ball_zero_iff.1 x_mem_ball) k) - fun s => ?_ - refine (ContinuousMultilinearMap.le_opNNNorm _ _).trans_eq ?_ - simp - refine hf.unique (changeOriginIndexEquiv.symm.hasSum_iff.1 ?_) - refine HasSum.sigma_of_hasSum - (p.hasSum x_add_y_mem_ball) (fun n => ?_) (changeOriginIndexEquiv.symm.summable_iff.2 hsf) - erw [(p n).map_add_univ (fun _ => x) fun _ => y] - simp_rw [← changeOriginSeriesTerm_changeOriginIndexEquiv_symm] - exact hasSum_fintype (fun c => f (changeOriginIndexEquiv.symm ⟨n, c⟩)) - -/-- Power series terms are analytic as we vary the origin -/ -theorem analyticAt_changeOrigin (p : FormalMultilinearSeries π•œ E F) (rp : p.radius > 0) (n : β„•) : - AnalyticAt π•œ (fun x ↦ p.changeOrigin x n) 0 := - (FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin p n rp).analyticAt - -end FormalMultilinearSeries - -section - -variable [CompleteSpace F] {f : E β†’ F} {p : FormalMultilinearSeries π•œ E F} {x y : E} {r : ℝβ‰₯0∞} - -/-- If a function admits a power series expansion `p` on a ball `B (x, r)`, then it also admits a -power series on any subball of this ball (even with a different center), given by `p.changeOrigin`. --/ -theorem HasFPowerSeriesOnBall.changeOrigin (hf : HasFPowerSeriesOnBall f p x r) - (h : (β€–yβ€–β‚Š : ℝβ‰₯0∞) < r) : HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - β€–yβ€–β‚Š) := - { r_le := by - apply le_trans _ p.changeOrigin_radius - exact tsub_le_tsub hf.r_le le_rfl - r_pos := by simp [h] - hasSum := fun {z} hz => by - have : f (x + y + z) = - FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z := by - rw [mem_emetric_ball_zero_iff, lt_tsub_iff_right, add_comm] at hz - rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum] - refine mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt ?_ hz) - exact mod_cast nnnorm_add_le y z - rw [this] - apply (p.changeOrigin y).hasSum - refine EMetric.ball_subset_ball (le_trans ?_ p.changeOrigin_radius) hz - exact tsub_le_tsub hf.r_le le_rfl } - -/-- If a function admits a power series expansion `p` on an open ball `B (x, r)`, then -it is analytic at every point of this ball. -/ -theorem HasFPowerSeriesOnBall.analyticAt_of_mem (hf : HasFPowerSeriesOnBall f p x r) - (h : y ∈ EMetric.ball x r) : AnalyticAt π•œ f y := by - have : (β€–y - xβ€–β‚Š : ℝβ‰₯0∞) < r := by simpa [edist_eq_coe_nnnorm_sub] using h - have := hf.changeOrigin this - rw [add_sub_cancel] at this - exact this.analyticAt - -theorem HasFPowerSeriesOnBall.analyticOn (hf : HasFPowerSeriesOnBall f p x r) : - AnalyticOn π•œ f (EMetric.ball x r) := - fun _y hy => hf.analyticAt_of_mem hy - -variable (π•œ f) - -/-- For any function `f` from a normed vector space to a Banach space, the set of points `x` such -that `f` is analytic at `x` is open. -/ -theorem isOpen_analyticAt : IsOpen { x | AnalyticAt π•œ f x } := by - rw [isOpen_iff_mem_nhds] - rintro x ⟨p, r, hr⟩ - exact mem_of_superset (EMetric.ball_mem_nhds _ hr.r_pos) fun y hy => hr.analyticAt_of_mem hy - -variable {π•œ} - -theorem AnalyticAt.eventually_analyticAt {f : E β†’ F} {x : E} (h : AnalyticAt π•œ f x) : - βˆ€αΆ  y in 𝓝 x, AnalyticAt π•œ f y := - (isOpen_analyticAt π•œ f).mem_nhds h - -theorem AnalyticAt.exists_mem_nhds_analyticOn {f : E β†’ F} {x : E} (h : AnalyticAt π•œ f x) : - βˆƒ s ∈ 𝓝 x, AnalyticOn π•œ f s := - h.eventually_analyticAt.exists_mem - -/-- If we're analytic at a point, we're analytic in a nonempty ball -/ -theorem AnalyticAt.exists_ball_analyticOn {f : E β†’ F} {x : E} (h : AnalyticAt π•œ f x) : - βˆƒ r : ℝ, 0 < r ∧ AnalyticOn π•œ f (Metric.ball x r) := - Metric.isOpen_iff.mp (isOpen_analyticAt _ _) _ h - -end - section open FormalMultilinearSeries @@ -1769,6 +1441,3 @@ theorem hasFPowerSeriesAt_iff' : simp_rw [add_sub_cancel_left] end - -/- TODO: move the part on `ChangeOrigin` to another file. -/ -set_option linter.style.longFile 1800 diff --git a/Mathlib/Analysis/Analytic/CPolynomial.lean b/Mathlib/Analysis/Analytic/CPolynomial.lean index 216f900d967b7..c9271baf1873a 100644 --- a/Mathlib/Analysis/Analytic/CPolynomial.lean +++ b/Mathlib/Analysis/Analytic/CPolynomial.lean @@ -3,7 +3,7 @@ Copyright (c) 2023 Sophie Morel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sophie Morel -/ -import Mathlib.Analysis.Analytic.Basic +import Mathlib.Analysis.Analytic.ChangeOrigin /-! We specialize the theory fo analytic functions to the case of functions that admit a development given by a *finite* formal multilinear series. We call them "continuously polynomial", diff --git a/Mathlib/Analysis/Analytic/ChangeOrigin.lean b/Mathlib/Analysis/Analytic/ChangeOrigin.lean new file mode 100644 index 0000000000000..9e2a610834e3a --- /dev/null +++ b/Mathlib/Analysis/Analytic/ChangeOrigin.lean @@ -0,0 +1,346 @@ +/- +Copyright (c) 2020 SΓ©bastien GouΓ«zel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: SΓ©bastien GouΓ«zel, Yury Kudryashov +-/ +import Mathlib.Analysis.Analytic.Basic + +/-! +# Changing origin in a power series + +If a function is analytic in a disk `D(x, R)`, then it is analytic in any disk contained in that +one. Indeed, one can write +$$ +f (x + y + z) = \sum_{n} p_n (y + z)^n = \sum_{n, k} \binom{n}{k} p_n y^{n-k} z^k += \sum_{k} \Bigl(\sum_{n} \binom{n}{k} p_n y^{n-k}\Bigr) z^k. +$$ +The corresponding power series has thus a `k`-th coefficient equal to +$\sum_{n} \binom{n}{k} p_n y^{n-k}$. In the general case where `pβ‚™` is a multilinear map, this has +to be interpreted suitably: instead of having a binomial coefficient, one should sum over all +possible subsets `s` of `Fin n` of cardinality `k`, and attribute `z` to the indices in `s` and +`y` to the indices outside of `s`. + +In this file, we implement this. The new power series is called `p.changeOrigin y`. Then, we +check its convergence and the fact that its sum coincides with the original sum. The outcome of this +discussion is that the set of points where a function is analytic is open. All these arguments +require the target space to be complete, as otherwise the series might not converge. + +### Main results + +In a complete space, if a function admits a power series in a ball, then it is analytic at any +point `y` of this ball, and the power series there can be expressed in terms of the initial power +series `p` as `p.changeOrigin y`. See `HasFPowerSeriesOnBall.changeOrigin`. It follows in particular +that the set of points at which a given function is analytic is open, see `isOpen_analyticAt`. +-/ + +noncomputable section + +open scoped NNReal ENNReal Topology +open Filter + +variable {π•œ E F : Type*} [NontriviallyNormedField π•œ] [NormedAddCommGroup E] [NormedSpace π•œ E] +[NormedAddCommGroup F] [NormedSpace π•œ F] + +namespace FormalMultilinearSeries + +section + +variable (p : FormalMultilinearSeries π•œ E F) {x y : E} {r R : ℝβ‰₯0} + +/-- A term of `FormalMultilinearSeries.changeOriginSeries`. + +Given a formal multilinear series `p` and a point `x` in its ball of convergence, +`p.changeOrigin x` is a formal multilinear series such that +`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense. Each term of `p.changeOrigin x` +is itself an analytic function of `x` given by the series `p.changeOriginSeries`. Each term in +`changeOriginSeries` is the sum of `changeOriginSeriesTerm`'s over all `s` of cardinality `l`. +The definition is such that `p.changeOriginSeriesTerm k l s hs (fun _ ↦ x) (fun _ ↦ y) = +p (k + l) (s.piecewise (fun _ ↦ x) (fun _ ↦ y))` +-/ +def changeOriginSeriesTerm (k l : β„•) (s : Finset (Fin (k + l))) (hs : s.card = l) : + E[Γ—l]β†’L[π•œ] E[Γ—k]β†’L[π•œ] F := + let a := ContinuousMultilinearMap.curryFinFinset π•œ E F hs + (by erw [Finset.card_compl, Fintype.card_fin, hs, add_tsub_cancel_right]) + a (p (k + l)) + +theorem changeOriginSeriesTerm_apply (k l : β„•) (s : Finset (Fin (k + l))) (hs : s.card = l) + (x y : E) : + (p.changeOriginSeriesTerm k l s hs (fun _ => x) fun _ => y) = + p (k + l) (s.piecewise (fun _ => x) fun _ => y) := + ContinuousMultilinearMap.curryFinFinset_apply_const _ _ _ _ _ + +@[simp] +theorem norm_changeOriginSeriesTerm (k l : β„•) (s : Finset (Fin (k + l))) (hs : s.card = l) : + β€–p.changeOriginSeriesTerm k l s hsβ€– = β€–p (k + l)β€– := by + simp only [changeOriginSeriesTerm, LinearIsometryEquiv.norm_map] + +@[simp] +theorem nnnorm_changeOriginSeriesTerm (k l : β„•) (s : Finset (Fin (k + l))) (hs : s.card = l) : + β€–p.changeOriginSeriesTerm k l s hsβ€–β‚Š = β€–p (k + l)β€–β‚Š := by + simp only [changeOriginSeriesTerm, LinearIsometryEquiv.nnnorm_map] + +theorem nnnorm_changeOriginSeriesTerm_apply_le (k l : β„•) (s : Finset (Fin (k + l))) + (hs : s.card = l) (x y : E) : + β€–p.changeOriginSeriesTerm k l s hs (fun _ => x) fun _ => yβ€–β‚Š ≀ + β€–p (k + l)β€–β‚Š * β€–xβ€–β‚Š ^ l * β€–yβ€–β‚Š ^ k := by + rw [← p.nnnorm_changeOriginSeriesTerm k l s hs, ← Fin.prod_const, ← Fin.prod_const] + apply ContinuousMultilinearMap.le_of_opNNNorm_le + apply ContinuousMultilinearMap.le_opNNNorm + +/-- The power series for `f.changeOrigin k`. + +Given a formal multilinear series `p` and a point `x` in its ball of convergence, +`p.changeOrigin x` is a formal multilinear series such that +`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense. Its `k`-th term is the sum of +the series `p.changeOriginSeries k`. -/ +def changeOriginSeries (k : β„•) : FormalMultilinearSeries π•œ E (E[Γ—k]β†’L[π•œ] F) := fun l => + βˆ‘ s : { s : Finset (Fin (k + l)) // Finset.card s = l }, p.changeOriginSeriesTerm k l s s.2 + +theorem nnnorm_changeOriginSeries_le_tsum (k l : β„•) : + β€–p.changeOriginSeries k lβ€–β‚Š ≀ + βˆ‘' _ : { s : Finset (Fin (k + l)) // s.card = l }, β€–p (k + l)β€–β‚Š := + (nnnorm_sum_le _ (fun t => changeOriginSeriesTerm p k l (Subtype.val t) t.prop)).trans_eq <| by + simp_rw [tsum_fintype, nnnorm_changeOriginSeriesTerm (p := p) (k := k) (l := l)] + +theorem nnnorm_changeOriginSeries_apply_le_tsum (k l : β„•) (x : E) : + β€–p.changeOriginSeries k l fun _ => xβ€–β‚Š ≀ + βˆ‘' _ : { s : Finset (Fin (k + l)) // s.card = l }, β€–p (k + l)β€–β‚Š * β€–xβ€–β‚Š ^ l := by + rw [NNReal.tsum_mul_right, ← Fin.prod_const] + exact (p.changeOriginSeries k l).le_of_opNNNorm_le _ (p.nnnorm_changeOriginSeries_le_tsum _ _) + +/-- Changing the origin of a formal multilinear series `p`, so that +`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense. +-/ +def changeOrigin (x : E) : FormalMultilinearSeries π•œ E F := + fun k => (p.changeOriginSeries k).sum x + +/-- An auxiliary equivalence useful in the proofs about +`FormalMultilinearSeries.changeOriginSeries`: the set of triples `(k, l, s)`, where `s` is a +`Finset (Fin (k + l))` of cardinality `l` is equivalent to the set of pairs `(n, s)`, where `s` is a +`Finset (Fin n)`. + +The forward map sends `(k, l, s)` to `(k + l, s)` and the inverse map sends `(n, s)` to +`(n - Finset.card s, Finset.card s, s)`. The actual definition is less readable because of problems +with non-definitional equalities. -/ +@[simps] +def changeOriginIndexEquiv : + (Ξ£ k l : β„•, { s : Finset (Fin (k + l)) // s.card = l }) ≃ Ξ£ n : β„•, Finset (Fin n) where + toFun s := ⟨s.1 + s.2.1, s.2.2⟩ + invFun s := + ⟨s.1 - s.2.card, s.2.card, + ⟨s.2.map + (finCongr <| (tsub_add_cancel_of_le <| card_finset_fin_le s.2).symm).toEmbedding, + Finset.card_map _⟩⟩ + left_inv := by + rintro ⟨k, l, ⟨s : Finset (Fin <| k + l), hs : s.card = l⟩⟩ + dsimp only [Subtype.coe_mk] + -- Lean can't automatically generalize `k' = k + l - s.card`, `l' = s.card`, so we explicitly + -- formulate the generalized goal + suffices βˆ€ k' l', k' = k β†’ l' = l β†’ βˆ€ (hkl : k + l = k' + l') (hs'), + (⟨k', l', ⟨s.map (finCongr hkl).toEmbedding, hs'⟩⟩ : + Ξ£k l : β„•, { s : Finset (Fin (k + l)) // s.card = l }) = ⟨k, l, ⟨s, hs⟩⟩ by + apply this <;> simp only [hs, add_tsub_cancel_right] + rintro _ _ rfl rfl hkl hs' + simp only [Equiv.refl_toEmbedding, finCongr_refl, Finset.map_refl, eq_self_iff_true, + OrderIso.refl_toEquiv, and_self_iff, heq_iff_eq] + right_inv := by + rintro ⟨n, s⟩ + simp [tsub_add_cancel_of_le (card_finset_fin_le s), finCongr_eq_equivCast] + +lemma changeOriginSeriesTerm_changeOriginIndexEquiv_symm (n t) : + let s := changeOriginIndexEquiv.symm ⟨n, t⟩ + p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ ↦ x) (fun _ ↦ y) = + p n (t.piecewise (fun _ ↦ x) fun _ ↦ y) := by + have : βˆ€ (m) (hm : n = m), p n (t.piecewise (fun _ ↦ x) fun _ ↦ y) = + p m ((t.map (finCongr hm).toEmbedding).piecewise (fun _ ↦ x) fun _ ↦ y) := by + rintro m rfl + simp (config := { unfoldPartialApp := true }) [Finset.piecewise] + simp_rw [changeOriginSeriesTerm_apply, eq_comm]; apply this + +theorem changeOriginSeries_summable_aux₁ {r r' : ℝβ‰₯0} (hr : (r + r' : ℝβ‰₯0∞) < p.radius) : + Summable fun s : Ξ£k l : β„•, { s : Finset (Fin (k + l)) // s.card = l } => + β€–p (s.1 + s.2.1)β€–β‚Š * r ^ s.2.1 * r' ^ s.1 := by + rw [← changeOriginIndexEquiv.symm.summable_iff] + dsimp only [Function.comp_def, changeOriginIndexEquiv_symm_apply_fst, + changeOriginIndexEquiv_symm_apply_snd_fst] + have : βˆ€ n : β„•, + HasSum (fun s : Finset (Fin n) => β€–p (n - s.card + s.card)β€–β‚Š * r ^ s.card * r' ^ (n - s.card)) + (β€–p nβ€–β‚Š * (r + r') ^ n) := by + intro n + -- TODO: why `simp only [tsub_add_cancel_of_le (card_finset_fin_le _)]` fails? + convert_to HasSum (fun s : Finset (Fin n) => β€–p nβ€–β‚Š * (r ^ s.card * r' ^ (n - s.card))) _ + Β· ext1 s + rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc] + rw [← Fin.sum_pow_mul_eq_add_pow] + exact (hasSum_fintype _).mul_left _ + refine NNReal.summable_sigma.2 ⟨fun n => (this n).summable, ?_⟩ + simp only [(this _).tsum_eq] + exact p.summable_nnnorm_mul_pow hr + +theorem changeOriginSeries_summable_auxβ‚‚ (hr : (r : ℝβ‰₯0∞) < p.radius) (k : β„•) : + Summable fun s : Ξ£l : β„•, { s : Finset (Fin (k + l)) // s.card = l } => + β€–p (k + s.1)β€–β‚Š * r ^ s.1 := by + rcases ENNReal.lt_iff_exists_add_pos_lt.1 hr with ⟨r', h0, hr'⟩ + simpa only [mul_inv_cancel_rightβ‚€ (pow_pos h0 _).ne'] using + ((NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr')).1 k).mul_right (r' ^ k)⁻¹ + +theorem changeOriginSeries_summable_aux₃ {r : ℝβ‰₯0} (hr : ↑r < p.radius) (k : β„•) : + Summable fun l : β„• => β€–p.changeOriginSeries k lβ€–β‚Š * r ^ l := by + refine NNReal.summable_of_le + (fun n => ?_) (NNReal.summable_sigma.1 <| p.changeOriginSeries_summable_auxβ‚‚ hr k).2 + simp only [NNReal.tsum_mul_right] + exact mul_le_mul' (p.nnnorm_changeOriginSeries_le_tsum _ _) le_rfl + +theorem le_changeOriginSeries_radius (k : β„•) : p.radius ≀ (p.changeOriginSeries k).radius := + ENNReal.le_of_forall_nnreal_lt fun _r hr => + le_radius_of_summable_nnnorm _ (p.changeOriginSeries_summable_aux₃ hr k) + +theorem nnnorm_changeOrigin_le (k : β„•) (h : (β€–xβ€–β‚Š : ℝβ‰₯0∞) < p.radius) : + β€–p.changeOrigin x kβ€–β‚Š ≀ + βˆ‘' s : Ξ£l : β„•, { s : Finset (Fin (k + l)) // s.card = l }, β€–p (k + s.1)β€–β‚Š * β€–xβ€–β‚Š ^ s.1 := by + refine tsum_of_nnnorm_bounded ?_ fun l => p.nnnorm_changeOriginSeries_apply_le_tsum k l x + have := p.changeOriginSeries_summable_auxβ‚‚ h k + refine HasSum.sigma this.hasSum fun l => ?_ + exact ((NNReal.summable_sigma.1 this).1 l).hasSum + +/-- The radius of convergence of `p.changeOrigin x` is at least `p.radius - β€–xβ€–`. In other words, +`p.changeOrigin x` is well defined on the largest ball contained in the original ball of +convergence. -/ +theorem changeOrigin_radius : p.radius - β€–xβ€–β‚Š ≀ (p.changeOrigin x).radius := by + refine ENNReal.le_of_forall_pos_nnreal_lt fun r _h0 hr => ?_ + rw [lt_tsub_iff_right, add_comm] at hr + have hr' : (β€–xβ€–β‚Š : ℝβ‰₯0∞) < p.radius := (le_add_right le_rfl).trans_lt hr + apply le_radius_of_summable_nnnorm + have : βˆ€ k : β„•, + β€–p.changeOrigin x kβ€–β‚Š * r ^ k ≀ + (βˆ‘' s : Ξ£l : β„•, { s : Finset (Fin (k + l)) // s.card = l }, β€–p (k + s.1)β€–β‚Š * β€–xβ€–β‚Š ^ s.1) * + r ^ k := + fun k => mul_le_mul_right' (p.nnnorm_changeOrigin_le k hr') (r ^ k) + refine NNReal.summable_of_le this ?_ + simpa only [← NNReal.tsum_mul_right] using + (NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr)).2 + +/-- `derivSeries p` is a power series for `fderiv π•œ f` if `p` is a power series for `f`, +see `HasFPowerSeriesOnBall.fderiv`. -/ +def derivSeries : FormalMultilinearSeries π•œ E (E β†’L[π•œ] F) := + (continuousMultilinearCurryFin1 π•œ E F : (E[Γ—1]β†’L[π•œ] F) β†’L[π•œ] E β†’L[π•œ] F) + |>.compFormalMultilinearSeries (p.changeOriginSeries 1) + +end + +-- From this point on, assume that the space is complete, to make sure that series that converge +-- in norm also converge in `F`. +variable [CompleteSpace F] (p : FormalMultilinearSeries π•œ E F) {x y : E} {r R : ℝβ‰₯0} + +theorem hasFPowerSeriesOnBall_changeOrigin (k : β„•) (hr : 0 < p.radius) : + HasFPowerSeriesOnBall (fun x => p.changeOrigin x k) (p.changeOriginSeries k) 0 p.radius := + have := p.le_changeOriginSeries_radius k + ((p.changeOriginSeries k).hasFPowerSeriesOnBall (hr.trans_le this)).mono hr this + +/-- Summing the series `p.changeOrigin x` at a point `y` gives back `p (x + y)`. -/ +theorem changeOrigin_eval (h : (β€–xβ€–β‚Š + β€–yβ€–β‚Š : ℝβ‰₯0∞) < p.radius) : + (p.changeOrigin x).sum y = p.sum (x + y) := by + have radius_pos : 0 < p.radius := lt_of_le_of_lt (zero_le _) h + have x_mem_ball : x ∈ EMetric.ball (0 : E) p.radius := + mem_emetric_ball_zero_iff.2 ((le_add_right le_rfl).trans_lt h) + have y_mem_ball : y ∈ EMetric.ball (0 : E) (p.changeOrigin x).radius := by + refine mem_emetric_ball_zero_iff.2 (lt_of_lt_of_le ?_ p.changeOrigin_radius) + rwa [lt_tsub_iff_right, add_comm] + have x_add_y_mem_ball : x + y ∈ EMetric.ball (0 : E) p.radius := by + refine mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt ?_ h) + exact mod_cast nnnorm_add_le x y + set f : (Ξ£ k l : β„•, { s : Finset (Fin (k + l)) // s.card = l }) β†’ F := fun s => + p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ => x) fun _ => y + have hsf : Summable f := by + refine .of_nnnorm_bounded _ (p.changeOriginSeries_summable_aux₁ h) ?_ + rintro ⟨k, l, s, hs⟩ + dsimp only [Subtype.coe_mk] + exact p.nnnorm_changeOriginSeriesTerm_apply_le _ _ _ _ _ _ + have hf : HasSum f ((p.changeOrigin x).sum y) := by + refine HasSum.sigma_of_hasSum ((p.changeOrigin x).summable y_mem_ball).hasSum (fun k => ?_) hsf + Β· dsimp only [f] + refine ContinuousMultilinearMap.hasSum_eval ?_ _ + have := (p.hasFPowerSeriesOnBall_changeOrigin k radius_pos).hasSum x_mem_ball + rw [zero_add] at this + refine HasSum.sigma_of_hasSum this (fun l => ?_) ?_ + Β· simp only [changeOriginSeries, ContinuousMultilinearMap.sum_apply] + apply hasSum_fintype + Β· refine .of_nnnorm_bounded _ + (p.changeOriginSeries_summable_auxβ‚‚ (mem_emetric_ball_zero_iff.1 x_mem_ball) k) + fun s => ?_ + refine (ContinuousMultilinearMap.le_opNNNorm _ _).trans_eq ?_ + simp + refine hf.unique (changeOriginIndexEquiv.symm.hasSum_iff.1 ?_) + refine HasSum.sigma_of_hasSum + (p.hasSum x_add_y_mem_ball) (fun n => ?_) (changeOriginIndexEquiv.symm.summable_iff.2 hsf) + erw [(p n).map_add_univ (fun _ => x) fun _ => y] + simp_rw [← changeOriginSeriesTerm_changeOriginIndexEquiv_symm] + exact hasSum_fintype (fun c => f (changeOriginIndexEquiv.symm ⟨n, c⟩)) + +/-- Power series terms are analytic as we vary the origin -/ +theorem analyticAt_changeOrigin (p : FormalMultilinearSeries π•œ E F) (rp : p.radius > 0) (n : β„•) : + AnalyticAt π•œ (fun x ↦ p.changeOrigin x n) 0 := + (FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin p n rp).analyticAt + +end FormalMultilinearSeries + +section + +variable [CompleteSpace F] {f : E β†’ F} {p : FormalMultilinearSeries π•œ E F} {x y : E} {r : ℝβ‰₯0∞} + +/-- If a function admits a power series expansion `p` on a ball `B (x, r)`, then it also admits a +power series on any subball of this ball (even with a different center), given by `p.changeOrigin`. +-/ +theorem HasFPowerSeriesOnBall.changeOrigin (hf : HasFPowerSeriesOnBall f p x r) + (h : (β€–yβ€–β‚Š : ℝβ‰₯0∞) < r) : HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - β€–yβ€–β‚Š) := + { r_le := by + apply le_trans _ p.changeOrigin_radius + exact tsub_le_tsub hf.r_le le_rfl + r_pos := by simp [h] + hasSum := fun {z} hz => by + have : f (x + y + z) = + FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z := by + rw [mem_emetric_ball_zero_iff, lt_tsub_iff_right, add_comm] at hz + rw [p.changeOrigin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum] + refine mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt ?_ hz) + exact mod_cast nnnorm_add_le y z + rw [this] + apply (p.changeOrigin y).hasSum + refine EMetric.ball_subset_ball (le_trans ?_ p.changeOrigin_radius) hz + exact tsub_le_tsub hf.r_le le_rfl } + +/-- If a function admits a power series expansion `p` on an open ball `B (x, r)`, then +it is analytic at every point of this ball. -/ +theorem HasFPowerSeriesOnBall.analyticAt_of_mem (hf : HasFPowerSeriesOnBall f p x r) + (h : y ∈ EMetric.ball x r) : AnalyticAt π•œ f y := by + have : (β€–y - xβ€–β‚Š : ℝβ‰₯0∞) < r := by simpa [edist_eq_coe_nnnorm_sub] using h + have := hf.changeOrigin this + rw [add_sub_cancel] at this + exact this.analyticAt + +theorem HasFPowerSeriesOnBall.analyticOn (hf : HasFPowerSeriesOnBall f p x r) : + AnalyticOn π•œ f (EMetric.ball x r) := + fun _y hy => hf.analyticAt_of_mem hy + +variable (π•œ f) in +/-- For any function `f` from a normed vector space to a Banach space, the set of points `x` such +that `f` is analytic at `x` is open. -/ +theorem isOpen_analyticAt : IsOpen { x | AnalyticAt π•œ f x } := by + rw [isOpen_iff_mem_nhds] + rintro x ⟨p, r, hr⟩ + exact mem_of_superset (EMetric.ball_mem_nhds _ hr.r_pos) fun y hy => hr.analyticAt_of_mem hy + +theorem AnalyticAt.eventually_analyticAt (h : AnalyticAt π•œ f x) : + βˆ€αΆ  y in 𝓝 x, AnalyticAt π•œ f y := + (isOpen_analyticAt π•œ f).mem_nhds h + +theorem AnalyticAt.exists_mem_nhds_analyticOn (h : AnalyticAt π•œ f x) : + βˆƒ s ∈ 𝓝 x, AnalyticOn π•œ f s := + h.eventually_analyticAt.exists_mem + +/-- If we're analytic at a point, we're analytic in a nonempty ball -/ +theorem AnalyticAt.exists_ball_analyticOn (h : AnalyticAt π•œ f x) : + βˆƒ r : ℝ, 0 < r ∧ AnalyticOn π•œ f (Metric.ball x r) := + Metric.isOpen_iff.mp (isOpen_analyticAt _ _) _ h + +end diff --git a/Mathlib/Analysis/Analytic/Uniqueness.lean b/Mathlib/Analysis/Analytic/Uniqueness.lean index b18db8f4e34b7..d626ccca6a55a 100644 --- a/Mathlib/Analysis/Analytic/Uniqueness.lean +++ b/Mathlib/Analysis/Analytic/Uniqueness.lean @@ -6,6 +6,7 @@ Authors: SΓ©bastien GouΓ«zel import Mathlib.Analysis.Analytic.Linear import Mathlib.Analysis.Analytic.Composition import Mathlib.Analysis.Normed.Module.Completion +import Mathlib.Analysis.Analytic.ChangeOrigin /-! # Uniqueness principle for analytic functions diff --git a/Mathlib/Analysis/Normed/Algebra/Exponential.lean b/Mathlib/Analysis/Normed/Algebra/Exponential.lean index 3a6c07c945357..e211c1cfd4a8d 100644 --- a/Mathlib/Analysis/Normed/Algebra/Exponential.lean +++ b/Mathlib/Analysis/Normed/Algebra/Exponential.lean @@ -3,7 +3,7 @@ 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 -/ -import Mathlib.Analysis.Analytic.Basic +import Mathlib.Analysis.Analytic.ChangeOrigin import Mathlib.Analysis.Complex.Basic import Mathlib.Data.Nat.Choose.Cast