High-contrast homogenization: Provider.Recurrence.AdaptedCellMeasurability

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

Consumers of the measurability clause over adapted cells

The measurability of the variational coarse block holds unconditionally on every adapted cell. This file records what the fixed-grid estimates draw from it, together with the symmetry of the annealed block, which needs nothing at all.

The annealed block inherits pathwise symmetry: its entries are integrals of the entries of the response, and the response is symmetric on every cell, so the adapted means E_r^q are symmetric with no hypothesis.

The scalarization display of l.fixed.geometry.matrix.averaging carries a measurability binder on the 4d² entries of the normalized centered block F^{-1/2}(𝐀 - E)F^{-1/2}. Normalization and centering are a fixed affine map of the entries, so that binder is discharged by the measurability clause on 𝐀(U; ·) itself. With the clause now proved on the adapted cells, the display applies to the centered moment v_r^q and to the centered aligned responses X_z of the fixed-grid recurrence with no hypothesis beyond the grid's own.

The annealed block is symmetric

theorem HCPolySupport.HighContrast.Recurrence.isSymmetricBlockMat_annealedBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (U : Set (Vec d)) : IsSymmetricBlockMat (annealedBlock P U)

The annealed block of any cell is symmetric. Its entries are the integrals of the entries of the coarse response, which is symmetric pathwise, so no integrability or measurability hypothesis enters.

theorem HCPolySupport.HighContrast.Recurrence.isSymmetricBlockMat_adaptedMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (r : ℤ) : IsSymmetricBlockMat (adaptedMean P q r)

The adapted mean E_r^q is symmetric, with no hypothesis.

The normalized centered block is an affine image of the response

theorem HCPolySupport.HighContrast.Recurrence.toFullBlockMat_normalizedBlock_apply {d : ℕ} (H F : BlockMat d) (α β : BlockCoord d) : toFullBlockMat (normalizedBlock H F) α β = ∑ γ : BlockCoord d, ∑ δ : BlockCoord d, matSqrt (toFullBlockMat F)⁻¹ α δ * toFullBlockMat H δ γ * matSqrt (toFullBlockMat F)⁻¹ γ β

The entries of a normalized doubled block, expanded as a double sum over the entries of the block itself.

theorem HCPolySupport.HighContrast.Recurrence.toFullBlockMat_blockSub_apply {d : ℕ} (A B : BlockMat d) (α β : BlockCoord d) : toFullBlockMat (blockSub A B) α β = toFullBlockMat A α β - toFullBlockMat B α β

The entries of a difference of doubled blocks.

theorem HCPolySupport.HighContrast.Recurrence.aestronglyMeasurable_toFullBlockMat_normalizedBlock_blockSub {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hmeas : HasMeasurableCoarseBlock P U) (E F : BlockMat d) (α β : BlockCoord d) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (blockSub (coarseBlock U a) E) F) α β) P

The measurability binder of the scalarization display is discharged by the measurability clause. The normalized centered block F^{-1/2}(𝐀 - E)F^{-1/2} has entries that are fixed real-linear combinations of the entries of 𝐀, so their measurability is exactly HasMeasurableCoarseBlock.

The scalarization display on a measurable cell

The fixed-grid moments