TranslatedTransport #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
One-shell law transport under real translations #
ABK26 upgrades the small-cube estimate e.km.kn.Linfty.smallcube to the large
cube cu_l by covering cu_l with translated copies of a small cube and
taking a maximum. Every translated copy must carry the same amplitude as the
copy at the origin, which is where the stationarity half of the frozen (J1)
assumption enters.
The frozen (J1) stationarity field is stationarity of the zero shell law, and
the frozen prefix supplies only the one-coordinate marginal scaling law
e.diff.law.shift. No joint shift invariance of the shell sequence is claimed
or used. What is proved here is exactly the one-shell statement: for a
measurable real observable F of a single shell,
law of F(j_k(· + z)) = law of F(j_k),
which follows from (J1) stationarity through the pointwise commutation
translate z ∘ triadicScale γ k = triadicScale γ k ∘ translate (3^{-k} z).
The module then transports the three single-shell inputs of the small-cube
argument to an arbitrary base point z:
- the value gauge
e.jk.O; - the derivative gauge
e.nabla.jk.Oand its sum overk ∈ (n, m]; - the mean-zero and independence facts for the shell values at
z, the first of which is the frozen (J1) mean-zero field read at the point3^{-k} zrather than at the origin.
Main results #
Algsuperdiff.Section3.Provider.Stream.translate_triadicScaleAlgsuperdiff.Section3.Provider.Stream.map_shellObservable_translate_eqAlgsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_shellObservable_translateAlgsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_shell_entryAlgsuperdiff.Section3.Provider.Stream.integral_shell_entry_eq_zeroAlgsuperdiff.Section3.Provider.Stream.iIndepFun_shell_entryAlgsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_shellDerivNormSum_Ioc_translate
References #
- ABK26, (J1).
- ABK26,
e.diff.law.shift, the marginal scaling law. - ABK26,
e.jk.O;e.nabla.jk.O. - ABK26,
e.km.kn.Linfty.
Commutation of the two frozen actions #
The frozen translation and triadic scaling actions commute after rescaling
the shift: j(3^{-k}(· + z)) = (j(· + 3^{-k} z))(3^{-k} ·). Both sides are
compared through ShellField.ext, so the stored derivatives need no separate
argument.
The one-shell translated law #
Stationarity of the zero shell, transported to every shell index: for a
measurable real observable F of a single shell, the law of F(j_k(· + z))
under the shell-sequence law is the law of F(j_k).
Only the one-coordinate marginal scaling law and the (J1) stationarity of the zero shell are used; no joint shift invariance of the sequence is claimed.
Transport a one-sided stretched-exponential estimate through an exact push-forward identity. The weak-Orlicz upper-tail relation only sees the law of the random variable.
Every one-shell Γ_σ estimate holds verbatim at every translated base
point.
The translated single-shell gauges #
ABK26's e.jk.O on the translated cube z + cu_k.
ABK26's e.nabla.jk.O on the translated cube z + cu_ell, for ell ≤ k.
The translated form of ABK26's e.nabla.km.kn.infty: the summed derivative
gauges on the translated small cube z + cu_n obey the same Γ₂ bound as at
the origin.
The translated summed first-derivative gauge estimate, with the second-derivative term discarded.
The shell values at an arbitrary base point #
The translated value gauge dominates every matrix entry of the shell at the translation vector itself, because the origin lies in every origin cube.
ABK26's e.jk.O read entrywise at an arbitrary point:
|j_k(z)_{il}| ≤ O_{Γ₂}(3^{γk}), with the amplitude independent of z.
ABK26's "j_k is mean zero" at every point: the frozen (J1) mean-zero
field holds at every point of space, so transporting it through the frozen
marginal scaling law centres the shell values at every base point.
The frozen shell independence, read on the scalar entries of the shell values at an arbitrary point.