CampanatoFeed

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

The oscillation family in the shape a Campanato characterisation consumes

The Campanato characterisation of Hölder spaces on a cube reads a scale-indexed family of clipped windows: at window index j the admissible centres are the points of the lattice of spacing 3 ^ (m-j-1) inside the cube, and the estimate required is

‖u - (u)_W‖_{L²(W)} ≤ K (3 ^ (m-j) / 2) ^ alpha, W = (z + □_{m-j}) ∩ □_m,

with one constant K serving every index and every centre. This module turns the two-parameter family of OscillationGrid.lean into exactly that predicate.

Two things happen here. The bottom scale is chosen: n = m-j-1 while that is admissible, and n = m - X for the top X window indices, which is what creates the factor 3 ^ ((1-alpha) X / 2) in K. And the seed is made independent of the centre: the window (z + □_m) ∩ □_m is compared with the cube itself at the volume price 2 ^ (d/2).

Main definitions

• campanatoGridConstant — the constant K produced, written out.

Main results

• hasClipGridOscillationDecay_zeroDatum — the family in the consumed shape.

References

• [ABK], ss.proof.regularity Step 3 and display e.oscillation.Holder.bound.

1. The window and grid dictionaries

theorem Algsuperdiff.Section4.Provider.Holder.clipBall_zero_eq_truncatedWindow {d : ℕ} (m : ℤ) (z : HCPolySupport.Vec d) (j : ℕ) : StochasticProcess.Common.Regularity.Campanato.clipBall 0 (3 ^ m / 2) z (StochasticProcess.Common.Regularity.Campanato.triadicRadius (3 ^ m / 2) j) = ExcessDecay.truncatedWindow z m (m - ↑j)

The clipped window of index j about z in the cube □_m is the truncated window of scale m - j about z.

theorem Algsuperdiff.Section4.Provider.Holder.truncatedWindow_top_eq_clipBall {d : ℕ} (m : ℤ) (z : HCPolySupport.Vec d) : ExcessDecay.truncatedWindow z m m = StochasticProcess.Common.Regularity.Campanato.clipBall 0 (3 ^ m / 2) z (3 ^ m / 2)

The top truncated window is the clipped window of index 0.

theorem Algsuperdiff.Section4.Provider.Holder.clipBall_centre_eq_openCubeSet {d : ℕ} (m : ℤ) : StochasticProcess.Common.Regularity.Campanato.clipBall 0 (3 ^ m / 2) 0 (3 ^ m / 2) = HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The clipped window at the centre of the cube is the cube.

theorem Algsuperdiff.Section4.Provider.Holder.two_mul_triadicRadius_succ (m : ℤ) (j : ℕ) : 2 * StochasticProcess.Common.Regularity.Campanato.triadicRadius (3 ^ m / 2) (j + 1) = 3 ^ (m - ↑j - 1)

The spacing of the admissible centres at window index j is 3 ^ (m-j-1).

theorem Algsuperdiff.Section4.Provider.Holder.exists_index_of_mem_centredTriadicGrid {d : ℕ} (m : ℤ) (j : ℕ) {z : HCPolySupport.Vec d} (hz : z ∈ StochasticProcess.Common.Regularity.Campanato.centredTriadicGrid 0 (3 ^ m / 2) (3 ^ m / 2) j) : ∃ (v : Fin d → ℤ), z = Support.triadicLatticePoint (m - ↑j - 1) v

An admissible centre at window index j is a point of the triadic lattice of scale m - j - 1.

theorem Algsuperdiff.Section4.Provider.Holder.mem_openCubeSet_of_mem_centredTriadicGrid {d : ℕ} (m : ℤ) (j : ℕ) {z : HCPolySupport.Vec d} (hz : z ∈ StochasticProcess.Common.Regularity.Campanato.centredTriadicGrid 0 (3 ^ m / 2) (3 ^ m / 2) j) : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

An admissible centre lies in the cube.

2. The centre-free seed

theorem Algsuperdiff.Section4.Provider.Holder.normalizedL2On_truncatedWindow_top_le {d : ℕ} {m : ℤ} {z : HCPolySupport.Vec d} {f : HCPolySupport.Vec d → ℝ} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : (Support.normalizedL2On (ExcessDecay.truncatedWindow z m m) fun (y : HCPolySupport.Vec d) => f y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m m) f) ≤ StochasticProcess.Common.Regularity.Ported.ballVolumePrice 2 d * Support.normalizedL2On (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (y : HCPolySupport.Vec d) => f y - HCPolySupport.volumeAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) f

The seed comparison. The oscillation on the top truncated window about a centre of the cube is at most 2 ^ (d/2) times the oscillation on the cube.

3. The constant

noncomputable def Algsuperdiff.Section4.Provider.Holder.campanatoGridConstant (alpha : ℝ) (m : ℤ) (Xn : ℕ) (Cosc D : ℝ) : ℝ

The Campanato constant produced by the choice of bottom scale. The factor 3 ^ ((1-alpha)(X+1)/2) is the price of the top X window indices, at which the bottom scale is frozen at m - X, together with the one triadic scale between a centre's own lattice and its window; the factor 3 ^ ((1-alpha) m) is the normalization of the seed, and 2 ^ alpha the half-side dictionary.

Equations

• Algsuperdiff.Section4.Provider.Holder.campanatoGridConstant alpha m Xn Cosc D = Real.rpow 2 alpha * Cosc * Real.rpow 3 ((1 - alpha) * (↑m + (↑Xn + 1) / 2)) * D

theorem Algsuperdiff.Section4.Provider.Holder.campanatoGridConstant_nonneg {alpha : ℝ} (m : ℤ) (Xn : ℕ) {Cosc D : ℝ} (hCosc : 0 ≤ Cosc) (hD : 0 ≤ D) : 0 ≤ campanatoGridConstant alpha m Xn Cosc D

4. The feed

theorem Algsuperdiff.Section4.Provider.Holder.hasClipGridOscillationDecay_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), ∀ (Xn : ℕ), X omega ≤ ↑Xn → ∀ (L : ℤ), m ≤ L → ∀ (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 → StochasticProcess.Common.Regularity.Campanato.HasClipGridOscillationDecay 0 (3 ^ m / 2) (StochasticProcess.Common.Regularity.Campanato.centredTriadicGrid 0 (3 ^ m / 2) (3 ^ m / 2)) (3 ^ m / 2) alpha (campanatoGridConstant alpha m Xn Cosc (3 ^ (-m) * (StochasticProcess.Common.Regularity.Ported.ballVolumePrice 2 d * Support.normalizedL2On (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) + Cdata * ((↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Kg))) 0 u.toFun

[ABK] e.oscillation.Holder.bound, in the shape a Campanato characterisation of Hölder spaces on the cube consumes.

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 natural bound Xn on X, every truncation index L ≥ m, and every zero-datum Dirichlet solution u on □_m with force g of C^{0,1/2} seminorm at most K_g, the clipped-window oscillation decay of exponent alpha holds at every index of the triadic family of centres inside □_m, with the single constant campanatoGridConstant and the seed read on the cube itself.

The bottom scale is chosen by the two-case rule of the source's scale range: n = m-j-1 while that is admissible, n = m - X above it.