eventually_hasSum_of_comp — Mathlib

English

Symmetric sum preserves a lower bound on the radius; min radius of components controls the radius of sum.

Русский

Симметрическая сумма сохраняет нижнюю границу радиуса; мин радиус компонентов задаёт радиус суммы.

LaTeX

$$$\\min(radius(p), radius(-p)) \\le radius(p+(-p))$$$

Lean4

theorem eventually_hasSum_of_comp {f : E → F} {g : F → G} {q : FormalMultilinearSeries 𝕜 F G}
    {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x)
    (hf : HasFPowerSeriesAt f p x) (hq : 0 < q.radius) :
    ∀ᶠ y in 𝓝 0, HasSum (fun n : ℕ => q n fun _ : Fin n => (f (x + y) - f x)) (g (f (x + y))) :=
  by
  have : ∀ᶠ y in 𝓝 (0 : E), f (x + y) - f x ∈ EMetric.ball 0 q.radius :=
    by
    have A : ContinuousAt (fun y ↦ f (x + y) - f x) 0 :=
      by
      apply ContinuousAt.sub _ continuousAt_const
      exact hf.continuousAt.comp_of_eq (continuous_add_left x).continuousAt (by simp)
    have B : EMetric.ball 0 q.radius ∈ 𝓝 (f (x + 0) - f x) := by simpa using EMetric.ball_mem_nhds _ hq
    exact A.preimage_mem_nhds B
  filter_upwards [hgf.tendsto_partialSum_prod_of_comp hq (hf.radius_pos), hf.tendsto_partialSum, this] with y hy h'y
    h''y
  have L : Tendsto (fun n ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y)))) :=
    by
    apply (closed_nhds_basis (g (f (x + y)))).tendsto_right_iff.2
    rintro u ⟨hu, u_closed⟩
    simp only [id_eq, eventually_atTop, ge_iff_le]
    rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
    obtain ⟨a₀, b₀, hab⟩ :
      ∃ a₀ b₀, ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b → q.partialSum a (p.partialSum b y - (p 0) fun _ ↦ 0) ∈ v := by
      simpa using hy (v_open.mem_nhds hv)
    refine ⟨a₀, fun a ha ↦ ?_⟩
    have :
      Tendsto (fun b ↦ q.partialSum a (p.partialSum b y - (p 0) fun _ ↦ 0)) atTop
        (𝓝 (q.partialSum a (f (x + y) - f x))) :=
      by
      have : ContinuousAt (q.partialSum a) (f (x + y) - f x) := (partialSum_continuous q a).continuousAt
      apply this.tendsto.comp
      apply Tendsto.sub h'y
      convert tendsto_const_nhds
      exact (HasFPowerSeriesAt.coeff_zero hf fun _ ↦ 0).symm
    apply u_closed.mem_of_tendsto this
    filter_upwards [Ici_mem_atTop b₀] with b hb using vu (hab _ _ ha hb)
  have C : CauchySeq (fun (s : Finset ℕ) ↦ ∑ n ∈ s, q n fun _ : Fin n => (f (x + y) - f x)) :=
    by
    have Z := q.summable_norm_apply (x := f (x + y) - f x) h''y
    exact cauchySeq_finset_of_norm_bounded Z (fun i ↦ le_rfl)
  exact tendsto_nhds_of_cauchySeq_of_subseq C tendsto_finset_range L

Похожие утверждения