LocalHolderEstimateProvider

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

The local Hölder estimate on a translated cube

This module assembles the local C^{0,alpha} estimate for the zero-datum Dirichlet problem on the cube y + □_m, at every exponent alpha ∈ (0, 1 - C sqrt gamma], from the clipped-window oscillation family of the regularity theorem and the Campanato characterisation of Hölder spaces on a cube.

Three things are supplied here.

• The centre. The oscillation family lives on the origin cube; the Dirichlet problem on y + □_m at the sample omega is the Dirichlet problem on □_m at the translated sample, and the cutoff-sample law is translation invariant, so the minimal scale of the centre y is the origin's minimal scale read at the translated sample.
• The exponent range. The chaining constant of the Campanato characterisation grows without bound as the exponent tends to 0, while the normalized seminorm 3 ^ (alpha m) [·]_{C^{0,alpha}(y + □_m)} increases with the exponent, because the cube has diameter 3 ^ m. The estimate at a small exponent is therefore deduced from the estimate at the exponent max alpha (1/2), whose chaining constant is uniform; the minimal scale is doubled so that the prefactor 3 ^ ((1 - alpha) X) still dominates, and the tail of the doubled scale is the tail of the original at half the index, which the sixteen-fold enlargement of the constant absorbs.
• The ℕ-valued scale. The oscillation family carries an ℕ∞-valued minimal scale; the exponential tail makes it finite almost surely, and the estimate is asserted almost surely, so the ℕ-valued recast costs nothing.

The small-disorder threshold is chosen so that 1/2 itself lies in the admissible exponent range, which is what makes the second item available.

Main results

• ae_ne_top_of_tail — an exponential tail forces almost-sure finiteness.
• tail_exponent_le — the tail arithmetic of the doubled scale.
• local_holder_estimate_provider — the estimate.

Tail bookkeeping

theorem Algsuperdiff.Section4.Provider.ae_ne_top_of_tail {d : ℕ} {M : Section3.ABKModel d} {Cst a : ℝ} (hCst : 0 < Cst) (ha : 0 < a) {X : Section3.Cutoff.CutoffSample d → ℕ∞} (htail : ∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ X omega} ≤ ENNReal.ofReal (Cst * Real.exp (-(a * (↑N - Cst)) / (Cst * M.gamma)))) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), X omega ≠ ⊤

The exponential tail forces almost-sure finiteness.

theorem Algsuperdiff.Section4.Provider.tail_exponent_le {A B C0 C N : ℝ} (hC0 : 0 < C0) (hC : 16 * C0 ≤ C) (hB : 0 ≤ B) (hBA : B ≤ A) (hA4B : A ≤ 4 * B) (hN : 0 ≤ N) : A * (N - C) / C ≤ B * (N / 2 - C0) / C0

The doubled minimal scale keeps an admissible tail.

The provider

theorem Algsuperdiff.Section4.Provider.local_holder_estimate_provider (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (alpha : ℝ), 0 < alpha → alpha ≤ 1 - C * √M.gamma → ∀ (m : ℤ) (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 (C * Real.exp (-((1 - alpha) ^ 2 * (↑N - C)) / (C * M.gamma)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (L : ℤ), m ≤ L → ∀ (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (u : HCPolySupport.H1Function (Section5.Support.cubeSetAt y m)), Section5.Support.IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField y m u g → ⨅ (uRep : HCPolySupport.Vec d → ℝ), ⨅ (_ : Section5.Support.IsCubeRepresentative y m u uRep), ENNReal.ofReal (Real.rpow 3 (alpha * ↑m)) * Section5.Support.holderSeminormOn (Section5.Support.cubeSetAt y m) alpha uRep ≤ ENNReal.ofReal (C * Real.rpow 3 ((1 - alpha) * ↑(X omega))) * (MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => u.toFun x - HCPolySupport.volumeAverage (Section5.Support.cubeSetAt y m) u.toFun) 2 (Support.normalizedVolumeMeasureOn (Section5.Support.cubeSetAt y m)) + ENNReal.ofReal ((↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (3 * ↑m / 2)) * Section5.Support.holderSeminormOn (Section5.Support.cubeSetAt y m) (1 / 2) g)