IterationSeries

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

The perturbation iteration as a sequence

One step of the perturbation iteration on the cube y + □_n is IterationStep.lean: from an increment w_j with a continuous representative of 1/2-Hölder seminorm at most K_j it produces the Laplace solution h_j forced by w_j ∇ · k and the next increment w_{j+1} solving the rough-field problem with datum ∇ h_j, together with the good-event bound on the seminorm of w_{j+1}.

Iterating that step needs the supremum bound ‖w_j‖_{L^∞} ≤ 3^{n/2} [w_j], which holds because each increment has zero trace on the cube, and needs the seminorm bound of the output to be of the same shape as the input's, which is where the contraction hypothesis enters: as soon as

  2 C_reg σ_n^{-1} 3^n C (‖∇·k‖_{L^∞} + 3^{n/2} [∇·k]_{1/2}) ≤ ρ ,

the seminorms obey K_{j+1} ≤ ρ K_j, so the whole sequence exists with K_j = K_0 ρ^j. The recursion is carried by a state carrying the increment, its representative, its seminorm bound and its zero-trace witness, so that the step can be applied again.

Main results

• rpow_three_neg_half_eq_inv — the power of three the normalization uses.
• sup_le_of_zeroTrace — the supremum of a zero-trace increment on the cube.
• exists_iterationSequence — the sequence of increments and Laplace solutions, with the geometric seminorm bound and the geometric supremum bound on the gradients of the Laplace solutions.

References

• ABK26, the iteration scheme of the proof of the injection estimate of Section 5.1.

1. Two elementary steps

theorem Algsuperdiff.Section5.Provider.rpow_three_neg_half_eq_inv (n : ℤ) : Real.rpow 3 (-↑n / 2) = (Real.rpow 3 (↑n / 2))⁻¹

3^{-n/2} = (3^{n/2})⁻¹.

theorem Algsuperdiff.Section5.Provider.sup_le_of_zeroTrace {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} (hd : 0 < d) {v : HCPolySupport.H1Function (Support.cubeSetAt y n)} {vRep : HCPolySupport.Vec d → ℝ} {K : ℝ} (hK0 : 0 ≤ K) (hzero : ∃ (z : HCPolySupport.H10Function (Support.cubeSetAt y n)), ∀ (x : HCPolySupport.Vec d), v.toFun x = z.toFun x) (hrep : Support.IsCubeRepresentative y n v vRep) (hKb : Section4.Support.HolderSeminormBoundOn (Support.cubeSetAt y n) (1 / 2) K vRep) (x : HCPolySupport.Vec d) : x ∈ Support.cubeSetAt y n → ‖vRep x‖ ≤ Real.rpow 3 (↑n / 2) * K

The supremum of a zero-trace increment on the cube, from its own Hölder seminorm.

2. The state of the iteration

3. The sequence produced by the step

theorem Algsuperdiff.Section5.Provider.exists_iterationSequence {d : ℕ} (hdim : 2 ≤ d) : ∃ (CIter : ℝ), 0 < CIter ∧ ∀ (M : Section3.ABKModel d) (Creg : ℝ), 0 ≤ Creg → ∀ (n : ℤ) (y : HCPolySupport.Vec d) (ep : ℝ), ∀ omega ∈ Support.goodCubeEvent M Creg n y ep, ∀ (k : HCPolySupport.Vec d → HCPolySupport.Mat d), (∀ (p q : Fin d), ContDiff ℝ 1 fun (x : HCPolySupport.Vec d) => k x p q) → (∀ (x : HCPolySupport.Vec d), HCPolySupport.matTranspose (k x) = -k x) → ∀ (Kk Sk : ℝ), Section4.Support.HolderSeminormBoundOn (Support.cubeSetAt y n) (1 / 2) Kk (Support.matFieldDiv k) → (∀ x ∈ Support.cubeSetAt y n, ‖Support.matFieldDiv k x‖ ≤ Sk) → ∀ (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (w0 : HCPolySupport.H1Function (Support.cubeSetAt y n)) (w0Rep : HCPolySupport.Vec d → ℝ) (K0 rho : ℝ), 0 ≤ K0 → 0 ≤ rho → Support.IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu n omega).toCoeffField y n w0 g → Support.IsCubeRepresentative y n w0 w0Rep → Section4.Support.HolderSeminormBoundOn (Support.cubeSetAt y n) (1 / 2) K0 w0Rep → 2 * Creg * (↑(Section3.Annealed.sigmaBar M n))⁻¹ * Real.rpow 3 ↑n * CIter * (Sk + Real.rpow 3 (↑n / 2) * Kk) ≤ rho → ∃ (w : ℕ → HCPolySupport.H1Function (Support.cubeSetAt y n)) (wRep : ℕ → HCPolySupport.Vec d → ℝ) (lap : ℕ → HCPolySupport.H1Function (Support.cubeSetAt y n)), w 0 = w0 ∧ (∀ (j : ℕ), Support.IsCubeRepresentative y n (w j) (wRep j)) ∧ (∀ (j : ℕ), ∃ (z : HCPolySupport.H10Function (Support.cubeSetAt y n)), ∀ (x : HCPolySupport.Vec d), (w j).toFun x = z.toFun x) ∧ (∀ (j : ℕ), Section4.Support.HolderSeminormBoundOn (Support.cubeSetAt y n) (1 / 2) (K0 * rho ^ j) (wRep j)) ∧ (∀ (j : ℕ), Support.IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => 1 • 1) y n (lap j) fun (x : HCPolySupport.Vec d) => -HCPolySupport.matVecMul (k x) ((w j).grad x)) ∧ (∀ (j : ℕ), ∀ x ∈ Support.cubeSetAt y n, ‖(lap j).grad x‖ ≤ CIter * Real.rpow 3 (↑n / 2) * K0 * (Sk + Real.rpow 3 (↑n / 2) * Kk) * rho ^ j) ∧ ∀ (j : ℕ), Support.IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu n omega).toCoeffField y n (w (j + 1)) (lap j).grad

The perturbation iteration, as a sequence of increments.

On the good cube event, and under the contraction hypothesis, the step of IterationStep.lean can be applied indefinitely: the 1/2-Hölder seminorms of the continuous representatives decay geometrically with ratio ρ, and so do the supremum norms of the gradients of the intermediate Laplace solutions.