ComparatorUniformBound

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

The comparator is uniformly bounded over the normalized forcing class

On the normalized class the interior Schauder estimate for the comparator reads, at Kg = 3^{-n/2},

  3^{-n/2} Ksup + KHol ≤ C 3^{-n/2} σ_n⁻¹ ,

so Ksup ≤ C σ_n⁻¹ uniformly in the forcing field, and the supremum bound of the comparator's Lipschitz representative becomes

  σ_n 3^{-n} ‖v‖_{L^∞(y+□_n)} ≤ σ_n 3^{-n} · d · C σ_n⁻¹ · 3^n / 2 = d C / 2 ,

a bound with no dependence on the scale, the centre, the model or the datum. This discharges the comparator hypothesis of the localized finiteness statements; the rough-field hypothesis is left explicit, to be discharged by the boundary Schauder estimate.

Main results

• ksup_le_of_normalized_estimate — the scalar step Ksup ≤ C σ_n⁻¹.
• exists_hasUniformComparatorSupBound — the comparator hypothesis of the localized finiteness statements holds, with an explicit constant.
• localizedError_comparator_term_le — the normalized form d C / 2.

References

• ABK26, the comparator of Section 5.1.

1. Congruence of the two gauges under a pointwise identity

theorem Algsuperdiff.Section5.Support.supNormOn_congr {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {f h : HCPolySupport.Vec d → E} (hfh : Set.EqOn f h U) : supNormOn U f = supNormOn U h

2. The scalar step

theorem Algsuperdiff.Section5.Support.ksup_le_of_normalized_estimate {C Ksup KHol sigma : ℝ} (n : ℤ) (hKHol : 0 ≤ KHol) (hest : Real.rpow 3 (-(1 / 2 * ↑n)) * Ksup + KHol ≤ C * (Real.rpow 3 (1 / 2 * ↑n))⁻¹ * (sigma⁻¹ * Real.rpow 3 (↑n / 2) * Real.rpow 3 (-↑n / 2))) : Ksup ≤ C * sigma⁻¹

Ksup ≤ C σ_n⁻¹ on the normalized class. The two powers of three on the right cancel at Kg = 3^{-n/2}, and the nonnegative Hölder constant is dropped from the left.

3. The comparator hypothesis of the localized finiteness statements

theorem Algsuperdiff.Section5.Support.exists_hasUniformComparatorSupBound (d : ℕ) (hdim : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d), HasUniformComparatorSupBound M n y (↑d * (C * (↑(Section3.Annealed.sigmaBar M n))⁻¹) * 3 ^ n / 2)

The comparator representatives are uniformly bounded on the normalized class. The constant is explicit and depends only on d, the universal Schauder constant, the diffusivity σ_n and the scale.

4. The normalized form

theorem Algsuperdiff.Section5.Support.localizedError_comparator_term_le (d : ℕ) (hdim : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) (g : HCPolySupport.Vec d → HCPolySupport.Vec d), NormalizedForceAt y n g → ∀ (v : HCPolySupport.H1Function (cubeSetAt y n)), IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => ↑(Section3.Annealed.sigmaBar M n) • 1) y n v g → ∀ (vRep : HCPolySupport.Vec d → ℝ), IsCubeRepresentative y n v vRep → ENNReal.ofReal (↑(Section3.Annealed.sigmaBar M n) * Real.rpow 3 (-↑n)) * supNormOn (cubeSetAt y n) vRep ≤ ENNReal.ofReal (↑d * C / 2)

The comparator contributes at most d C / 2 to the localized error.