High-contrast homogenization: Analytic.OptimizerGradientReadout

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

Weighted readouts of the response optimizer state

The response optimizer of the variational coarse block of s.introduction is a chosen maximizer of a variational problem whose admissible class is the a-harmonic functions of the domain, a class that moves with the coefficient field. Its gradient and flux are nevertheless recovered from the minimizer of the doubled variational problem, whose admissible class is fixed: the gradient is the sum of the potential component of the doubled minimizer and the lower component of its coefficient-operator image, and the flux is the sum of the flux component and the upper component of that image.

This file turns that recovery into a formula for the weighted coordinate readouts of the doubled optimizer state. For a fixed square-integrable weight and a fixed doubled coordinate, the weighted integral of the corresponding component of the optimizer state over the domain is the sum of an ambient inner product of the doubled minimizer against a fixed test state and a fixed multiple of the doubled energy pairing of the minimizer against the swapped test state. Both are readouts of the doubled minimizer of the kind the selection theorem makes measurable.

The ambient inner product of two block fields

theorem HCPolySupport.HighContrast.Selection.inner_toHilbertBlockL2OfBlockField_eq_integral {d : ℕ} {U : Set (Vec d)} {F G : Vec d → BlockVec d} (hF : MemBlockL2 U F) (hG : MemBlockL2 U G) : inner ℝ (toHilbertBlockL2OfBlockField hF) (toHilbertBlockL2OfBlockField hG) = ∫ (x : Vec d) in U, blockVecDot (F x) (G x)

The ambient inner product of two block L² fields is the integral of their pointwise doubled pairing.

The fixed test states of a weighted coordinate readout

def HCPolySupport.HighContrast.Selection.gradTestState {d : ℕ} (eta : Vec d → ℝ) (i : Fin d) : BlockState d

The test state pairing a weight against the potential component.

Equations

• HCPolySupport.HighContrast.Selection.gradTestState eta i = { potential := fun (x : HCPolySupport.Vec d) => eta x • HCPolySupport.basisVec i, flux := fun (x : HCPolySupport.Vec d) => 0 }

def HCPolySupport.HighContrast.Selection.fluxTestState {d : ℕ} (eta : Vec d → ℝ) (i : Fin d) : BlockState d

The test state pairing a weight against the flux component.

Equations

• HCPolySupport.HighContrast.Selection.fluxTestState eta i = { potential := fun (x : HCPolySupport.Vec d) => 0, flux := fun (x : HCPolySupport.Vec d) => eta x • HCPolySupport.basisVec i }

theorem HCPolySupport.HighContrast.Selection.memVectorL2_smul_basisVec {d : ℕ} {U : Set (Vec d)} {eta : Vec d → ℝ} (heta : MemScalarL2 U eta) (i : Fin d) : MemVectorL2 U fun (x : Vec d) => eta x • basisVec i

theorem HCPolySupport.HighContrast.Selection.gradTestState_memBlockL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {eta : Vec d → ℝ} (heta : MemScalarL2 U eta) (i : Fin d) : MemBlockL2 U (gradTestState eta i).eval

theorem HCPolySupport.HighContrast.Selection.fluxTestState_memBlockL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {eta : Vec d → ℝ} (heta : MemScalarL2 U eta) (i : Fin d) : MemBlockL2 U (fluxTestState eta i).eval

theorem HCPolySupport.HighContrast.Selection.blockVecDot_gradTestState {d : ℕ} (eta : Vec d → ℝ) (i : Fin d) (Z : BlockVec d) (x : Vec d) : blockVecDot ((gradTestState eta i).eval x) Z = eta x * Z.1 i

theorem HCPolySupport.HighContrast.Selection.blockVecDot_fluxTestState {d : ℕ} (eta : Vec d → ℝ) (i : Fin d) (Z : BlockVec d) (x : Vec d) : blockVecDot ((fluxTestState eta i).eval x) Z = eta x * Z.2 i

def HCPolySupport.HighContrast.Selection.blockTestState {d : ℕ} (eta : Vec d → ℝ) : BlockCoord d → BlockState d

The fixed test state selecting one doubled coordinate against a weight.

Equations

• HCPolySupport.HighContrast.Selection.blockTestState eta (Sum.inl i) = HCPolySupport.HighContrast.Selection.gradTestState eta i
• HCPolySupport.HighContrast.Selection.blockTestState eta (Sum.inr i) = HCPolySupport.HighContrast.Selection.fluxTestState eta i

theorem HCPolySupport.HighContrast.Selection.blockTestState_memBlockL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {eta : Vec d → ℝ} (heta : MemScalarL2 U eta) (alpha : BlockCoord d) : MemBlockL2 U (blockTestState eta alpha).eval

theorem HCPolySupport.HighContrast.Selection.blockVecDot_blockTestState {d : ℕ} (eta : Vec d → ℝ) (alpha : BlockCoord d) (Z : BlockVec d) (x : Vec d) : blockVecDot ((blockTestState eta alpha).eval x) Z = eta x * toFullBlockVec Z alpha

The doubled optimizer state

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

The doubled state of the response optimizer: its gradient paired with its flux.

Equations

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

The doubled minimizer of the paper's domain layer

theorem HCPolySupport.HighContrast.Selection.isBlockMuAdmissible_of_isDoubledMuAdmissible {d : ℕ} {U : Book.Ch02.Domain d} {P0 : BlockVec d} {X : Book.Ch02.DoubledField d} (hX : Book.Ch02.IsDoubledMuAdmissible U P0 X) : IsBlockMuAdmissible U.carrier P0 { potential := X.potential, flux := X.flux }

A doubled admissible field of the paper's domain layer is a block admissible state of the variational layer.

theorem HCPolySupport.HighContrast.Selection.toHilbertBlockL2_eq_minimizerMap_of_isDoubledMuMinimizer {d : ℕ} {U : Book.Ch02.Domain d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U.carrier)] {k : ℕ} (hvol : 0 < (MeasureTheory.volume U.carrier).toReal) {aU : Book.Ch02.CoeffOn U} (hk : AEEQuantitativeEllipticSlice U.carrier k aU.toCoeffField) (P0 : BlockVec d) {X : Book.Ch02.DoubledField d} (hX : Book.Ch02.IsDoubledMuMinimizer U aU P0 X) (hAdm : IsBlockMuAdmissible U.carrier P0 { potential := X.potential, flux := X.flux }) : toHilbertBlockL2OfBlockField ⋯ = (cellMuHilbert hvol ⟨aU.toCoeffField, hk⟩).minimizerMap P0

A pointwise doubled minimizer represents the Hilbert minimizer of the cell's doubled problem.

theorem HCPolySupport.HighContrast.Selection.ae_toFullBlockVec_optimizerBlockState {d : ℕ} {U : Book.Ch02.Domain d} {aU : Book.Ch02.CoeffOn U} (p q : Vec d) (alpha : BlockCoord d) {X : Book.Ch02.DoubledField d} (hX : Book.Ch02.IsDoubledMuMinimizer U aU (-p, q) X) : (fun (x : Vec d) => toFullBlockVec (optimizerBlockState U aU p q x) alpha) =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => toFullBlockVec (X.eval x) alpha + toFullBlockVec (blockMatVecMul (blockCoeffField aU.toCoeffField x) (X.eval x)) (Sum.swap alpha)

The doubled optimizer state is recovered from a doubled minimizer: in every doubled coordinate it is the corresponding component of the minimizer plus the swapped component of its coefficient-operator image.

Integrability of the doubled pairing integrand

theorem HCPolySupport.HighContrast.Selection.integrableOn_blockPairingIntegrand_of_slice {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {k : ℕ} {a : CoeffField d} (hSlice : AEEQuantitativeEllipticSlice U k a) {X Y : BlockState d} (hX : MemBlockL2 U X.eval) (hY : MemBlockL2 U Y.eval) : MeasureTheory.IntegrableOn (blockPairingIntegrand a X Y) U MeasureTheory.volume

The doubled pairing integrand of two block L² states is integrable on a quantitative ellipticity slice of the cell.

The weighted coordinate readout

theorem HCPolySupport.HighContrast.Selection.integral_weighted_optimizerBlockState {d : ℕ} {U : Book.Ch02.Domain d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U.carrier)] {k : ℕ} (hvol : 0 < (MeasureTheory.volume U.carrier).toReal) {aU : Book.Ch02.CoeffOn U} (hk : AEEQuantitativeEllipticSlice U.carrier k aU.toCoeffField) (p q : Vec d) (alpha : BlockCoord d) {eta : Vec d → ℝ} (heta : MemScalarL2 U.carrier eta) : ∫ (x : Vec d) in U.carrier, eta x * toFullBlockVec (optimizerBlockState U aU p q x) alpha = inner ℝ (toHilbertBlockL2OfBlockField ⋯) ((cellMuHilbert hvol ⟨aU.toCoeffField, hk⟩).minimizerMap (-p, q)) + (MeasureTheory.volume U.carrier).toReal * ((cellMuHilbert hvol ⟨aU.toCoeffField, hk⟩).energyBilin (toHilbertBlockL2OfBlockField ⋯)) ((cellMuHilbert hvol ⟨aU.toCoeffField, hk⟩).minimizerMap (-p, q))

The weighted coordinate readout of the doubled optimizer state is a readout of the doubled minimizer. The weight and the coordinate enter only through two fixed test states, and the coefficient field only through the doubled problem.

Measurability of the weighted coordinate readout

theorem HCPolySupport.HighContrast.Selection.measurable_integral_weighted_optimizerBlockState {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) (alpha : BlockCoord d) {eta : Vec d → ℝ} (heta : MemScalarL2 U.carrier eta) : Measurable fun (w : Om) => ∫ (x : Vec d) in U.carrier, eta x * toFullBlockVec (optimizerBlockState U (aU w) p q x) alpha

The weighted coordinate readout of the doubled optimizer state is a measurable function of the sample, on one quantitative ellipticity slice of the cell and for any parameter space whose localized smooth entry tests are measurable.