Scaling #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Exact scaling of local cube controls #
The local value control is homogeneous under the shell scaling action. This
is a deterministic statement; probabilistic transport belongs in
LawTransport.
theorem
Algsuperdiff.Section3.Cutoff.localCubeControl_triadicScale
{d : ℕ}
(gamma : ℝ)
(ell k : ℤ)
(j : Frozen.Assumptions.ShellField d)
:
localCubeControl ell (Frozen.Assumptions.ShellField.triadicScale gamma k j) = Real.rpow 3 (gamma * ↑k) * localCubeControl (ell - k) j
A triadically scaled shell has local control equal to its amplitude
factor times the control of the original shell on the shifted cube scale
ell - k.