OneStepAssembly

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

The triangle assembly: the deterministic one-step contraction

This module proves the third display of the proof of l.excess.decay.good.scales,

  E(u,U_k) ≤ C 3^{-k/2} E(u,U_0) + C 3^{(d/2+1)k} 3^{-n} ‖u-v‖_{L²(U_2)}
              + C 3^{(n-k)/2} [∇h]_{C^{0,1/2}(U_0)} 1_{bd} ,

as one pathwise, real-valued, coefficient-free theorem (excessDecay_oneStep_triangle_of_schauder) on the truncated window family U_j = (x+□_{n-j}) ∩ □_m.

The single remaining input: the Schauder obligation

The theorem takes the Schauder conclusion as an explicit, disclosingly named hypothesis:

  hschauder :  K  ≤  Csch · (3^{-n})^{1/2} · E(v, U_2)  +  Kh

where K is the C^{0,1/2} seminorm bound of ∇v on U_3 and Kh is the boundary-datum leg C [∇h]_{C^{0,1/2}(U_2)} 1_{bd}. Nothing else in this module is assumed: the harmonicity of v is not used, and every other leg is proved.

The three legs, and where each constant comes from

• taylorContractionConst d · Csch · windowRatioConst d 2 · (3^{-k})^{1/2} on E(u,U_0) — the printed^{-k/2}. taylorContractionConstis the affine-competitor constant ofOneStepCompetitor, windowRatioConst d 2the excess quasi-monotonicityE(u,U_2) ≤ κ E(u,U_0)ofOneStepWindows`.
• triangleRemainderConst d Csch k · 3^{-n} on ‖u-v‖_{L²(U_2)}, with `triangleRemainderConst d Csch k = 81 · taylorContractionConst d · Csch
  • 9 · 3^k · √((3^k)^d). Since √((3^k)^d) = 3^{kd/2}, this is the printed^{(1+d/2)k} exactly (the 81 and 9 are the aspect-1/9 slacks of the two truncated normalizers, which the printed proof does not display).
• taylorContractionConst d · (3^{n-k})^{1/2} on Kh — the printed C 3^{(n-k)/2} [∇h]_{C^{0,1/2}}.

1. Two small 3-power identities

2. Restriction of the gradient carrier

HasGradientOn.mono_set now lives with its carrier in Algsuperdiff/Section4/Support/ClassicalGradient.lean; the duplicate copy that used to sit here was deleted with the AffineSplitLift re-point.

3. The assembled constant

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.triangleRemainderConst (d : ℕ) (Csch : ℝ) (k : ℕ) : ℝ

The remainder constant of the assembly: 81 C_taylor Csch + 9·3^k·√((3^k)^d), i.e. the printed C 3^{(1+d/2)k}.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.triangleRemainderConst d Csch k = 81 * Algsuperdiff.Section4.Provider.ExcessDecay.taylorContractionConst d * Csch + 9 * 3 ^ ↑k * √((3 ^ ↑k) ^ d)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.triangleRemainderConst_nonneg (d : ℕ) {Csch : ℝ} (hCsch : 0 ≤ Csch) (k : ℕ) : 0 ≤ triangleRemainderConst d Csch k

4. The assembly

theorem Algsuperdiff.Section4.Provider.ExcessDecay.excessDecay_oneStep_triangle_of_schauder {d : ℕ} (hd : d ≠ 0) {m n : ℤ} {k : ℕ} (hk : 3 ≤ k) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n - 1 ≤ m) {u v : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (truncatedWindow x m n))) (hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict (truncatedWindow x m n))) {Gv : HCPolySupport.Vec d → HCPolySupport.Vec d} {K Kh Csch : ℝ} (hK : 0 ≤ K) (hCsch : 0 ≤ Csch) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => Gv p i) (truncatedWindow x m (n - 3)) MeasureTheory.volume) (hgrad : Support.HasGradientOn (truncatedWindow x m (n - 3)) v Gv) (hhol : Support.HolderSeminormBoundOn (truncatedWindow x m (n - 3)) (1 / 2) K Gv) (hschauder : K ≤ Csch * (3 ^ (-n)) ^ (1 / 2) * Support.affineExcess (truncatedWindow x m (n - 2)) v + Kh) : Support.affineExcess (truncatedWindow x m (n - ↑k)) u ≤ taylorContractionConst d * Csch * windowRatioConst d 2 * (3 ^ (-↑k)) ^ (1 / 2) * Support.affineExcess (truncatedWindow x m n) u + triangleRemainderConst d Csch k * (3 ^ (-n) * Support.normalizedL2On (truncatedWindow x m (n - 2)) fun (y : HCPolySupport.Vec d) => u y - v y) + taylorContractionConst d * (3 ^ (n - ↑k)) ^ (1 / 2) * Kh

The triangle assembly, deterministic form.

Given the affine competitor's C^{1,1/2} data on U_3, the Schauder bound hschauder on its gradient-Hölder constant, and nothing else, the excess of u on U_k contracts:

  E(u,U_k) ≤ C_t Csch κ (3^{-k})^{1/2} E(u,U_0)
              + (81 C_t Csch + 9·3^k √((3^k)^d)) · 3^{-n} ‖u-v‖_{L²(U_2)}
              + C_t (3^{n-k})^{1/2} Kh .