WaveTranslation

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

The uniform large-cube supremum gauge at an arbitrary triadic cube

Provider/Stream/IncrementTranslation.lean moved the cube-averaged L^p chain of ABK26's Step 2 from the centered cube cu_l to an arbitrary triadic cube Q. The L^infty chain did not move with it, and this is what blocked the wave terms of Step 2: largeCubeSupBound l n m is not a cube average but a uniform supremum gauge, represented by a maximum of small-cube gauges over an explicit covering grid inside cu_l (Provider/Stream/LargeCubeLinfty.lean). Transporting it to Q therefore requires re-indexing the covering grid, which no proved statement did: TranslatedLargeCubeW1Inf.lean and TranslatedTransport.lean carry the one-shell half of that machinery only (a single translated base point z, and the covering maximum only for the own-scale derivative gauge of a single shell).

This module supplies the missing deterministic half and its immediate probabilistic consequence.

The grid re-indexing

The covering family of the origin cube cu_l at scale n is indexed by the finite set subcubeShifts d n l of lattice points of 3^{n-1} Z^d, the grid point of index p sitting at subcubeCenter n p. The covering family of Q is the SAME index set at l = Q.scale, with every grid point pushed forward by the base point z_Q = triadicCubeShift Q of Q:

  cubeSubcubeCenter Q n p  =  subcubeCenter n p + z_Q .

exists_cubeSubcubeCenter_mem is the resulting covering property at Q (every point of the open cube Q lies in one of the translated open small cubes), obtained from CoarseGraining's openCubeSet_eq_translateSet_originCube_of_triadicCube and the proved origin covering property exists_subcubeShift_mem.

The generator

cubeSupBound_eq_largeCubeSupBound_translate:

  cubeSupBound Q n m omega  =  largeCubeSupBound Q.scale n m (tau_{z_Q} omega) ,

with tau_z = ShellField.translateSequence z the joint translation action on the whole shell sequence. This is an equality of functions of the sample, not an equality in law: the per-cube gauge is the origin-cube gauge read at the translated sample. Its one-cube step is translatedIncrementSupBound_cubeSubcubeCenter, which is exactly the re-indexing: the small-cube gauge at the pushed-forward grid point of the original sample is the small-cube gauge at the original grid point of the translated sample.

Everything else here is a corollary of the generator together with the proved abstract transport isBigOWith_comp_translateSequence / isBigOWith_comp_translateCutoffSample. In particular every transported amplitude is the O amplitude read at l = Q.scale, V: translation is an exact isometry of the law, so there is no union bound, no covering penalty beyond the one the origin display already pays, and no new dimension-only constant anywhere in this module.

Main definitions

• Algsuperdiff.Section3.Provider.Stream.cubeSubcubeCenter
• Algsuperdiff.Section3.Provider.Stream.cubeSupBound

Main results

• Algsuperdiff.Section3.Provider.Stream.exists_cubeSubcubeCenter_mem
• Algsuperdiff.Section3.Provider.Stream.cubeSupBound_eq_largeCubeSupBound_translate
• Algsuperdiff.Section3.Provider.Stream.matrixOperatorNorm_finiteShellIncrement_le_cubeSupBound
• Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_cubeSupBound
• Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_cubeSupBound_cutoffLaw

References

• ABK26, e.km.kn.Linfty, proof (the origin display whose covering grid is re-indexed here).
• ABK26, e.kmn.bounds, ("by the assumption of R^d-stationarity"), and l.bad.event.lemma, in particular the reduction "by stationarity, it suffices to prove the case z = 0" with z in R^d.
• Provider/Stream/LargeCubeLinfty.lean (the origin covering grid), Provider/Stream/IncrementTranslation.lean (the abstract transport), Homogenization/Geometry/TriadicCubeTranslation.lean (the cube geometry).

The covering grid of an arbitrary triadic cube

noncomputable def Algsuperdiff.Section3.Provider.Stream.cubeSubcubeCenter {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n : ℤ) (p : Fin d → ℤ) : HCPolySupport.Vec d

The base point of the scale-n covering cube of index p inside the triadic cube Q: the origin grid point subcubeCenter n p pushed forward by the base point triadicCubeShift Q of Q.

This is the re-indexing of the covering family under the translation: the index set is unchanged, only the grid points move.

Equations

• Algsuperdiff.Section3.Provider.Stream.cubeSubcubeCenter Q n p = Algsuperdiff.Section3.Provider.Stream.subcubeCenter n p + HCPolySupport.triadicCubeShift Q

theorem Algsuperdiff.Section3.Provider.Stream.exists_cubeSubcubeCenter_mem {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n : ℤ) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet Q) : ∃ p ∈ subcubeShifts d n Q.scale, x ∈ HCPolySupport.translateSet (cubeSubcubeCenter Q n p) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))

The covering property at an arbitrary cube. Every point of the open cube Q lies in one of the translated open small cubes of the re-indexed family, whose index set is the origin index set at the scale of Q.

The per-cube uniform supremum gauge

noncomputable def Algsuperdiff.Section3.Provider.Stream.cubeSupBound {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : ℝ

The single random variable dominating ‖k_m - k_n‖_{L∞(Q)} at an A triadic cube Q: the maximum of the small-cube gauges over the re-indexed covering family of Q.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Stream.translatedIncrementSupBound_cubeSubcubeCenter {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n m : ℤ) (p : Fin d → ℤ) (omega : Cutoff.ShellSeq d) : translatedIncrementSupBound (cubeSubcubeCenter Q n p) n m omega = translatedIncrementSupBound (subcubeCenter n p) n m (Frozen.Assumptions.ShellField.translateSequence (HCPolySupport.triadicCubeShift Q) omega)

The one-cube re-indexing step. The small-cube gauge at the pushed-forward grid point, read at the original sample, is the small-cube gauge at the original grid point, read at the T sample.

theorem Algsuperdiff.Section3.Provider.Stream.cubeSupBound_eq_largeCubeSupBound_translate {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : cubeSupBound Q n m omega = largeCubeSupBound Q.scale n m (Frozen.Assumptions.ShellField.translateSequence (HCPolySupport.triadicCubeShift Q) omega)

The grid re-indexing identity. The uniform supremum gauge of the finite stream increment on an arbitrary triadic cube Q is the origin-cube gauge at the scale of Q, read at the sample translated by the base point of Q.

This is an exact identity of functions of the sample — not an identity in law — and it is the deterministic half of the transport of the Step-2 wave terms.

theorem Algsuperdiff.Section3.Provider.Stream.cubeSupBound_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : 0 ≤ cubeSupBound Q n m omega

theorem Algsuperdiff.Section3.Provider.Stream.matrixOperatorNorm_finiteShellIncrement_le_cubeSupBound {d : ℕ} (omega : Cutoff.ShellSeq d) (Q : HCPolySupport.TriadicCube d) (n m : ℤ) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet Q) : HCPolySupport.Book.Ch02.matrixOperatorNorm ((Cutoff.finiteShellIncrement omega n m).toFun x) ≤ cubeSupBound Q n m omega

The deterministic half of e.km.kn.Linfty at an arbitrary cube: at every point of the open cube Q the finite stream increment is dominated by the single random variable cubeSupBound Q n m.

Measurability

theorem Algsuperdiff.Section3.Provider.Stream.measurable_translatedIncrementSupBound {d : ℕ} (z : HCPolySupport.Vec d) (n m : ℤ) : Measurable (translatedIncrementSupBound z n m)

The translated small-cube gauge is a random variable.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_largeCubeSupBound {d : ℕ} (l n m : ℤ) : Measurable (largeCubeSupBound l n m)

The origin-cube uniform gauge is a random variable.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_cubeSupBound {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n m : ℤ) : Measurable (cubeSupBound Q n m)

The per-cube uniform gauge is a random variable.

e.km.kn.Linfty at an arbitrary triadic cube

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_cubeSupBound {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (cubeSupBound Q n m) ((3 * max 1 (Real.log ↑(subcubeShifts d n Q.scale).card)) ^ 2⁻¹ * (streamLinftyConst d * min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m)))

The estimates on the lower-tail cutoff carrier

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_cubeSupBound_cutoffLaw {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.CutoffSample d) => cubeSupBound Q n m ↑omega) ((3 * max 1 (Real.log ↑(subcubeShifts d n Q.scale).card)) ^ 2⁻¹ * (streamLinftyConst d * min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m)))

The per-cube covering maximum, read on the lower-tail cutoff carrier.