LocalScaling #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Spatial transport of the integral-local sigma-fields #
The marginal scaling action reads a field at r • x. This module proves, at
the generators of LocalSigmaR, that information on U after that action is
information on r • U before it. No restriction sigma-field is used here.
theorem
Algsuperdiff.Section3.Cutoff.measurable_smulReg_local
{d : ℕ}
(r : ℝ)
(hr : r ≠ 0)
(U : Set (HCPolySupport.Vec d))
:
Measurable (HCPolySupport.smulReg r hr)
Spatial rescaling transports CoarseGraining's integral-local sigma-field by the corresponding image of the observation set.
theorem
Algsuperdiff.Section3.Cutoff.measurable_triadicScale_local
{d : ℕ}
(gamma : ℝ)
(k : ℤ)
(U : Set (HCPolySupport.Vec d))
:
The literal triadic shell scaling action transports integral-local shell information from the contracted observation set to the original one.