TranslatedLargeCubeW1Inf

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

The summed derivative-stream bound on a translated cube

LargeCubeW1Inf.lean proves local versions of ABK26's e.W1inf.jL.bound.smaller and e.W.1.inf.bound on the centered cube cu_l. The proof of l.bad.event.lemma on the branch n < m needs both displays on the translated cube z + cu_m, since the good local sensitivity event e.good.local.events is stated at z + cu_m.

This module re-runs the covering half of the source proof at an arbitrary base point. Nothing else changes: the covering family subcubeShifts and the maximum lemma l.maximums.Gamma.s are the proved ones, and each translated member of the cover is priced by the proved translated single-shell display isBigOWith_gammaSigma_shellDerivGauge_cube_translate (ABK26's e.nabla.jk.O at a base point, which is available at the same amplitude as at the origin by the one-shell stationarity of TranslatedTransport.lean). The base points compose: covering the translated cube z + cu_l by translates of cu_k is covering cu_l by translates of cu_k and then translating the shell, which is translate_translate below.

The amplitudes are therefore identical to the centered ones; the base point z is a silent parameter throughout.

Main results

• Algsuperdiff.Section3.Provider.Stream.translate_translate
• Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_shellDerivGaugeCover_translate
• Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_largeCubeDerivGauge_lt_translate
• Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_largeCubeDerivGauge_translate

References

• ABK26, e.W.1.inf.bound.
• ABK26, e.W1inf.jL.bound.smaller.
• ABK26, e.nabla.jk.O; l.maximums.Gamma.s.
• ABK26, l.bad.event.lemma.

Elementary rewrites

Composition of the translation action

theorem Algsuperdiff.Section3.Provider.Stream.translate_translate {d : ℕ} (a b : HCPolySupport.Vec d) (j : Frozen.Assumptions.ShellField d) : Frozen.Assumptions.ShellField.translate a (Frozen.Assumptions.ShellField.translate b j) = Frozen.Assumptions.ShellField.translate (a + b) j

The frozen translation action composes: j((· + b) + a) = j(· + (a + b)).

The translated covering maximum

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_shellDerivGaugeCover_translate {d : ℕ} (M : ABKModel d) (l k : ℤ) (z : HCPolySupport.Vec d) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => shellDerivGaugeCover l k (Frozen.Assumptions.ShellField.translate z (omega k))) ((3 * max 1 (Real.log ↑(subcubeShifts d k l).card)) ^ 2⁻¹ * Real.rpow 3 ((M.gamma - 1) * ↑k))

The probabilistic half of e.W1inf.jL.bound.smaller at an arbitrary base point: the covering maximum of the translated own-scale derivative gauges obeys the single-shell Γ₂ estimate e.nabla.jk.O with the same amplitude as at the origin, since each member of the cover is itself a translate.

e.W1inf.jL.bound.smaller at a base point

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_largeCubeDerivGauge_lt_translate {d : ℕ} (M : ABKModel d) {l k : ℤ} (hkl : k < l) (z : HCPolySupport.Vec d) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => largeCubeDerivGauge l k (Frozen.Assumptions.ShellField.translate z (omega k))) (shellW1InfSmallerConst d * √(↑l - ↑k) * 3 ^ (M.gamma * ↑k))

ABK26's e.W1inf.jL.bound.smaller on the translated cube z + cu_l: for k < l,

3^k ‖∇j_k‖_{L∞(z+cu_l)} + 3^{2k} ‖∇²j_k‖_{L∞(z+cu_l)} ≤ O_{Γ₂}(C (l-k)^{1/2} 3^{γk}),

with the same dimensional constant as the centered display.

The uniform per-shell estimate at a base point

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_largeCubeDerivGauge_translate {d : ℕ} (M : ABKModel d) {l n k : ℤ} (hnk : n < k) (z : HCPolySupport.Vec d) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => largeCubeDerivGauge l k (Frozen.Assumptions.ShellField.translate z (omega k))) (shellW1InfConst d * √(max 1 (↑l - ↑n)) * 3 ^ (M.gamma * ↑k))

The per-shell estimate on z + cu_l, uniform in the two regimes of the source proof: for n < k,

3^k ‖∇j_k‖_{L∞(z+cu_l)} + 3^{2k} ‖∇²j_k‖_{L∞(z+cu_l)} ≤ O_{Γ₂}(C (1 ∨ (l-n))^{1/2} 3^{γk}).