High-contrast homogenization: Provider.Recurrence.CellLocalMeasurability

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

The response of a cell is measurable for the sigma-field of that cell

The first of the coarse-block properties taken from HC asks for F(U)-measurability of 𝐀(U), not merely measurability: the coarse response of a cell must be a function of the coefficient field inside that cell. This file proves the clause in that form, on every bounded open cell of positive volume, hence on every adapted cell.

Only one step separates it from the measurability already proved. The representative map from the coefficient space into the exact coarse source carries the generating linear statistics of F(U) to the generating bilinear tests of the source's own sigma-field of U — the two families of test functions are the same, and the representative agrees with the field almost everywhere — so the map is measurable for the local sigma-fields and not only for the global ones. The coarse-grained energy of the cell is already known to be local on the source, and the entries of the response are its polarizations.

The local sigma-fields of the coefficient space are monotone

theorem HCPolySupport.HighContrast.Recurrence.coeffSigma_mono {d : ℕ} {U V : Set (Vec d)} (hUV : U ⊆ V) : coeffSigma d U ≤ coeffSigma d V

The sigma-fields F(U) grow with the cell: a test function supported in U is one supported in any larger set.

The representative map is local

theorem HCPolySupport.HighContrast.Recurrence.measurable_sourceRepresentative_local {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) : Measurable sourceRepresentative

The representative map is measurable for the sigma-fields of a cell: it pulls each generator of the source's sigma-field of U back to a generator of F(U), the test functions of the two families being the same and the representative agreeing with the field almost everywhere.

The response of a cell is measurable for the sigma-field of the cell

theorem HCPolySupport.HighContrast.Recurrence.measurable_Mu_coeffSigma {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (hUbdd : IsBoundedDomain U) (hvol : 0 < (MeasureTheory.volume U).toReal) (Q : BlockVec d) : Measurable fun (a : CoeffSpace d) => Mu U Q ↑↑a

The coarse-grained energy of a bounded open cell of positive volume is F(U)-measurable.

theorem HCPolySupport.HighContrast.Recurrence.measurable_blockMatEntry_coarseBlock_coeffSigma {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (hUbdd : IsBoundedDomain U) (hvol : 0 < (MeasureTheory.volume U).toReal) (α β : BlockCoord d) : Measurable fun (a : CoeffSpace d) => blockMatEntry (coarseBlock U a) α β

The measurability of the variational coarse block in its printed form: every entry of the coarse block response of a bounded open cell of positive volume is measurable for the sigma-field of that cell.

The clause on the adapted cells

theorem HCPolySupport.HighContrast.Recurrence.measurable_blockMatEntry_coarseBlock_adaptedCellAt {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (j : ℤ) (w : Fin d → ℤ) (α β : BlockCoord d) : Measurable fun (a : CoeffSpace d) => blockMatEntry (coarseBlock (adaptedCellAt q j w) a) α β

The coarse response of an aligned adapted cell is measurable for the sigma-field of that cell.