IncrementTranslation

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

The stream-increment L^p chain at an arbitrary triadic cube

ABK26 states every stream-increment estimate at the centered cube cu_l and then moves it to an off-centre cube by the single phrase "by R^d-stationarity" (for e.kmn.bounds;, for the bad-event lemma). The whole proved Step-2 chain of this repository — streamIncrementLpMass, streamIncrementLpNorm, streamIncrementLpTail and the Gamma estimates built on them — is likewise defined on the origin cubes only. This module supplies the passage, at the level of the observable, from the origin cube to every triadic cube Q.

The two halves, and what was already available

The manuscript's step has a deterministic half and a probabilistic half, and BOTH halves were already proved in this repository before this module:

• the joint multi-shell covariance of the increment, Stream.translateReg_finiteShellIncrement (IncrementLaw.lean): translateReg z (k_m - k_n)(omega) = (k_m - k_n)(tau_z omega) with tau_z = ShellField.translateSequence z acting on every shell at once; and
• the joint law invariance Cutoff.sequenceLaw_stationary (Cutoff/Symmetry.lean): (tau_z)_* P = P for every z : Vec d, derived from the frozen shell independence, the frozen marginal scaling law and (J1) through Measure.infinitePi.

What was missing is the composite: no statement anywhere carried a stream-increment L^p quantity at a cube other than cu_l.

The generator

cubeAverage_streamIncrementLpDensity_eq_streamIncrementLpMass_translate:

  ⨍_{Q} |(k_m - k_n)(x)|^p dx  =  ⨍_{cu_{Q.scale}} |(k_m - k_n)(tau_{z_Q} omega)(x)|^p dx ,

z_Q = triadicCubeShift Q the base point of Q. This is an equality of functions of the sample, not an equality in law: the per-cube mass is the origin-cube mass read at the translated sample. It is assembled from CoarseGraining's cubeSet_eq_translateSet_originCube_of_triadicCube, the proved regFieldLpMass_translateSet and translateReg_finiteShellIncrement.

Everything else in the module is a corollary of the generator together with the one abstract transport principle isBigOWith_comp_of_map_eq: a weak-Orlicz upper-tail bound sees only the law of its random variable, so it survives composition with any measure-preserving self-map, for Orlicz profile Psi (not only gammaSigma sigma).

What is delivered

• the generator and its norm form (cubeStreamIncrementLpNorm_eq_streamIncrementLpNorm_translate);
• e.kmn.bounds at every cube — Gamma_{2/p} for the per-cube mass, Gamma_2 for the per-cube norm, Gamma_1 for its square. The Gamma_2-per-cube norm estimate is the "translated Gamma_2 wave estimate applied cube by cube" that the corrected e.bL Step-3 aggregation (with the exponent bookkeeping) requires, and that Provider/Multiscale/ConclusionSeam2.lean recorded as its missing Step-2 input. Nothing in this module changed; ConclusionSeam2's own root-collapse route also remains proved;
• e.kl.bounds.large at every cube — the head-plus-decaying-tail form of streamIncrementLpMass_head_tail_gain / streamIncrementLpNorm_head_tail_gain transported to Q, with the gain read at Q.scale;
• the abstract translate transport on the cutoff carrier, isBigOWith_comp_translateCutoffSample and measureReal_preimage_translateCutoffSample: any law-level bound, and any event probability, proved at the origin holds verbatim at every real translate of the cutoff sample. This is the shape of the manuscript's own reduction "by stationarity, it suffices to prove the case z = 0", and the shape a translate family for e.bL.multiscale would be consumed through. NOTE: e.bL.multiscale itself has no realization in this repository, and none is asserted here.

Conventions

• cubeAverage Q is CoarseGraining's average over the HALF-O cube cubeSet Q, which is what CoarseGraining's partition identity and Provider/Stream/IncrementConcentration.lean use; streamIncrementLpMass is the average over the O origin cube. The two agree (streamIncrementLpMass_eq_cubeAverage), the boundary being null.
• Q.scale replaces the origin-cube index l everywhere: a per-cube statement at Q is the origin statement at l = Q.scale.

Main definitions

• cubeStreamIncrementLpNorm, cubeStreamIncrementLpTail.

Main results

• cubeAverage_streamIncrementLpDensity_eq_streamIncrementLpMass_translate.
• isBigOWith_comp_of_map_eq, isBigOWith_comp_translateSequence, isBigOWith_comp_translateCutoffSample, measureReal_preimage_translateCutoffSample.
• isBigOWith_gammaSigma_cubeAverage_streamIncrementLpDensity, isBigOWith_gammaSigma_cubeStreamIncrementLpNorm, isBigOWith_gammaSigma_cubeAverage_streamIncrementLpDensity_cutoffLaw.
• cubeStreamIncrementLpNorm_head_tail_gain.

References

• ABK26, e.kmn.bounds, (its "R^d-stationarity" is the step proved locally here); e.kl.bounds.large; e.km.kn.Lp; l.bad.event.lemma, (the "by stationarity" reduction, with z in R^d).
• Provider/Stream/IncrementLaw.lean, Cutoff/Symmetry.lean — the two halves of the stationarity step that this module composes.

The generator: the per-cube mass as a translated origin-cube mass

theorem Algsuperdiff.Section3.Provider.Stream.cubeAverage_streamIncrementLpDensity_eq_streamIncrementLpMass_translate {d : ℕ} {p : ℝ} (hp : 0 < p) (Q : HCPolySupport.TriadicCube d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : HCPolySupport.cubeAverage Q (streamIncrementLpDensity p n m omega) = streamIncrementLpMass p Q.scale n m (Frozen.Assumptions.ShellField.translateSequence (HCPolySupport.triadicCubeShift Q) omega)

The stationarity reduction, at the level of the observable. The volume-normalized L^p mass of a stream increment on an A triadic cube Q is the origin-cube mass at the scale of Q, read at the sample translated by the base point triadicCubeShift Q of Q.

This is an exact identity of functions of the sample — not an identity in law — and it is what makes every proved origin-cube estimate transport verbatim to every cube.

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

The volume-normalized L^p norm ‖k_m - k_n‖_{L^p(Q)} of a stream increment on an arbitrary triadic cube Q.

Equations

• Algsuperdiff.Section3.Provider.Stream.cubeStreamIncrementLpNorm p Q n m omega = HCPolySupport.cubeAverage Q (Algsuperdiff.Section3.Provider.Stream.streamIncrementLpDensity p n m omega) ^ p⁻¹

theorem Algsuperdiff.Section3.Provider.Stream.cubeStreamIncrementLpNorm_eq_streamIncrementLpNorm_translate {d : ℕ} {p : ℝ} (hp : 0 < p) (Q : HCPolySupport.TriadicCube d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : cubeStreamIncrementLpNorm p Q n m omega = streamIncrementLpNorm p Q.scale n m (Frozen.Assumptions.ShellField.translateSequence (HCPolySupport.triadicCubeShift Q) omega)

The norm form of the generator.

theorem Algsuperdiff.Section3.Provider.Stream.cubeStreamIncrementLpNorm_nonneg {d : ℕ} {p : ℝ} (hp : 0 < p) (Q : HCPolySupport.TriadicCube d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : 0 ≤ cubeStreamIncrementLpNorm p Q n m omega

Transport of a weak-Orlicz bound along a measure-preserving self-map

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_comp_of_map_eq {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {T : Omega → Omega} (hT : Measurable T) (hmap : MeasureTheory.Measure.map T mu = mu) {Psi : ℝ → ℝ} {X : Omega → ℝ} (hX : Measurable X) {A : ℝ} (h : HCPolySupport.IndependentSums.IsBigOWith mu Psi X A) : HCPolySupport.IndependentSums.IsBigOWith mu Psi (fun (omega : Omega) => X (T omega)) A

The abstract transport principle. A weak-Orlicz upper-tail bound sees only the law of its random variable, so it survives composition with any measure-preserving self-map of the sample space — for every Orlicz profile Psi, not only for gammaSigma sigma.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_comp_translateSequence {d : ℕ} (M : ABKModel d) (z : HCPolySupport.Vec d) {Psi : ℝ → ℝ} {X : Cutoff.ShellSeq d → ℝ} (hX : Measurable X) {A : ℝ} (h : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) Psi X A) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) Psi (fun (omega : Cutoff.ShellSeq d) => X (Frozen.Assumptions.ShellField.translateSequence z omega)) A

Every weak-Orlicz bound on a measurable shell-sequence observable holds verbatim for the observable read at the jointly translated sample.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_comp_translateCutoffSample {d : ℕ} (M : ABKModel d) (z : HCPolySupport.Vec d) {Psi : ℝ → ℝ} {X : Cutoff.CutoffSample d → ℝ} (hX : Measurable X) {A : ℝ} (h : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) Psi X A) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) Psi (fun (omega : Cutoff.CutoffSample d) => X (Cutoff.translateCutoffSample z omega)) A

The translate transport on the cutoff carrier. Every weak-Orlicz bound proved for a measurable observable of the cutoff sample holds verbatim for the observable read at every translate of the sample.

This is the shape in which a translate family for an origin-only display is consumed: whatever bound is available at the origin-centred cube is available, with the same amplitude and the same Orlicz profile, at z + cu_n for every z : Vec d. Nothing here asserts any particular origin bound.

theorem Algsuperdiff.Section3.Provider.Stream.measureReal_preimage_translateCutoffSample {d : ℕ} (M : ABKModel d) (z : HCPolySupport.Vec d) {E : Set (Cutoff.CutoffSample d)} (hE : MeasurableSet E) : (↑(Cutoff.cutoffSampleLaw M)).real (Cutoff.translateCutoffSample z ⁻¹' E) = (↑(Cutoff.cutoffSampleLaw M)).real E

The event form of the manuscript's "by stationarity" reduction: a translated event has exactly the probability of the original one, for every real translation vector.

Measurability of the transported observables

e.kmn.bounds at every triadic cube

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_cubeAverage_streamIncrementLpDensity {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma (2 / p)) (fun (omega : Cutoff.ShellSeq d) => HCPolySupport.cubeAverage Q (streamIncrementLpDensity p n m omega)) (streamIncrementLpMassScale M p n m)

e.kmn.bounds at every cube. The Gamma_{2/p} estimate of ABK26's e.kmn.bounds holds at every triadic cube Q, with the SAME amplitude as at the origin cube of the same scale.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_cubeStreamIncrementLpNorm {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (cubeStreamIncrementLpNorm p Q n m) (streamIncrementLpNormScale M p n m)

The per-cube Gamma_2 L^p-norm estimate. This is the "translated Gamma_2 wave estimate applied cube by cube" of the corrected e.bL Step-3 aggregation (exponents), and the Step-2 input recorded as missing by Provider/Multiscale/ConclusionSeam2.lean; the per-cube route is consumed there through isBigOWith_gammaSigma_cubeAverage_streamIncrementLpDensity_cutoffLaw (in LayerPerCubePricing.lean and ConclusionSeam2PerCube.lean; attribution corrected).

No large-scale gain is claimed here: this is the Q-uniform envelope of e.kmn.bounds. The gain is cubeStreamIncrementLpNorm_head_tail_gain.

The estimates on the cutoff carrier

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_cubeAverage_streamIncrementLpDensity_cutoffLaw {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (2 / p)) (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.cubeAverage Q (streamIncrementLpDensity p n m ↑omega)) (streamIncrementLpMassScale M p n m)

The per-cube Gamma_{2/p} mass estimate, read on the lower-tail cutoff carrier.

e.kl.bounds.large at every triadic cube

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

The per-cube tail of the head-plus-gain decomposition: the proved origin-cube tail streamIncrementLpTail at scale Q.scale, read at the sample translated by the base point of Q.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.cubeStreamIncrementLpTail_nonneg {d : ℕ} (M : ABKModel d) (p : ℝ) (Q : HCPolySupport.TriadicCube d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : 0 ≤ cubeStreamIncrementLpTail M p Q n m omega

theorem Algsuperdiff.Section3.Provider.Stream.cubeStreamIncrementLpNorm_head_tail_gain {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) (Q : HCPolySupport.TriadicCube d) : (∀ (omega : Cutoff.ShellSeq d), cubeStreamIncrementLpNorm p Q n m omega ≤ streamIncrementLpMassHead M p n m ^ p⁻¹ + cubeStreamIncrementLpTail M p Q n m omega ^ p⁻¹) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => cubeStreamIncrementLpTail M p Q n m omega ^ p⁻¹) (streamIncrementLpGainScale M p Q.scale n m ^ p⁻¹)

The norm form of the previous display: the per-cube L^p norm is a deterministic head plus a tail obeying a Gamma_2 bound whose scale carries the gain with its exponent divided by p. At p = 4 this is the 3^{-(d/8)(Q.scale - m)} gain of the third term of e.wave.influence.bound, now available at every cube rather than only at cu_l.