SeriesLimit

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

From a geometrically decaying series of representatives to a continuous limit

The perturbation iteration produces zero-trace increments w_j whose continuous representatives obey [w_j]_{C^{0,1/2}(y+□_n)} ≤ K_0 ρ^j with ρ < 1. Because each increment vanishes on the boundary of the cube, its supremum norm is controlled by its own Hölder seminorm, so the series of representatives converges absolutely and uniformly on the cube. Its sum is continuous, carries the summed Hölder bound, and — since the partial sums converge in L² to a prescribed H¹ function — is a continuous representative of that function.

This is the step that turns the C^{0,1/2} contraction into a statement about the solution itself: the Hölder bound of the limit is inherited from the uniform bound on the partial sums, and the identification of the limit is the L² convergence of the series identification.

Main results

• isCubeRepresentative_partialSum — a finite sum of representatives represents the partial sum.
• exists_isCubeRepresentative_of_tendsto — the limit representative, its Hölder bound, and the Hölder bound of the tail after the first term.

References

• ABK26, the summation of the iteration series in the proof of the injection estimate of Section 5.1.

1. Representatives of finite sums

theorem Algsuperdiff.Section5.Provider.isCubeRepresentative_partialSum {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {w : ℕ → HCPolySupport.H1Function (Support.cubeSetAt y n)} {wRep : ℕ → HCPolySupport.Vec d → ℝ} (hrep : ∀ (j : ℕ), Support.IsCubeRepresentative y n (w j) (wRep j)) (J : ℕ) : Support.IsCubeRepresentative y n (Support.iterationPartialSum w J) fun (x : HCPolySupport.Vec d) => ∑ j ∈ Finset.range (J + 1), wRep j x

A finite sum of representatives represents the partial sum.

2. The limit of the series of representatives

noncomputable def Algsuperdiff.Section5.Provider.seriesTail {d : ℕ} (wRep : ℕ → HCPolySupport.Vec d → ℝ) (k : ℕ) (x : HCPolySupport.Vec d) : ℝ

The tail of the series of representatives, as a function on the cube.

Equations

• Algsuperdiff.Section5.Provider.seriesTail wRep k x = ∑' (j : ℕ), wRep (j + k) x

theorem Algsuperdiff.Section5.Provider.exists_isCubeRepresentative_of_tendsto {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {w : ℕ → HCPolySupport.H1Function (Support.cubeSetAt y n)} {wRep : ℕ → HCPolySupport.Vec d → ℝ} {K0 rho : ℝ} (hd : 0 < d) (hK0 : 0 ≤ K0) (hrho0 : 0 ≤ rho) (hrho1 : rho < 1) (hrep : ∀ (j : ℕ), Support.IsCubeRepresentative y n (w j) (wRep j)) (hzero : ∀ (j : ℕ), ∃ (z : HCPolySupport.H10Function (Support.cubeSetAt y n)), ∀ (x : HCPolySupport.Vec d), (w j).toFun x = z.toFun x) (hK : ∀ (j : ℕ), Section4.Support.HolderSeminormBoundOn (Support.cubeSetAt y n) (1 / 2) (K0 * rho ^ j) (wRep j)) {u : HCPolySupport.H1Function (Support.cubeSetAt y n)} (hlim : Filter.Tendsto (fun (J : ℕ) => √(∫ (x : HCPolySupport.Vec d) in Support.cubeSetAt y n, (u.toFun x - (Support.iterationPartialSum w J).toFun x) ^ 2)) Filter.atTop (nhds 0)) : ∃ (uRep : HCPolySupport.Vec d → ℝ), Support.IsCubeRepresentative y n u uRep ∧ Section4.Support.HolderSeminormBoundOn (Support.cubeSetAt y n) (1 / 2) (K0 / (1 - rho)) uRep ∧ Section4.Support.HolderSeminormBoundOn (Support.cubeSetAt y n) (1 / 2) (K0 * rho / (1 - rho)) fun (x : HCPolySupport.Vec d) => uRep x - wRep 0 x

The sum of the series of representatives is a continuous representative of the L² limit of the partial sums, with the summed Hölder bound, and its distance to the first term carries the tail bound.