RefinedIndependence

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

Aggregate independence from independent pairs

The two local views of each shell may be dependent on the same shell, but are independent at the prescribed spatial separation. This file is the purely measure-theoretic step which combines those within-shell independences with mutual independence across shells. It has no coefficient-field semantics.

@[reducible, inline]

abbrev Algsuperdiff.Probability.refinedSigma {Ω : Type u_1} {ι : Type u_2} (a b : ι → MeasurableSpace Ω) : ι × Bool → MeasurableSpace Ω

Split each index into its left and right local sigma-field.

Equations

• Algsuperdiff.Probability.refinedSigma a b p = bif p.2 then b p.1 else a p.1

theorem Algsuperdiff.Probability.iIndep_refinedSigma {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {κ a b : ι → MeasurableSpace Ω} (hκ : ProbabilityTheory.iIndep κ μ) (ha : ∀ (i : ι), a i ≤ κ i) (hb : ∀ (i : ι), b i ≤ κ i) (hab : ∀ (i : ι), ProbabilityTheory.Indep (a i) (b i) μ) : ProbabilityTheory.iIndep (refinedSigma a b) μ

The Boolean refinement of independently-paired sigma-fields is mutually independent.

theorem Algsuperdiff.Probability.indep_iSup_of_indep_of_iIndep {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {κ a b : ι → MeasurableSpace Ω} (hκ : ProbabilityTheory.iIndep κ μ) (hle : ∀ (i : ι), κ i ≤ mΩ) (ha : ∀ (i : ι), a i ≤ κ i) (hb : ∀ (i : ι), b i ≤ κ i) (hab : ∀ (i : ι), ProbabilityTheory.Indep (a i) (b i) μ) : ProbabilityTheory.Indep (⨆ (i : ι), a i) (⨆ (i : ι), b i) μ

Aggregate the two local sigma-fields from independent shell coordinates. This is the exact countable iSup theorem used by the cutoff range proof.