Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Holder.OscillationFamily

OscillationFamily #

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

The truncated-window oscillation family at triadic lattice centres #

This module assembles, below the frozen surface, the two-parameter oscillation estimate of [ABK] e.oscillation.Holder.bound for the zero-boundary-datum Dirichlet problem of the cutoff field on the cube □_m.

For a scale m, a truncation index L ≥ m, a bottom scale n admissible for the minimal scale X and a lattice centre z = 3 ^ n v ∈ 3 ^ n ℤ^d ∩ □_m, the family is stated on the truncated windows U_j = (z + □_j) ∩ □_m and reads, for every n ≤ n' ≤ m' ≤ m,

   3 ^ (-n') ‖u - (u)_{U_{n'}}‖_{L²(U_{n'})}
     ≤ Cosc · 3 ^ ((1/2)(1-α)(m-n))
         ( 3 ^ (-m') ‖u - (u)_{U_{m'}}‖_{L²(U_{m'})}
           + Cdata · σ_m⁻¹ 3 ^ (m/2) K_g ) ,

with K_g a C^{0,1/2} seminorm bound for the force on □_m. The exponent 1/2 is the source's β. There is no boundary-datum leg: at zero datum the ∇h term of the source's δ_j budget vanishes identically.

The minimal scale is the one the excess-decay chain builds, X = Z + k + 3 at the Step-1 parameters, and it is returned with the same measurability and the same exponential tail that the regularity theorem of Section 4 carries, so a consumer may read the tail from either.

Main definitions #

Main results #

References #

1. The zero boundary datum #

The zero element of H¹ has the zero value field.

At the zero datum every Hölder seminorm bound holds with constant 0.

At the zero datum the pointwise gradient cap holds with constant 0.

The zero datum is classically differentiable with the zero gradient field.

The printed boundary ∇h datum leg vanishes at the zero datum: both of its summands carry the factor K_h.

2. The amplitude of the force leg #

The model-free amplitude of the force leg. The Step-5 budget's weight 4 C_δ / (1 - 3 ^ (-(1/2 - γ))) is enlarged to the γ-free 4 C_δ / (1 - 3 ^ (-1/4)) and multiplied by the Step-4 Gagliardo constant that converts the printed C^{0,1/2} seminorm of the force into the fractional seminorm the excess-decay lane reads.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Algsuperdiff.Section4.Provider.Holder.edFinalDataG_le_oscillationDataConst (d : ℕ) [NeZero d] {M : Section3.ABKModel d} (hgamma : M.gamma < 1 / 2) (hquarter : M.gamma ≤ 1 / 4) (Cb : ℝ) {C Kg : ℝ} (hC : 0 ≤ C) (hKg : 0 ≤ Kg) (k : ℕ) (m : ℤ) :

    The force leg, in the gauge the source prints. The excess-decay lane's own data leg is at most the amplitude times σ_m⁻¹ 3 ^ (m/2) K_g.

    3. The oscillation family #

    theorem Algsuperdiff.Section4.Provider.Holder.oscillationHolderBound_zeroDatum (d : ℕ) [NeZero d] (hd : d ≠ 0) (cstar : ℝ) (hcstar : 0 < cstar) :
    ∃ (gamma0 : ℝ) (C : ℝ) (Cosc : ℝ) (Cdata : ℝ), 0 < gamma0 ∧ 0 < C ∧ 0 ≤ Cosc ∧ 0 ≤ Cdata ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (alpha : ℝ), 0 < alpha → alpha ≤ 1 - C * √M.gamma → ∀ (m : ℤ), ∃ (X : Section3.Cutoff.CutoffSample d → ℕ∞), Measurable X ∧ (∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ X omega} ≤ ENNReal.ofReal (C * Real.exp (-((1 - alpha) ^ 2 * (↑N - C)) / (C * M.gamma)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (L n : ℤ), m ≤ L → n ≤ m → X omega ≤ ↑(m - n).toNat → ∀ v ∈ Support.latticeCubeSet d n m, ∀ (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg : ℝ), 0 ≤ Kg → Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u 0 g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → ∀ (n' m' : ℤ), n ≤ n' → n' ≤ m' → m' ≤ m → (3 ^ (-n') * Support.normalizedL2On (ExcessDecay.truncatedWindow (Support.triadicLatticePoint n v) m n') fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow (Support.triadicLatticePoint n v) m n') u.toFun) ≤ Cosc * Real.rpow 3 (1 / 2 * ((1 - alpha) * (↑m - ↑n))) * ((3 ^ (-m') * Support.normalizedL2On (ExcessDecay.truncatedWindow (Support.triadicLatticePoint n v) m m') fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow (Support.triadicLatticePoint n v) m m') u.toFun) + Cdata * ((↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Kg))

    [ABK] e.oscillation.Holder.bound at zero boundary datum.

    For a disorder model of strength gamma small enough and every Hölder exponent alpha below 1 - C sqrt gamma, and for every scale m, there is a minimal scale X -- measurable, with the exponential tail of the regularity theorem -- such that, almost surely, for every truncation index L ≥ m, every bottom scale n ≤ m admissible for X, every lattice centre z = 3 ^ n v of the cube, every zero-datum Dirichlet solution u on □_m with force g of C^{0,1/2} seminorm at most K_g, and every pair of scales n ≤ n' ≤ m' ≤ m, the normalized oscillation on the truncated window U_{n'} = (z + □_{n'}) ∩ □_m is bounded by 3 ^ ((1/2)(1-alpha)(m-n)) times the oscillation on U_{m'} plus the force leg σ_m⁻¹ 3 ^ (m/2) K_g.

    The exponent 1/2 is the source's β; the boundary-datum leg of the source's display vanishes at zero datum.