High-contrast homogenization: Provider.Response.OptimizerEnergyMeasurability

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

Sample measurability of localized optimizer energies

A localized energy of the response optimizer is the average of a bounded weight against the quadratic form of the coefficient field on the optimizer gradient. It is a continuous quadratic functional of the ambient doubled optimizer state, hence a measurable function of the sample.

The passage from one quantitative ellipticity slice of the cell to the whole coefficient space is isolated here as a reusable rule: a real observable of the coefficient object that sees only its almost everywhere class and is measurable on each slice is measurable on the coefficient space.

From the ellipticity slices to the coefficient space

theorem HCPolySupport.HighContrast.Selection.measurable_coeffSpace_of_slicewise {d : ℕ} {U : Book.Ch02.Domain d} (hUopen : IsOpen U.carrier) (hUbdd : IsBoundedDomain U.carrier) (R : Book.Ch02.CoeffOn U → ℝ) (hcongr : ∀ (aU bU : Book.Ch02.CoeffOn U), aU.AEEq bU → R aU = R bU) (hslice : ∀ (k : ℕ) (Om : Type) (mOm : MeasurableSpace Om) (A : Om → RegCoeffField d), (∀ (w : Om), AEEQuantitativeEllipticSlice U.carrier k (A w).toFun) → (∀ (i j : Fin d) {φ : Vec d → ℝ}, ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U.carrier → Measurable fun (w : Om) => entryTestR i j φ (A w)) → ∀ (aU : Om → Book.Ch02.CoeffOn U), (∀ (w : Om), (aU w).toCoeffField = (A w).toFun) → Measurable fun (w : Om) => R (aU w)) : Measurable fun (a : CoeffSpace d) => R (a.coeffOn U)

The slice-gluing rule. An observable of the coefficient object that depends only on its almost everywhere class and is measurable over every parameter family lying in a single quantitative ellipticity slice is measurable on the coefficient space.

Bounded weights against square integrable functions

theorem HCPolySupport.HighContrast.Selection.memScalarL2_bounded_mul {d : ℕ} {U : Set (Vec d)} {eta w : Vec d → ℝ} (hmeas : Measurable eta) {C : ℝ} (hbound : ∀ (x : Vec d), |eta x| ≤ C) (hw : MemScalarL2 U w) : MemScalarL2 U fun (x : Vec d) => eta x * w x

The localized optimizer energy

theorem HCPolySupport.HighContrast.Selection.optimizerBlockState_fst {d : ℕ} (U : Book.Ch02.Domain d) (aU : Book.Ch02.CoeffOn U) (p q x : Vec d) : (optimizerBlockState U aU p q x).1 = (Book.Ch02.canonicalMaximizer ⋯ p q).toSolution.toH1.grad x

theorem HCPolySupport.HighContrast.Selection.optimizerBlockState_snd {d : ℕ} (U : Book.Ch02.Domain d) (aU : Book.Ch02.CoeffOn U) (p q x : Vec d) : (optimizerBlockState U aU p q x).2 = matVecMul (aU.toCoeffField x) (optimizerBlockState U aU p q x).1

noncomputable def HCPolySupport.HighContrast.Selection.weightedOptimizerEnergy {d : ℕ} (U : Book.Ch02.Domain d) (aU : Book.Ch02.CoeffOn U) (p q : Vec d) (eta : Vec d → ℝ) : ℝ

The localized weighted energy of the response optimizer on its cell.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Selection.weightedOptimizerEnergy_eq {d : ℕ} {U : Book.Ch02.Domain d} (aU : Book.Ch02.CoeffOn U) (p q : Vec d) {eta : Vec d → ℝ} (hmeas : Measurable eta) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (x : Vec d), |eta x| ≤ C) : weightedOptimizerEnergy U aU p q eta = (MeasureTheory.volume U.carrier).toReal⁻¹ * (1 / 2 * ∑ i : Fin d, inner ℝ ((weightedCoordOperator hmeas hC hbound (Sum.inl i) (Sum.inr i)) (optimizerStateL2 U aU p q)) (optimizerStateL2 U aU p q))

The localized optimizer energy is a continuous quadratic functional of the ambient optimizer state.

Measurability of the localized optimizer energy

theorem HCPolySupport.HighContrast.Selection.continuous_weightedEnergyFunctional {d : ℕ} {U : Set (Vec d)} {eta : Vec d → ℝ} (hmeas : Measurable eta) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (x : Vec d), |eta x| ≤ C) : Continuous fun (z : ↥(HilbertBlockL2 U)) => (MeasureTheory.volume U).toReal⁻¹ * (1 / 2 * ∑ i : Fin d, inner ℝ ((weightedCoordOperator hmeas hC hbound (Sum.inl i) (Sum.inr i)) z) z)

The weighted quadratic functional of the ambient state is continuous.

theorem HCPolySupport.HighContrast.Selection.measurable_weightedOptimizerEnergy_slice {d : ℕ} {Om : Type u_1} [mOm : MeasurableSpace Om] {U : Book.Ch02.Domain d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U.carrier)] {k : ℕ} (hUopen : IsOpen U.carrier) (hUfin : MeasureTheory.volume U.carrier ≠ ⊤) (hvol : 0 < (MeasureTheory.volume U.carrier).toReal) {A : Om → RegCoeffField d} (hSlice : ∀ (w : Om), AEEQuantitativeEllipticSlice U.carrier k (A w).toFun) (hEntry : ∀ (i j : Fin d) {φ : Vec d → ℝ}, ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U.carrier → Measurable fun (w : Om) => entryTestR i j φ (A w)) (aU : Om → Book.Ch02.CoeffOn U) (haU : ∀ (w : Om), (aU w).toCoeffField = (A w).toFun) (p q : Vec d) {eta : Vec d → ℝ} (hmeas : Measurable eta) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (x : Vec d), |eta x| ≤ C) : Measurable fun (w : Om) => weightedOptimizerEnergy U (aU w) p q eta

The localized optimizer energy is measurable on one ellipticity slice.

theorem HCPolySupport.HighContrast.Selection.weightedOptimizerEnergy_congr {d : ℕ} {U : Book.Ch02.Domain d} {aU bU : Book.Ch02.CoeffOn U} (h : aU.AEEq bU) (p q : Vec d) (eta : Vec d → ℝ) : weightedOptimizerEnergy U aU p q eta = weightedOptimizerEnergy U bU p q eta

The localized optimizer energy sees only the almost everywhere class of the coefficient field.

theorem HCPolySupport.HighContrast.Selection.measurable_weightedOptimizerEnergy_coeffSpace {d : ℕ} {U : Book.Ch02.Domain d} (hUopen : IsOpen U.carrier) (hUbdd : IsBoundedDomain U.carrier) (hvol : 0 < (MeasureTheory.volume U.carrier).toReal) (p q : Vec d) {eta : Vec d → ℝ} (hmeas : Measurable eta) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (x : Vec d), |eta x| ≤ C) : Measurable fun (a : CoeffSpace d) => weightedOptimizerEnergy U (a.coeffOn U) p q eta

The localized optimizer energy is measurable on the coefficient space.

The response functional is a localized optimizer energy

theorem HCPolySupport.HighContrast.Selection.responseJ_eq_weightedOptimizerEnergy {d : ℕ} (U : Book.Ch02.Domain d) (aU : Book.Ch02.CoeffOn U) (p q : Vec d) : Book.Ch02.responseJ U aU p q = weightedOptimizerEnergy U aU p q fun (x : Vec d) => 1

The response functional is the optimizer energy at unit weight.

theorem HCPolySupport.HighContrast.Selection.measurable_responseJ_coeffSpace {d : ℕ} {U : Book.Ch02.Domain d} (hUopen : IsOpen U.carrier) (hUbdd : IsBoundedDomain U.carrier) (hvol : 0 < (MeasureTheory.volume U.carrier).toReal) (p q : Vec d) : Measurable fun (a : CoeffSpace d) => Book.Ch02.responseJ U (a.coeffOn U) p q

The response functional is measurable on the coefficient space.