OneStepDatumSplit

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

The datum reduction: from the true competitor to an odd one

The manuscript's boundary Schauder step reads

  [∇v]_{C^{0,1/2}(U₃)} ≤ C 3^{-n/2} E(v, U₂)
                          + C [∇h]_{C^{0,1/2}(U₂)} 𝟙_{(x+□_n) ∩ ∂□_m ≠ ∅} ,

refuted the reading of that second leg as a pricing of the odd-class defect and located it here instead, in the reduction from the true competitor to an odd one. This module proves the reduction's two quantitative atoms.

1. The datum's deviation from its affine part

AffineSplitLift.abs_sub_affineLift_volumeAverage_le prices h - ℓ_h on a convex window of sup-radius r by 2 d [∇h]_{C^{0,1/2}} r^{3/2}. Instantiated at U₂ = (x + □_{n-2}) ∩ □_m and r = 3^{n-2}/2 this is

  ‖h - ℓ_h‖_{L^∞(U₂)} ≤ 2 d [∇h]_{C^{0,1/2}(U₂)} (3^{n-2}/2)^{3/2}
                      =: datumResidualBound d n [∇h] .

The integrability slot that lemma carries for the gradient field is derived here, not assumed: a C^{0,1/2} field on a window is continuous (continuousOn_of_holderSeminormBoundOn) and bounded, hence integrable.

2. The corrector carrying that deviation

ResidualCorrectorExistence.exists_residualCorrector_truncatedWindow solves the Dirichlet problem on U₂ with that datum and BoundaryLaneMaxPrinciple.ae_abs_le_of_isWeaklyHarmonicOn bounds the solution by the same constant. The output w is the manuscript's v₁:

  v₁ weakly harmonic on U₂,  ‖v₁‖_{L^∞(U₂)} ≤ datumResidualBound d n [∇h] ,

with v - ℓ_h - v₁ carrying zero data on the met portion of ∂□_m — the odd competitor the/ producer consumes.

3. Where the [∇h] leg proves (measured)

The corrector is not priced through a gradient-Hölder seminorm: no interior estimate reaches the met face, and a boundary Schauder estimate for v₁ would be circular. It is priced through the L² comparison slot instead, and the measured leg is

  3^{-n} · datumResidualBound d n [∇h] = (2 d · 3^{-3} · 2^{-3/2}) (3^n)^{1/2} [∇h] ,

1. A C^{0,1/2} field on a window is continuous and integrable

theorem Algsuperdiff.Section4.Provider.ExcessDecay.continuousOn_of_holderSeminormBoundOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} {K : ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hK : 0 ≤ K) (hG : Support.HolderSeminormBoundOn U (1 / 2) K G) : ContinuousOn G U

A Hölder field is continuous on its window. The C^{0,1/2} bound is an explicit modulus of continuity.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.integrableOn_coord_of_holderSeminormBoundOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (hUtop : MeasureTheory.volume U ≠ ⊤) {K r : ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {x : HCPolySupport.Vec d} (hx : x ∈ U) (hK : 0 ≤ K) (hG : Support.HolderSeminormBoundOn U (1 / 2) K G) (hdiam : ∀ p ∈ U, ‖p - x‖ ≤ r) (i : Fin d) : MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => G p i) U MeasureTheory.volume

A Hölder field is integrable on a bounded window, coordinatewise. This is the integrability slot of AffineSplitLift.abs_sub_affineLift_volumeAverage_le and it is derived, not assumed.

2. The residual bound

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.datumResidualBound (d : ℕ) (n : ℤ) (Kh : ℝ) : ℝ

The L^∞ size of the datum's deviation from its affine lift on U₂. 2 d [∇h]_{C^{0,1/2}(U₂)} (3^{n-2}/2)^{3/2}.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.datumResidualBound d n Kh = 2 * ↑d * Kh * (3 ^ (n - 2) / 2) ^ (3 / 2)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.datumResidualBound_nonneg (d : ℕ) (n : ℤ) {Kh : ℝ} (hKh : 0 ≤ Kh) : 0 ≤ datumResidualBound d n Kh

3. The corrector carrying the datum's deviation

4. Where the [∇h] leg proves

theorem Algsuperdiff.Section4.Provider.ExcessDecay.datumResidualBound_zpow_mul (d : ℕ) (n : ℤ) (Kh : ℝ) : 3 ^ (-n) * datumResidualBound d n Kh = 2 * ↑d * Kh * (3 ^ (-3) * 2 ^ (-(3 / 2))) * (3 ^ n) ^ (1 / 2)

The measured scale shape of the datum leg. The corrector enters the one-step chain through the L² comparison slot, i.e. against the normalizer 3^{-n}; the product is the manuscript's own (3^n)^{1/2} [∇h].