Coarse-graining support: Support.Book.Ch04.Theorems.RestrictionIndependence

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Restriction-local independence and coloring lemmas

This module owns the finite-family independence consequences of the explicit restriction-unit-range assumption. It concerns RestrictionSigmaR and whole-restriction-local random variables only; source-local finite independence belongs in a separate module.

theorem HCPolySupport.Book.Ch04.iIndep_restrictionSigmaR_of_restrictionUnitRangeDependentLaw {d : ℕ} {ι : Type u_1} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {U : ι → Set (Vec d)} (hU : ∀ (i : ι), MeasurableSet (U i)) (hP : RestrictionUnitRangeDependentLaw P) (hsep : Pairwise fun (i j : ι) => AreUnitSeparated (U i) (U j)) : ProbabilityTheory.iIndep (fun (i : ι) => RestrictionSigmaR (U i) ⋯) P

Restriction-unit-range dependence gives independence of any pairwise separated finite family of carrier restriction σ-algebras.

theorem HCPolySupport.Book.Ch04.iIndepFun_of_restrictionUnitRangeDependentLaw_of_pairwise_separated {d : ℕ} {ι : Type u_1} {β : ι → Type u_2} [(i : ι) → MeasurableSpace (β i)] {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {U : ι → Set (Vec d)} {X : (i : ι) → RegCoeffField d → β i} (hU : ∀ (i : ι), MeasurableSet (U i)) (hP : RestrictionUnitRangeDependentLaw P) (hX : ∀ (i : ι), IsRestrictionLocalRandomVariable (U i) ⋯ (X i)) (hsep : Pairwise fun (i j : ι) => AreUnitSeparated (U i) (U j)) : ProbabilityTheory.iIndepFun X P

Restriction-local random variables indexed by pairwise separated observation sets are independent under restriction-unit-range dependence.

theorem HCPolySupport.Book.Ch04.iIndepFun_descendantsAtScaleScaleColorClass_of_restrictionUnitRangeDependentLaw {d : ℕ} {Q : TriadicCube d} {k : ℤ} {c : ScaleColor d k} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {β : ↥(descendantsAtScaleScaleColorClass Q k c) → Type u_1} [(R : ↥(descendantsAtScaleScaleColorClass Q k c)) → MeasurableSpace (β R)] {X : (R : ↥(descendantsAtScaleScaleColorClass Q k c)) → RegCoeffField d → β R} (hP : RestrictionUnitRangeDependentLaw P) (hX : ∀ (R : ↥(descendantsAtScaleScaleColorClass Q k c)), IsRestrictionLocalRandomVariable (cubeSet ↑R) ⋯ (X R)) : ProbabilityTheory.iIndepFun X P

A single scale-color class of descendant cube observables is an independent family under the explicit restriction-unit-range dependence assumption.