High-contrast homogenization: Provider.Recurrence.AdaptedColourIndependence

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

Independence of the responses of one colour class

Putting the colour separation together with the grouping induction gives the second step of l.fixed.geometry.matrix.averaging: the coarse responses of a same-colour family of aligned adapted cells form a jointly independent family.

The random variables are recorded in the two forms the averaging step uses. The first is the bare entry 𝐀(z + ⋄_j^𝐪)_{αβ} of the coarse response. The second is the entry of the normalized centred block R^{-1/2}(𝐀 - E)R^{-1/2}, which is the variable the printed proof calls X_i; normalization and centring by deterministic blocks are a fixed affine map of the entries, so they preserve both locality and independence. Since the moment inequality applied to the family asks for measurability against the global structure of the coefficient space, that consequence of locality is recorded as well.

The index type is left arbitrary and the colour condition is carried as a hypothesis, so a colour class of any concrete family can be used; the specialization to the class {w ∈ Z : w ≡ c} of a finite family Z of aligned indices is stated last, in the subtype form a finite-sum moment inequality consumes.

The adapted cells are Borel

theorem HCPolySupport.HighContrast.Recurrence.measurableSet_adaptedCellAt {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (j : ℤ) (w : Fin d → ℤ) : MeasurableSet (adaptedCellAt q j w)

An aligned adapted cell is a Borel set, being open.

Independence of the coarse responses

The normalized centred block

theorem HCPolySupport.HighContrast.Recurrence.measurable_toFullBlockMat_normalizedBlock_coeffSigma {d : ℕ} {U : Set (Vec d)} (hU : ∀ (α β : BlockCoord d), Measurable fun (a : CoeffSpace d) => blockMatEntry (coarseBlock U a) α β) (E F : BlockMat d) (α β : BlockCoord d) : Measurable fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock U a) E) F) α β

The entries of the normalized centred block of a cell are measurable for the sigma-field of that cell. Normalization and centring by deterministic blocks are a fixed real-linear map of the entries of the coarse response.

theorem HCPolySupport.HighContrast.Recurrence.measurable_toFullBlockMat_normalizedBlock_adaptedCellAt_coeffSigma {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (j : ℤ) (w : Fin d → ℤ) (E F : BlockMat d) (α β : BlockCoord d) : Measurable fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellAt q j w) a) E) F) α β

The entries of the normalized centred block of an aligned adapted cell are measurable for the sigma-field of that cell.

theorem HCPolySupport.HighContrast.Recurrence.measurable_toFullBlockMat_normalizedBlock_adaptedCellAt {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (j : ℤ) (w : Fin d → ℤ) (E F : BlockMat d) (α β : BlockCoord d) : Measurable fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellAt q j w) a) E) F) α β

The entries of the normalized centred block of an aligned adapted cell are measurable for the global structure of the coefficient space.

theorem HCPolySupport.HighContrast.Recurrence.iIndepFun_toFullBlockMat_normalizedBlock_adaptedCellAt {d : ℕ} {ι : Type u_1} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (hP : IsUnitRangeLaw P) {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) {z : ι → Fin d → ℤ} (hinj : Function.Injective z) (hcol : ∀ (n n' : ι), (fun (i : Fin d) => ↑(z n i)) = fun (i : Fin d) => ↑(z n' i)) (E F : BlockMat d) (α β : BlockCoord d) : ProbabilityTheory.iIndepFun (fun (n : ι) (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellAt q j (z n)) a) E) F) α β) P

The normalized centred responses of a same-colour family of distinct aligned adapted cells are jointly independent, entry by entry. These are the variables X_i of l.fixed.geometry.matrix.averaging.

One colour class of a finite family

theorem HCPolySupport.HighContrast.Recurrence.iIndepFun_toFullBlockMat_normalizedBlock_colourClass {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (hP : IsUnitRangeLaw P) {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hj : l ≤ j) (Z : Finset (Fin d → ℤ)) (c : Fin d → ZMod 3) (E F : BlockMat d) (α β : BlockCoord d) : ProbabilityTheory.iIndepFun (fun (v : ↥({v ∈ Z | (fun (i : Fin d) => ↑(v i)) = c})) (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellAt q j ↑v) a) E) F) α β) P

The normalized centred responses of one colour class of a finite family of aligned adapted cells are jointly independent. This is the specialization the finite-sum moment inequality is applied to: the index type is the colour class {w ∈ Z : w ≡ c mod 3}, and the family is centred and normalized by the deterministic blocks E and R.