High-contrast homogenization: Analytic.DoubledMinimizerReadouts

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

Readouts of the doubled variational minimizer

A readout of the doubled minimizer of a cell is a real-valued functional of the minimizing field which may itself depend on the coefficient field, the leading example being the energy pairing against a fixed test state. This file records the general transfer principle: a readout that is continuous in the field for every sample and measurable in the sample on every fixed generator competitor is measurable in the sample when evaluated at the minimizer.

The proof is the Galerkin selection again. The selected competitors are countably valued measurable functions of the sample converging to the minimizer, so continuity of the readout in its field argument turns them into a sequence of measurable real functions converging pointwise to the readout of the minimizer.

Two consequences are recorded: the pairing of the minimizer with a fixed L² test field, and the doubled energy pairing of the minimizer with a fixed test state — that is, the localized average of the coefficient-operator image of the minimizer.

theorem HCPolySupport.HighContrast.Selection.measurable_readout_cellMuMinimizer {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) {F : Om → ↥(HilbertBlockL2 U) → ℝ} (hFcont : ∀ (w : Om), Continuous (F w)) (hFmeas : ∀ (Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)), Measurable fun (w : Om) => F w (cellMuCandidate P0 Y)) : Measurable fun (w : Om) => F w ((cellMuHilbert hvol (sliceOf hSlice w)).minimizerMap P0)

Transfer principle for readouts of the doubled minimizer. A readout continuous in the field argument and measurable in the sample on every fixed generator competitor is measurable in the sample at the minimizer.

theorem HCPolySupport.HighContrast.Selection.measurable_inner_cellMuMinimizer {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) (y : ↥(HilbertBlockL2 U)) : Measurable fun (w : Om) => inner ℝ y ((cellMuHilbert hvol (sliceOf hSlice w)).minimizerMap P0)

The pairing of the doubled minimizer with a fixed L² test field is a measurable function of the sample.

The doubled energy pairing against a fixed test state

theorem HCPolySupport.HighContrast.Selection.measurable_blockPairingAverage_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 ≠ ⊤) {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)) (X Y : BlockState d) (hX : MemBlockL2 U X.eval) (hY : MemBlockL2 U Y.eval) : Measurable fun (w : Om) => blockPairingAverage U (A w).toFun X Y

The doubled block pairing average against a fixed pair of L² block states is measurable in the sample.

theorem HCPolySupport.HighContrast.Selection.energyBilin_cellMuCandidate_eq_blockPairingAverage {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hvol : 0 < (MeasureTheory.volume U).toReal) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P0 : BlockVec d) {Y : BlockState d} (hY : MemBlockL2 U Y.eval) (Z : ↥(canonicalMuBlockCorrectionGeneratorSubmodule U)) : ((cellMuHilbert hvol a).energyBilin (toHilbertBlockL2OfBlockField hY)) (cellMuCandidate P0 Z) = blockPairingAverage U (↑a) (canonicalMuGeneratorAffineField P0 Z) Y

The doubled energy pairing of a fixed test state against a generator competitor is a block pairing average.

theorem HCPolySupport.HighContrast.Selection.measurable_energyBilin_cellMuMinimizer {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) {Y : BlockState d} (hY : MemBlockL2 U Y.eval) : Measurable fun (w : Om) => ((cellMuHilbert hvol (sliceOf hSlice w)).energyBilin (toHilbertBlockL2OfBlockField hY)) ((cellMuHilbert hvol (sliceOf hSlice w)).minimizerMap P0)

The doubled energy pairing of a fixed test state against the minimizer is a measurable function of the sample. This is the localized average of the coefficient-operator image of the minimizer.