Realization

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

Provider: the measurable spatial realization of a stationary random field

Algsuperdiff/Probability/StationaryProjection.lean builds the stationary Hilbert layer over an abstract carrier Ω carrying an AddAction (Vec d) Ω and a translation-invariant measure μ. That layer is purely abstract: the docstring of Algsuperdiff.Probability.Stationary.measurePreserving_const_vadd records that only fixed-shift measurability is available there, "not joint measurability of the translation parameter and the field".

Every displayed quantity of l.approximation.stationary.by.local and l.corrector.limit lives instead on the space side: ‖·‖_{L²(cu_K)}, ⨍_{cu_K}, H¹₀(cu_K). Passing between the two sides requires the realization map

realize X ω : x ↦ X (x +ᵥ ω),

which is what this file provides, together with the measurability facts that make it usable under Fubini. This is item of the corrector-limit design.

Joint measurability of (x, ω) ↦ x +ᵥ ω is genuinely extra data over the abstract layer; it is taken here as Mathlib's existing class MeasurableVAdd₂ (Vec d) Ω, so that no new class and no new global instance is introduced. For L²-classes the realization is representative dependent (changing X on a μ-null set can change realize X ω at every point), so every statement below is made for an honest StronglyMeasurable representative and transported to Lp along a.e. equality at the point of use.

def Algsuperdiff.Section3.Provider.Corrector.realize {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] {E : Type u_2} (X : Ω → E) (ω : Ω) (x : HCPolySupport.Vec d) : E

The spatial realization of an abstract random field X at the sample ω: the field x ↦ X (x +ᵥ ω) on ℝᵈ. This is the map denoted X(x + ω) in the ergodic-theory literature and implicitly used throughout Section 3 whenever a stationary field is integrated over a cube.

Equations

• Algsuperdiff.Section3.Provider.Corrector.realize X ω x = X (x +ᵥ ω)

theorem Algsuperdiff.Section3.Provider.Corrector.realize_apply {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] {E : Type u_2} (X : Ω → E) (ω : Ω) (x : HCPolySupport.Vec d) : realize X ω x = X (x +ᵥ ω)

theorem Algsuperdiff.Section3.Provider.Corrector.isFiniteMeasure_volume_restrict_cubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (HCPolySupport.cubeSet Q))

The restricted Lebesgue measure of a triadic cube is finite.

theorem Algsuperdiff.Section3.Provider.Corrector.measurable_vadd_pair {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableSpace Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] : Measurable fun (p : HCPolySupport.Vec d × Ω) => p.1 +ᵥ p.2

Joint measurability of the translation action, in the order (space, sample).

theorem Algsuperdiff.Section3.Provider.Corrector.measurable_vadd_pair_swap {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableSpace Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] : Measurable fun (p : Ω × HCPolySupport.Vec d) => p.2 +ᵥ p.1

Joint measurability of the translation action, in the order (sample, space). This is the order in which the product measure μ.prod (volume.restrict …) is formed below.

theorem Algsuperdiff.Section3.Provider.Corrector.measurable_vadd_const_sample {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableSpace Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] (ω : Ω) : Measurable fun (x : HCPolySupport.Vec d) => x +ᵥ ω

The spatial translation at a fixed sample is measurable.

theorem Algsuperdiff.Section3.Provider.Corrector.stronglyMeasurable_realize {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableSpace Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] {E : Type u_2} [TopologicalSpace E] {X : Ω → E} (hX : MeasureTheory.StronglyMeasurable X) (ω : Ω) : MeasureTheory.StronglyMeasurable (realize X ω)

, per-sample form. For a measurable representative the spatial realization is measurable in the space variable, for every sample.

theorem Algsuperdiff.Section3.Provider.Corrector.stronglyMeasurable_uncurry_realize {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableSpace Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] {E : Type u_2} [TopologicalSpace E] {X : Ω → E} (hX : MeasureTheory.StronglyMeasurable X) : MeasureTheory.StronglyMeasurable fun (p : Ω × HCPolySupport.Vec d) => realize X p.1 p.2

, joint form. For a measurable representative the spatial realization is jointly measurable in the sample and the space variable. This is the fact the abstract stationary layer does not supply, and the one that makes the Fubini argument of RealizationTransfer.lean legitimate.

theorem Algsuperdiff.Section3.Provider.Corrector.stronglyMeasurable_uncurry_vecDot_realize {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableSpace Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] {X Y : Ω → HCPolySupport.HilbertVec d} (hX : MeasureTheory.StronglyMeasurable X) (hY : MeasureTheory.StronglyMeasurable Y) : MeasureTheory.StronglyMeasurable fun (p : Ω × HCPolySupport.Vec d) => HCPolySupport.vecDot (realize X p.1 p.2).toVec (realize Y p.1 p.2).toVec

, Fubini-ready form. The pointwise pairing of two realizations is jointly measurable.

theorem Algsuperdiff.Section3.Provider.Corrector.integral_comp_const_vadd {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : Ω → E) (x : HCPolySupport.Vec d) : ∫ (ω : Ω), g (x +ᵥ ω) ∂μ = ∫ (ω : Ω), g ω ∂μ

Real-shift Koopman transfer of expectations: a stationary expectation is unchanged by translating the sample. This is the real-parameter analogue of CoarseGraining's integer-shift Homogenization.IsStationaryR.integral_comp_translateReg, obtained from Algsuperdiff.Probability.Stationary.measurePreserving_const_vadd.

theorem Algsuperdiff.Section3.Provider.Corrector.integrable_comp_const_vadd {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] {E : Type u_2} [NormedAddCommGroup E] {g : Ω → E} (hg : MeasureTheory.Integrable g μ) (x : HCPolySupport.Vec d) : MeasureTheory.Integrable (fun (ω : Ω) => g (x +ᵥ ω)) μ

Stationary translation preserves integrability.

theorem Algsuperdiff.Section3.Provider.Corrector.integrable_vecDot {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X Y : Ω → HCPolySupport.HilbertVec d} (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : MeasureTheory.Integrable (fun (ω : Ω) => HCPolySupport.vecDot (X ω).toVec (Y ω).toVec) μ

The pointwise pairing of two square-integrable stationary fields is integrable on the sample space.

theorem Algsuperdiff.Section3.Provider.Corrector.integrable_prod_vecDot_realize {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (Q : HCPolySupport.TriadicCube d) {X Y : Ω → HCPolySupport.HilbertVec d} (hXm : MeasureTheory.StronglyMeasurable X) (hYm : MeasureTheory.StronglyMeasurable Y) (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) : MeasureTheory.Integrable (fun (p : Ω × HCPolySupport.Vec d) => HCPolySupport.vecDot (realize X p.1 p.2).toVec (realize Y p.1 p.2).toVec) (μ.prod (MeasureTheory.volume.restrict (HCPolySupport.cubeSet Q)))

, product integrability. The pointwise pairing of two realizations is integrable on the product of the sample space with a triadic cube. This is the hypothesis of the Fubini exchange used, and it also produces the per-sample square integrability of a realization on a cube.

theorem Algsuperdiff.Section3.Provider.Corrector.ae_memHilbertVectorL2_realize {d : ℕ} {Ω : Type u_1} [AddAction (HCPolySupport.Vec d) Ω] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (Q : HCPolySupport.TriadicCube d) {X : Ω → HCPolySupport.HilbertVec d} (hXm : MeasureTheory.StronglyMeasurable X) (hX : MeasureTheory.MemLp X 2 μ) : ∀ᵐ (ω : Ω) ∂μ, HCPolySupport.MemHilbertVectorL2 (HCPolySupport.cubeSet Q) (realize X ω)

, per-sample square integrability. For almost every sample the spatial realization of a stationary L² field is square integrable on any triadic cube, i.e. it is an honest element of CoarseGraining's L²(Q; ℝᵈ) scale.