High-contrast homogenization: Provider.Recurrence.CellMuMeasurability

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

The measurability of the coarse block on a bounded open cell

The coarse-grained energy of a bounded open cell of positive volume is measurable in the coefficient field, for the sigma-field the coefficient space carries — the global one generated by the smooth linear statistics. This is the measurability half of the first of the coarse-block properties taken from HC, and with it the whole clause holds on the adapted cells ⋄_j^q and their aligned translates.

The argument has three moves. A field of the coefficient space is represented, up to a null set, by a field of the exact coarse source, and the representative map is measurable for the two global sigma-fields; that is already available. Every coarse-source field is uniformly elliptic on every Euclidean ball, hence on the bounded cell, so it lies in one of the countably many quantitative ellipticity slices of the cell; and the slice events are measurable. On each slice the coarse-grained energy is measurable, being the infimum of countably many fixed competitor energies. Gluing the slices gives measurability on the whole source, and composing with the representative map brings it back to the coefficient space.

Every coarse-source field lies in a slice of a bounded cell

theorem HCPolySupport.HighContrast.Recurrence.exists_subset_sourceEuclideanBall {d : ℕ} {U : Set (Vec d)} (hU : IsBoundedDomain U) : ∃ (R : ℝ), 1 ≤ R ∧ U ⊆ Source.Coarse.euclideanBall R

A bounded cell is contained in a Euclidean ball of radius at least one, the shape the coarse source's ellipticity data is indexed by.

theorem HCPolySupport.HighContrast.Recurrence.exists_source_isAEEllipticFieldOn {d : ℕ} {U : Set (Vec d)} (hUmeas : MeasurableSet U) (hUbdd : IsBoundedDomain U) (b : Source.Coarse.Carrier d) : ∃ (eps : ℝ), 0 < eps ∧ IsAEEllipticFieldOn eps eps⁻¹ U ↑b

A coarse-source field is almost everywhere uniformly elliptic on every bounded measurable cell.

theorem HCPolySupport.HighContrast.Recurrence.exists_source_aeeQuantitativeEllipticSlice {d : ℕ} {U : Set (Vec d)} (hUmeas : MeasurableSet U) (hUbdd : IsBoundedDomain U) (b : Source.Coarse.Carrier d) : ∃ (k : ℕ), AEEQuantitativeEllipticSlice U k ↑b

Every coarse-source field belongs to one of the countably many quantitative ellipticity slices of a bounded measurable cell.

The coarse-grained energy is measurable on the coarse source

theorem HCPolySupport.HighContrast.Recurrence.measurable_Mu_carrier_local {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (hUbdd : IsBoundedDomain U) (hvol : 0 < (MeasureTheory.volume U).toReal) (P0 : BlockVec d) : Measurable fun (b : Source.Coarse.Carrier d) => Mu U P0 ↑b

The coarse-grained energy of a bounded open cell of positive volume is measurable on the exact coarse source, for the source's own sigma-field of that cell. The slices cover the source and are measurable there, and on each of them the energy is a countable infimum of fixed competitor energies. This is the local form: the energy of a cell sees only the field inside it.

theorem HCPolySupport.HighContrast.Recurrence.measurable_Mu_carrier {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (hUbdd : IsBoundedDomain U) (hvol : 0 < (MeasureTheory.volume U).toReal) (P0 : BlockVec d) : Measurable fun (b : Source.Coarse.Carrier d) => Mu U P0 ↑b

The coarse-grained energy of a bounded open cell of positive volume is measurable on the exact coarse source for its global sigma-field.

The measurability clause on the coefficient space

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

The coarse-grained energy of a bounded open cell of positive volume is measurable on the coefficient space. The representative map into the exact coarse source is measurable for the global sigma-fields and leaves the energy unchanged.

theorem HCPolySupport.HighContrast.Recurrence.hasMeasurableCoarseBlock_of_isBoundedDomain {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {U : Set (Vec d)} (hUopen : IsOpen U) (hUbdd : IsBoundedDomain U) (hvol : 0 < (MeasureTheory.volume U).toReal) : HasMeasurableCoarseBlock P U

The measurability of the variational coarse block, on every bounded open cell of positive volume and for every law at once.

The clause on the adapted cells

theorem HCPolySupport.HighContrast.Recurrence.hasMeasurableCoarseBlock_adaptedCell {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (j : ℤ) : HasMeasurableCoarseBlock P (adaptedCell q j)

The coarse response on an adapted cell is measurable in the coefficient field, for every law at once.

theorem HCPolySupport.HighContrast.Recurrence.hasMeasurableCoarseBlock_adaptedCellAt {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (j : ℤ) (w : Fin d → ℤ) : HasMeasurableCoarseBlock P (adaptedCellAt q j w)

The coarse response on an aligned adapted cell is measurable in the coefficient field, for every law at once.

theorem HCPolySupport.HighContrast.Recurrence.hasMeasurableCoarseBlock_adaptedCell_of_isRoundedGrid {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) (j : ℤ) : HasMeasurableCoarseBlock P (adaptedCell q j)

The measurability clause at a rounded adapted grid: the grid's positivity is part of IsRoundedGrid.