PointwiseBound

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

The localized regularity at the Hölder exponent one half

The local Hölder estimate is read at the exponent alpha = 1/2, on the cube it is stated on, at the truncation scale equal to the scale of the cube. Three normalizations then meet:

• the localized regularity measures the 1/2-Hölder seminorm of the continuous representative in the gauge σ_n 3^{-n/2}, while the local estimate measures it in the gauge 3^{n/2}; the two differ by the factor σ_n 3^{-n}, which is exactly the gauge of the localized error;
• on the normalized forcing class the datum leg of the local estimate, carrying σ_n⁻¹ 3^{3n/2} and the seminorm [g]_{C^{0,1/2}} ≤ 3^{-n/2}, contributes at most one after that rescaling;
• the mean-oscillation seed of the local estimate, in the same gauge, is at most C (1 + E) with E the localized error.

The result is the almost sure pointwise bound

localizedRegularity ≤ C 3^{X/2} (1 + localizedError),

uniform over the forcing class and over the solutions, with X the minimal scale of the local Hölder estimate at alpha = 1/2 and its exponential tail.

Main results

• exists_localizedRegularity_pointwise_bound — the bound above, together with the measurability and the tail of the scale X.

theorem Algsuperdiff.Section4.Provider.RegularityMoment.exists_localizedRegularity_pointwise_bound (d : ℕ) (cstar : ℝ) (hdim : 2 ≤ d) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (Ctail : ℝ) (Camp : ℝ), 0 < gamma0 ∧ 0 < Ctail ∧ 0 < Camp ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (n : ℤ) (y : HCPolySupport.Vec d), ∃ (X : Section3.Cutoff.CutoffSample d → ℕ), Measurable X ∧ (∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | N ≤ X omega} ≤ ENNReal.ofReal (Ctail * Real.exp (-((1 - 1 / 2) ^ 2 * (↑N - Ctail)) / (Ctail * M.gamma)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), Section5.Support.localizedRegularity M n y omega ≤ ENNReal.ofReal (Camp * Real.rpow 3 (1 / 2 * ↑(X omega))) * (1 + Section5.Support.localizedError M n y omega)

The localized regularity is bounded by the minimal-scale factor and the localized error. At the Hölder exponent 1/2 the local Hölder estimate, the normalization of the forcing class and the mean-oscillation seed give, almost surely and simultaneously for every datum of the normalized class and every solution of the rough-field Dirichlet problem on the cube,

localizedRegularity M n y ω ≤ C 3^{X ω / 2} (1 + localizedError M n y ω),

where X is the minimal scale of the local Hölder estimate at alpha = 1/2, with its measurability and its exponential tail. The centre y is arbitrary, as it is in both inputs.