OscillationGrid

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

The truncated-window oscillation family at a scale-indexed grid of centres

The oscillation family of OscillationFamily.lean is stated at a centre of the triadic lattice of the bottom scale. A Campanato characterisation of Hölder spaces instead reads a scale-indexed family of centres: at window scale j the admissible centres are the points of the lattice of spacing 3 ^ (j-1), one triadic scale finer than the window, which is what makes the family fine enough to reach every point of the cube.

This module supplies the two dictionaries that connect the two readings and then restates the family in the grid form.

• the truncated window (z + □_j) ∩ □_m is the intersection of the sup-ball of radius 3 ^ j / 2 about z with the sup-ball of radius 3 ^ m / 2 about the origin — the shape a Campanato telescope on a cube consumes;
• a point of the lattice of spacing 3 ^ (j-1) lies on the lattice of spacing 3 ^ n for every n ≤ j - 1, so a single grid centre serves every admissible bottom scale at or below its own.

Main definitions

• latticeDescent — the index of a lattice point read at a coarser scale.

Main results

• truncatedWindow_eq_ball_inter_ball — the window dictionary.
• triadicLatticePoint_latticeDescent — the lattice dictionary.
• oscillationHolderBound_zeroDatum_grid — the family at a grid centre, with the bottom scale free below the centre's own lattice scale.

References

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

1. The window dictionary

theorem Algsuperdiff.Section4.Provider.Holder.openCubeAtScale_eq_ball {d : ℕ} (x : HCPolySupport.Vec d) (k : ℤ) : HCPolySupport.Book.Ch03.openCubeAtScale x k = Metric.ball x (3 ^ k / 2)

The open cube of scale k about x is the sup-ball of radius 3 ^ k / 2.

theorem Algsuperdiff.Section4.Provider.Holder.openCubeSet_originCube_eq_ball_zero {d : ℕ} (m : ℤ) : HCPolySupport.openCubeSet (HCPolySupport.originCube d m) = Metric.ball 0 (3 ^ m / 2)

The cube □_m is the sup-ball of radius 3 ^ m / 2 about the origin.

theorem Algsuperdiff.Section4.Provider.Holder.truncatedWindow_eq_ball_inter_ball {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : ExcessDecay.truncatedWindow x m k = Metric.ball x (3 ^ k / 2) ∩ Metric.ball 0 (3 ^ m / 2)

The window dictionary. The truncated window (z + □_k) ∩ □_m is the intersection of the sup-ball of radius 3 ^ k / 2 about z with the sup-ball of radius 3 ^ m / 2 about the origin.

2. The lattice dictionary

def Algsuperdiff.Section4.Provider.Holder.latticeDescent {d : ℕ} (n n₀ : ℤ) (v : Fin d → ℤ) : Fin d → ℤ

The index of a lattice point read at a coarser scale. A point of 3 ^ n₀ ℤ^d is a point of 3 ^ n ℤ^d for every n ≤ n₀, with index scaled by 3 ^ (n₀ - n).

Equations

• Algsuperdiff.Section4.Provider.Holder.latticeDescent n n₀ v i = 3 ^ (n₀ - n).toNat * v i

theorem Algsuperdiff.Section4.Provider.Holder.triadicLatticePoint_latticeDescent {d : ℕ} {n n₀ : ℤ} (hn : n ≤ n₀) (v : Fin d → ℤ) : Support.triadicLatticePoint n (latticeDescent n n₀ v) = Support.triadicLatticePoint n₀ v

The descended index names the same point.

theorem Algsuperdiff.Section4.Provider.Holder.latticeDescent_mem_latticeCubeSet {d : ℕ} {n n₀ m : ℤ} (hn : n ≤ n₀) {v : Fin d → ℤ} (hv : Support.triadicLatticePoint n₀ v ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : latticeDescent n n₀ v ∈ Support.latticeCubeSet d n m

The descended index is admissible for the ambient cube.

3. The family at a grid centre

theorem Algsuperdiff.Section4.Provider.Holder.oscillationHolderBound_zeroDatum_grid (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 : ℤ), 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 → ∀ (n j m' : ℤ), n ≤ j - 1 → j ≤ m' → m' ≤ m → X omega ≤ ↑(m - n).toNat → ∀ z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), (∃ (v : Fin d → ℤ), z = Support.triadicLatticePoint (j - 1) v) → (3 ^ (-j) * Support.normalizedL2On (ExcessDecay.truncatedWindow z m j) fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m j) u.toFun) ≤ Cosc * Real.rpow 3 (1 / 2 * ((1 - alpha) * (↑m - ↑n))) * ((3 ^ (-m') * Support.normalizedL2On (ExcessDecay.truncatedWindow z m m') fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m m') u.toFun) + Cdata * ((↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Kg))

[ABK] e.oscillation.Holder.bound at a scale-indexed grid centre.

The oscillation family of oscillationHolderBound_zeroDatum, read at a centre z of the triadic lattice of spacing 3 ^ (j-1) -- one scale finer than the window of scale j it carries -- with the bottom scale n left free below that lattice scale. This is the reading a Campanato characterisation on the cube consumes: the centres available at window scale j form a lattice fine enough to approximate every point of the cube, and one and the same centre serves every admissible bottom scale at or below j - 1.

The seed is the oscillation on the truncated window (z + □_{m'}) ∩ □_m at the caller's own upper scale m'.