Lean4
/-- If two functions `g` and `f` have power series `q` and `p` respectively at `f x` and `x`, within
two sets `s` and `t` such that `f` maps `s` to `t`, then `g ∘ f` admits the power
series `q.comp p` at `x` within `s`. -/
theorem comp {g : F → G} {f : E → F} {q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
{t : Set F} {s : Set E} (hg : HasFPowerSeriesWithinAt g q t (f x)) (hf : HasFPowerSeriesWithinAt f p s x)
(hs : Set.MapsTo f s t) : HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x := by
/- Consider `rf` and `rg` such that `f` and `g` have power series expansion on the disks
of radius `rf` and `rg`. -/
rcases hg with ⟨rg, Hg⟩
rcases hf with
⟨rf, Hf⟩
-- The terms defining `q.comp p` are geometrically summable in a disk of some radius `r`.
rcases q.comp_summable_nnreal p Hg.radius_pos Hf.radius_pos with
⟨r, r_pos : 0 < r, hr⟩
/- We will consider `y` which is smaller than `r` and `rf`, and also small enough that
`f (x + y)` is close enough to `f x` to be in the disk where `g` is well behaved. Let
`min (r, rf, δ)` be this new radius. -/
obtain ⟨δ, δpos, hδ⟩ :
∃ δ : ℝ≥0∞, 0 < δ ∧ ∀ {z : E}, z ∈ insert x s ∩ EMetric.ball x δ → f z ∈ insert (f x) t ∩ EMetric.ball (f x) rg :=
by
have : insert (f x) t ∩ EMetric.ball (f x) rg ∈ 𝓝[insert (f x) t] (f x) :=
by
apply inter_mem_nhdsWithin
exact EMetric.ball_mem_nhds _ Hg.r_pos
have := Hf.analyticWithinAt.continuousWithinAt_insert.tendsto_nhdsWithin (hs.insert x) this
rcases EMetric.mem_nhdsWithin_iff.1 this with ⟨δ, δpos, Hδ⟩
exact ⟨δ, δpos, fun {z} hz => Hδ (by rwa [Set.inter_comm])⟩
let rf' := min rf δ
have min_pos : 0 < min rf' r := by
simp only [rf', r_pos, Hf.r_pos, δpos, lt_min_iff, ENNReal.coe_pos, and_self_iff]
/- We will show that `g ∘ f` admits the power series `q.comp p` in the disk of
radius `min (r, rf', δ)`. -/
refine ⟨min rf' r, ?_⟩
refine
⟨le_trans (min_le_right rf' r) (FormalMultilinearSeries.le_comp_radius_of_summable q p r hr), min_pos,
fun {y} h'y hy ↦ ?_⟩
/- Let `y` satisfy `‖y‖ < min (r, rf', δ)`. We want to show that `g (f (x + y))` is the sum of
`q.comp p` applied to `y`. -/
-- First, check that `y` is small enough so that estimates for `f` and `g` apply.
have y_mem : y ∈ EMetric.ball (0 : E) rf :=
(EMetric.ball_subset_ball (le_trans (min_le_left _ _) (min_le_left _ _))) hy
have fy_mem : f (x + y) ∈ insert (f x) t ∩ EMetric.ball (f x) rg :=
by
apply hδ
have : y ∈ EMetric.ball (0 : E) δ := (EMetric.ball_subset_ball (le_trans (min_le_left _ _) (min_le_right _ _))) hy
simpa [-Set.mem_insert_iff, edist_eq_enorm_sub, h'y]
/- Now the proof starts. To show that the sum of `q.comp p` at `y` is `g (f (x + y))`,
we will write `q.comp p` applied to `y` as a big sum over all compositions.
Since the sum is summable, to get its convergence it suffices to get
the convergence along some increasing sequence of sets.
We will use the sequence of sets `compPartialSumTarget 0 n n`,
along which the sum is exactly the composition of the partial sums of `q` and `p`, by design.
To show that it converges to `g (f (x + y))`, pointwise convergence would not be enough,
but we have uniform convergence to save the day. -/
-- First step: the partial sum of `p` converges to `f (x + y)`.
have A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, p a fun _ ↦ y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x)) :=
by
apply Tendsto.prodMk tendsto_id
have L : ∀ᶠ n in atTop, (∑ a ∈ Finset.range n, p a fun _b ↦ y) - f x = ∑ a ∈ Finset.Ico 1 n, p a fun _b ↦ y :=
by
rw [eventually_atTop]
refine ⟨1, fun n hn => ?_⟩
symm
rw [eq_sub_iff_add_eq', Finset.range_eq_Ico, ← Hf.coeff_zero fun _i => y, Finset.sum_eq_sum_Ico_succ_bot hn]
have : Tendsto (fun n => (∑ a ∈ Finset.range n, p a fun _b => y) - f x) atTop (𝓝 (f (x + y) - f x)) :=
(Hf.hasSum h'y y_mem).tendsto_sum_nat.sub tendsto_const_nhds
exact Tendsto.congr' L this
have B : Tendsto (fun n => q.partialSum n (∑ a ∈ Finset.Ico 1 n, p a fun _b ↦ y)) atTop (𝓝 (g (f (x + y)))) := by
-- we use the fact that the partial sums of `q` converge to `g (f (x + y))`, uniformly on a
-- neighborhood of `f (x + y)`.
have :
Tendsto (fun (z : ℕ × F) ↦ q.partialSum z.1 z.2) (atTop ×ˢ 𝓝 (f (x + y) - f x))
(𝓝 (g (f x + (f (x + y) - f x)))) :=
by
apply Hg.tendsto_partialSum_prod (y := f (x + y) - f x)
· simpa [edist_eq_enorm_sub] using fy_mem.2
· simpa using fy_mem.1
simpa using this.comp A
have C :
Tendsto (fun n => ∑ i ∈ compPartialSumTarget 0 n n, q.compAlongComposition p i.2 fun _j => y) atTop
(𝓝 (g (f (x + y)))) :=
by simpa [comp_partialSum] using B
have D : HasSum (fun i : Σ n, Composition n => q.compAlongComposition p i.2 fun _j => y) (g (f (x + y))) :=
haveI cau : CauchySeq fun s : Finset (Σ n, Composition n) => ∑ i ∈ s, q.compAlongComposition p i.2 fun _j => y :=
by
apply cauchySeq_finset_of_norm_bounded (NNReal.summable_coe.2 hr) _
simp only [coe_nnnorm, NNReal.coe_mul, NNReal.coe_pow]
rintro ⟨n, c⟩
calc
‖(compAlongComposition q p c) fun _j : Fin n => y‖ ≤ ‖compAlongComposition q p c‖ * ∏ _j : Fin n, ‖y‖ := by
apply ContinuousMultilinearMap.le_opNorm
_ ≤ ‖compAlongComposition q p c‖ * (r : ℝ) ^ n :=
by
rw [Finset.prod_const, Finset.card_fin]
gcongr
rw [EMetric.mem_ball, edist_zero_eq_enorm] at hy
have := le_trans (le_of_lt hy) (min_le_right _ _)
rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
tendsto_nhds_of_cauchySeq_of_subseq cau compPartialSumTarget_tendsto_atTop C
have E : HasSum (fun n => (q.comp p) n fun _j => y) (g (f (x + y))) :=
by
apply D.sigma
intro n
simp only [compAlongComposition_apply, FormalMultilinearSeries.comp, ContinuousMultilinearMap.sum_apply]
exact hasSum_fintype _
rw [Function.comp_apply]
exact E
