High-contrast homogenization: Analytic.OptimizerStateL2

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

The doubled optimizer state as an ambient L² field

The doubled state of the response optimizer is square integrable on its cell: the gradient because the optimizer is a Sobolev function, the flux because the coefficient object is essentially bounded. This file realizes it as an element of the ambient block L² space and shows that this element is a strongly measurable function of the sample.

Measurability is obtained from the weighted coordinate readouts already available: the ambient inner product against a fixed block test state is a finite sum of such readouts, every ambient element is the image of a block state, and a map into a separable Hilbert space is measurable once its inner products against a dense family are. Localized quadratic observables of the optimizer state then become continuous functionals of a measurable field.

Doubled pairing as a coordinate sum

theorem HCPolySupport.HighContrast.Selection.blockVecDot_eq_sum_toFullBlockVec {d : ℕ} (X Y : BlockVec d) : blockVecDot X Y = ∑ alpha : BlockCoord d, toFullBlockVec X alpha * toFullBlockVec Y alpha

Every ambient block field comes from a block state

theorem HCPolySupport.HighContrast.Selection.exists_blockState_toHilbertBlockL2 {d : ℕ} {U : Set (Vec d)} (f : ↥(HilbertBlockL2 U)) : ∃ (Y : BlockState d) (hY : MemBlockL2 U Y.eval), toHilbertBlockL2OfBlockField hY = f

Every element of the ambient block L² space is the image of a block state.

The optimizer state is square integrable

theorem HCPolySupport.HighContrast.Selection.memBlockL2_optimizerBlockState {d : ℕ} {U : Book.Ch02.Domain d} (aU : Book.Ch02.CoeffOn U) (p q : Vec d) : MemBlockL2 U.carrier (optimizerBlockState U aU p q)

noncomputable def HCPolySupport.HighContrast.Selection.optimizerStateL2 {d : ℕ} (U : Book.Ch02.Domain d) (aU : Book.Ch02.CoeffOn U) (p q : Vec d) : ↥(HilbertBlockL2 U.carrier)

The doubled optimizer state as an element of the ambient block L² space.

Equations

• HCPolySupport.HighContrast.Selection.optimizerStateL2 U aU p q = HCPolySupport.toHilbertBlockL2OfBlockField ⋯

theorem HCPolySupport.HighContrast.Selection.coeFn_optimizerStateL2 {d : ℕ} (U : Book.Ch02.Domain d) (aU : Book.Ch02.CoeffOn U) (p q : Vec d) : ↑↑(optimizerStateL2 U aU p q) =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => HilbertBlockVec.ofBlockVec (optimizerBlockState U aU p q x)

The inner product against a fixed block state

theorem HCPolySupport.HighContrast.Selection.inner_optimizerStateL2 {d : ℕ} {U : Book.Ch02.Domain d} (aU : Book.Ch02.CoeffOn U) (p q : Vec d) {Y : BlockState d} (hY : MemBlockL2 U.carrier Y.eval) : inner ℝ (toHilbertBlockL2OfBlockField hY) (optimizerStateL2 U aU p q) = ∑ alpha : BlockCoord d, ∫ (x : Vec d) in U.carrier, toFullBlockVec (Y.eval x) alpha * toFullBlockVec (optimizerBlockState U aU p q x) alpha

Strong measurability of the ambient optimizer state

theorem HCPolySupport.HighContrast.Selection.stronglyMeasurable_optimizerStateL2 {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) : MeasureTheory.StronglyMeasurable fun (w : Om) => optimizerStateL2 U (aU w) p q

The ambient doubled optimizer state is a strongly measurable function of the sample, on one quantitative ellipticity slice of the cell.