LawTransport

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

Marginal-law and stationary transport for local controls

Only one-coordinate marginal scaling is used here. In particular, no claim of joint shift invariance for the shell sequence is made or needed.

theorem Algsuperdiff.Section3.Cutoff.map_shellObservable_eq_zero_triadicScale {d : ℕ} (M : ABKModel d) (k : ℤ) (F : Frozen.Assumptions.ShellField d → ℝ) (hF : Measurable F) : MeasureTheory.Measure.map (fun (omega : ShellSeq d) => F (omega k)) ↑M.P = MeasureTheory.Measure.map (fun (j : Frozen.Assumptions.ShellField d) => F (Frozen.Assumptions.ShellField.triadicScale M.gamma k j)) ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)

The law of a measurable observable of shell k is the law of the same observable after the exact triadic action on the zero shell.

theorem Algsuperdiff.Section3.Cutoff.map_localCubeControl_shell_eq_zero {d : ℕ} (M : ABKModel d) (ell k : ℤ) : MeasureTheory.Measure.map (fun (omega : ShellSeq d) => localCubeControl ell (omega k)) ↑M.P = MeasureTheory.Measure.map (fun (j : Frozen.Assumptions.ShellField d) => Real.rpow 3 (M.gamma * ↑k) * localCubeControl (ell - k) j) ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)

Distributional form of the local-control transport. This uses only the one-coordinate marginal equality for shell k.

theorem Algsuperdiff.Section3.Cutoff.map_zeroObservable_translate_eq {d : ℕ} (M : ABKModel d) (z : HCPolySupport.Vec d) (F : Frozen.Assumptions.ShellField d → ℝ) (hF : Measurable F) : MeasureTheory.Measure.map (fun (j : Frozen.Assumptions.ShellField d) => F (Frozen.Assumptions.ShellField.translate z j)) ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P) = MeasureTheory.Measure.map F ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)

Stationarity of the zero shell transports the distribution of any measurable one-shell observable through a real translation.

theorem Algsuperdiff.Section3.Cutoff.map_translatedUnitCubeControl_zero_eq {d : ℕ} (M : ABKModel d) (z : HCPolySupport.Vec d) : MeasureTheory.Measure.map (translatedUnitCubeControl z) ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P) = MeasureTheory.Measure.map Frozen.Assumptions.ShellField.unitCubeValueNorm ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)

The exact translated unit-cube control has the same zero-shell law as the origin unit-cube control.