Shared normalized stream observables and law transport

The general observable and its stationary law are shared by both moment-boosted exponent regimes. Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_comp_of_map {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {F : Omega → HCPolySupport.RegCoeffField d} (hF : Measurable F) {g : HCPolySupport.RegCoeffField d → ℝ} (hg : Measurable g) {Psi : ℝ → ℝ} {A : ℝ} (h : HCPolySupport.IndependentSums.IsBigOWith (MeasureTheory.Measure.map F mu) Psi g A) : HCPolySupport.IndependentSums.IsBigOWith mu Psi (fun (omega : Omega) => g (F omega)) A

A one-sided tail bound pulls back along a measurable map.

theorem Algsuperdiff.Section3.Provider.Stream.integral_eq_of_map_eq {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {f g : Omega → ℝ} (hf : Measurable f) (hg : Measurable g) (hmap : MeasureTheory.Measure.map f mu = MeasureTheory.Measure.map g mu) : ∫ (omega : Omega), f omega ∂mu = ∫ (omega : Omega), g omega ∂mu

Measurable real observables with the same law have equal integrals.

noncomputable def Algsuperdiff.Section3.Provider.Stream.normalizedCenteredLpMassRep {d : ℕ} (P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d) (p V : ℝ) (R : HCPolySupport.TriadicCube d) : HCPolySupport.RegCoeffField d → ℝ

Internal normalized centered cube-mass observable, reusable by both moment-boosted exponent regimes.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_normalizedCenteredLpMassRep {d : ℕ} (P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d) (p V : ℝ) (R : HCPolySupport.TriadicCube d) : Measurable (normalizedCenteredLpMassRep P p V R)

Measurability of the internal normalized centered cube-mass observable.

theorem Algsuperdiff.Section3.Provider.Stream.local_normalizedCenteredLpMassRep {d : ℕ} (P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d) (p V : ℝ) (R : HCPolySupport.TriadicCube d) : HCPolySupport.Book.Ch04.IsRestrictionLocalRandomVariable (HCPolySupport.cubeSet R) ⋯ (normalizedCenteredLpMassRep P p V R)

Locality of the internal normalized centered cube-mass observable.

theorem Algsuperdiff.Section3.Provider.Stream.map_normalizedCenteredLpMassRep_descendant_eq_origin {d : ℕ} (M : ABKModel d) (p V : ℝ) (n m j : ℤ) (hj : 0 ≤ j) (R : HCPolySupport.TriadicCube d) (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d j) 0) : MeasureTheory.Measure.map (normalizedCenteredLpMassRep (partitionStreamIncrementLaw M n m) p V R) (partitionStreamIncrementLaw M n m) = MeasureTheory.Measure.map (normalizedCenteredLpMassRep (partitionStreamIncrementLaw M n m) p V (HCPolySupport.originCube d 0)) (partitionStreamIncrementLaw M n m)

Stationarity gives every descendant of the normalized partition the same law as the origin local variable. This is the exact public-A rederivation of the structural part of CoarseGraining's private partition-average proof.