High-contrast homogenization: Provider.Recurrence.DomainMuMeasurability

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

The coarse-grained energy of a general cell, as a countable infimum

The measurability among the coarse-block properties taken from HC is asked of the coarse response on a Lipschitz cell. CoarseGraining proves the variational quantity μ(U, P; ·) measurable only when U is a triadic cube; the obstruction is not mathematical but bookkeeping — the two facts its cube proof rests on are stated at cubeSet Q although their proofs never use anything but finiteness and positivity of the volume of U. This file transports those two facts to an arbitrary cell, so that the measurability clause becomes available on every bounded open cell of positive volume, the adapted cells among them.

The first is the identification of the variational quantity with the value of the Hilbert minimization problem attached to the canonical potential/solenoidal correction space: both are the infimum of the same block energies, one over the admissible block states and one over the dense generator submodule.

The second is the resulting countable presentation μ(U, P; a) = inf_n E(U, a; X_n) along a dense sequence of fixed smooth generators — fixed meaning independent of the coefficient field. Measurability of μ is then measurability of each fixed-competitor energy, which is CoarseGraining's carrier machinery and is already stated on an arbitrary cell.

The variational quantity is the Hilbert candidate

theorem HCPolySupport.HighContrast.Recurrence.mu_eq_aeeMuCandidate {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {lam Lam : ℝ} {a : CoeffField d} (hAEE : IsAEEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (P0 : BlockVec d) : Mu U P0 a = ((PotentialSolenoidalL2Data.ofSubmoduleClosures U).toAEEMuOperatorSystemData (AEEMuCoeffOperatorData.ofIsAEEllipticFieldOn hAEE hvol)).toMuHilbertRealization.muCandidate P0

The variational quantity of an arbitrary cell of positive finite volume is the canonical Hilbert candidate. The candidate is at most every admissible block energy, so it is at most μ; and the generator submodule is dense in the correction space and its affine fields are admissible, so μ is at most the candidate. This is CoarseGraining's cube statement with the cube removed.

The countable presentation along a dense generator sequence

theorem HCPolySupport.HighContrast.Recurrence.mu_eq_iInf_blockEnergyAverage {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {lam Lam : ℝ} {a : CoeffField d} (hAEE : IsAEEllipticFieldOn lam Lam U a) (hvol : 0 < (MeasureTheory.volume U).toReal) (P0 : BlockVec d) (xi : ℕ → ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) (hxi : DenseRange xi) : Mu U P0 a = ⨅ (n : ℕ), blockEnergyAverage U a (canonicalMuGeneratorAffineField P0 (xi n))

The variational quantity of an arbitrary cell is the infimum of the block energies of a fixed dense sequence of smooth generators. The sequence does not depend on the coefficient field, which is what makes the presentation a measurability tool.

The measurability engine on a general cell

theorem HCPolySupport.HighContrast.Recurrence.measurable_Mu_of_measurable_entryTest {d : ℕ} {Om : Type u_1} [mOm : MeasurableSpace Om] {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hUopen : IsOpen U) (hUfin : MeasureTheory.volume U ≠ ⊤) (hvol : 0 < (MeasureTheory.volume U).toReal) {A : Om → RegCoeffField d} (hSlice : ∀ (w : Om), AEEQuantitativeEllipticSlice U k (A w).toFun) (hEntry : ∀ (i j : Fin d) {φ : Vec d → ℝ}, ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → Measurable fun (w : Om) => entryTestR i j φ (A w)) (P0 : BlockVec d) : Measurable fun (w : Om) => Mu U P0 (A w).toFun

The coarse-grained energy of a general bounded open cell is measurable in the coefficient field, for any parameter space whose localized smooth entry tests are measurable and whose fields all lie in one quantitative ellipticity slice of the cell. This is CoarseGraining's carrier Mu engine with the cube removed: the countable presentation replaces μ by an infimum of fixed competitor energies, and each of those is measurable by the carrier's L² realization.

From the variational quantity to the coarse response

theorem HCPolySupport.HighContrast.Recurrence.measurable_blockMatEntry_coarseBlock_of_measurable_Mu {d : ℕ} {m : MeasurableSpace (CoeffSpace d)} {U : Set (Vec d)} (hMu : ∀ (Q : BlockVec d), Measurable fun (a : CoeffSpace d) => Mu U Q ↑↑a) (α β : BlockCoord d) : Measurable fun (a : CoeffSpace d) => blockMatEntry (coarseBlock U a) α β

Every entry of the coarse block response is measurable once the variational quantity is: the entries are the polarizations of μ(U, ·; a) at the doubled vectors built from a pair of basis directions. The sigma-field is arbitrary, so the reduction serves both the global sigma-field of the coefficient space and the local one of the cell.

theorem HCPolySupport.HighContrast.Recurrence.hasMeasurableCoarseBlock_of_measurable_Mu {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {U : Set (Vec d)} (hMu : ∀ (Q : BlockVec d), Measurable fun (a : CoeffSpace d) => Mu U Q ↑↑a) : HasMeasurableCoarseBlock P U

The measurability of the variational coarse block, on an arbitrary cell and for every law at once, reduced to the measurability of the variational quantity.