High-contrast homogenization: Provider.Recurrence.ColourIndependence

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Joint independence of a unit-separated family of local sigma-fields

The unit-range assumption is a statement about two Borel sets at sup-distance at least one. The finite-range averaging lemma needs the joint independence of a whole finite family, and derives it by the grouping argument printed there: enumerate the family, observe that the union of the cells already treated stays at sup-distance at least one from the next cell, that the sigma-field of that union dominates the sigma-fields of its members, and induct.

Both ingredients are elementary here. Sup-separation from a fixed set is inherited by any union of separated sets, because the separation is a pointwise condition. And the sigma-field F(U) is generated by the linear statistics with test support inside U, so it grows with U; the intersection of finitely many sets, each measurable for the sigma-field of its own cell, is therefore measurable for the sigma-field of the union. No partition of unity is needed: the printed proof uses one to obtain the equality of the sigma-field of the union with the join, whereas the induction consumes only the inclusion of the join in the sigma-field of the union.

The conclusions are stated for an arbitrary index type: joint independence of the sigma-fields, and joint independence of any family of random variables each measurable for the sigma-field of its own cell. The last lemma records that locally measurable random variables are measurable for the global structure, which is what a moment inequality applied to them will ask for.

Unit separation is closed under finite unions on one side

theorem HCPolySupport.HighContrast.Recurrence.unitSeparated_biUnion_right {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} {V : ι → Set (Vec d)} {s : Finset ι} (h : ∀ i ∈ s, UnitSeparated U (V i)) : UnitSeparated U (⋃ i ∈ s, V i)

A set separated from each member of a finite family is separated from their union. Sup-separation is a pointwise condition, so this is immediate.

The sigma-field of a union dominates the join

Joint independence

theorem HCPolySupport.HighContrast.Recurrence.iIndep_coeffSigma_of_pairwise_unitSeparated {d : ℕ} {ι : Type u_1} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (hP : IsUnitRangeLaw P) {U : ι → Set (Vec d)} (hU : ∀ (i : ι), MeasurableSet (U i)) (hsep : Pairwise fun (i j : ι) => UnitSeparated (U i) (U j)) : ProbabilityTheory.iIndep (fun (i : ι) => coeffSigma d (U i)) P

A pairwise unit-separated family of local sigma-fields is jointly independent. This is the grouping induction of l.fixed.geometry.matrix.averaging, carried out in the dialect of unit range of dependence: at each step the unit-range assumption separates the next cell from the union of those already taken.

theorem HCPolySupport.HighContrast.Recurrence.iIndepFun_of_measurable_coeffSigma {d : ℕ} {ι : Type u_1} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (hP : IsUnitRangeLaw P) {U : ι → Set (Vec d)} (hU : ∀ (i : ι), MeasurableSet (U i)) {β : ι → Type u_2} [(i : ι) → MeasurableSpace (β i)] {X : (i : ι) → CoeffSpace d → β i} (hX : ∀ (i : ι), Measurable (X i)) (hsep : Pairwise fun (i j : ι) => UnitSeparated (U i) (U j)) : ProbabilityTheory.iIndepFun X P

A family of locally measurable random variables over pairwise unit-separated cells is jointly independent. This is the form the moment inequalities of the finite-range averaging lemma consume.

theorem HCPolySupport.HighContrast.Recurrence.measurable_of_measurable_coeffSigma {d : ℕ} {U : Set (Vec d)} {β : Type u_1} [MeasurableSpace β] {X : CoeffSpace d → β} (hX : Measurable X) : Measurable X

A random variable measurable for the sigma-field of a cell is measurable for the global structure of the coefficient space.