High-contrast homogenization: Provider.Response.OptimizerReadoutMeasurability

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

Sample measurability of the weighted optimizer state readouts

The sigma-field of the coefficient space is the global one generated by the smooth linear statistics. This file carries the weighted coordinate readouts of the doubled response optimizer state to that sigma-field, on every bounded open cell of positive volume.

The route is the one the coarse-grained energy already uses. A field of the coefficient space is represented, up to a null set, by a field of the exact coarse source, and the representative map is measurable; the readout only sees the almost everywhere class of the field, so the value is unchanged. Every coarse-source field is almost everywhere uniformly elliptic on the cell, so it carries a coefficient object there, and it lies in one of the countably many quantitative ellipticity slices; the slice events are measurable, and on each slice the readout is measurable by the Galerkin selection. Gluing the slices and composing with the representative map gives the statement on the coefficient space.

The readout as a function of the coefficient object

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

The weighted coordinate readout of the doubled optimizer state.

Equations

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

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

The readout only sees the almost everywhere class of the coefficient field. Two coefficient objects that agree almost everywhere on the cell have response optimizers with the same gradient almost everywhere, hence the same doubled state almost everywhere and the same weighted readouts.

The coefficient object carried by a coarse-source field

theorem HCPolySupport.HighContrast.Selection.exists_srcAEE {d : ℕ} (U : Book.Ch02.Domain d) (hUbdd : IsBoundedDomain U.carrier) (b : Source.Coarse.Carrier d) : ∃ (eps : ℝ), 0 < eps ∧ IsAEEllipticFieldOn eps eps⁻¹ U.carrier ↑b

Every coarse-source field is almost everywhere uniformly elliptic on a bounded cell, with reciprocal constants.

noncomputable def HCPolySupport.HighContrast.Selection.srcLam {d : ℕ} (U : Book.Ch02.Domain d) (hUbdd : IsBoundedDomain U.carrier) (b : Source.Coarse.Carrier d) : ℝ

The normalized lower ellipticity constant of a coarse-source field on the cell: at most one, so its reciprocal is an upper constant.

Equations

• HCPolySupport.HighContrast.Selection.srcLam U hUbdd b = min ⋯.choose 1

theorem HCPolySupport.HighContrast.Selection.srcLam_pos {d : ℕ} (U : Book.Ch02.Domain d) (hUbdd : IsBoundedDomain U.carrier) (b : Source.Coarse.Carrier d) : 0 < srcLam U hUbdd b

theorem HCPolySupport.HighContrast.Selection.srcLam_le_inv {d : ℕ} (U : Book.Ch02.Domain d) (hUbdd : IsBoundedDomain U.carrier) (b : Source.Coarse.Carrier d) : srcLam U hUbdd b ≤ (srcLam U hUbdd b)⁻¹

theorem HCPolySupport.HighContrast.Selection.srcLam_isAEElliptic {d : ℕ} (U : Book.Ch02.Domain d) (hUbdd : IsBoundedDomain U.carrier) (b : Source.Coarse.Carrier d) : IsAEEllipticFieldOn (srcLam U hUbdd b) (srcLam U hUbdd b)⁻¹ U.carrier ↑b

noncomputable def HCPolySupport.HighContrast.Selection.sourceCoeffOn {d : ℕ} (U : Book.Ch02.Domain d) (hUbdd : IsBoundedDomain U.carrier) (b : Source.Coarse.Carrier d) : Book.Ch02.CoeffOn U

A coarse-source field, viewed as a coefficient object on a bounded open cell.

Equations

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

noncomputable def HCPolySupport.HighContrast.Selection.sourceOptimizerStateReadout {d : ℕ} (U : Book.Ch02.Domain d) (hUbdd : IsBoundedDomain U.carrier) (p q : Vec d) (alpha : BlockCoord d) (eta : Vec d → ℝ) (b : Source.Coarse.Carrier d) : ℝ

The weighted coordinate readout of a coarse-source field.

Equations

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

Measurability on the exact coarse source

theorem HCPolySupport.HighContrast.Selection.measurable_sourceOptimizerStateReadout_local {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) (alpha : BlockCoord d) {eta : Vec d → ℝ} (heta : MemScalarL2 U.carrier eta) : Measurable (sourceOptimizerStateReadout U hUbdd p q alpha eta)

The readout is measurable on the exact coarse source, for the source's own sigma-field of the cell.

theorem HCPolySupport.HighContrast.Selection.measurable_sourceOptimizerStateReadout {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) (alpha : BlockCoord d) {eta : Vec d → ℝ} (heta : MemScalarL2 U.carrier eta) : Measurable (sourceOptimizerStateReadout U hUbdd p q alpha eta)

The readout is measurable on the exact coarse source for its global sigma-field.

Measurability on the coefficient space

theorem HCPolySupport.HighContrast.Selection.measurable_optimizerStateReadout_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) (alpha : BlockCoord d) {eta : Vec d → ℝ} (heta : MemScalarL2 U.carrier eta) : Measurable fun (a : CoeffSpace d) => optimizerStateReadout U (a.coeffOn U) p q alpha eta

The weighted coordinate readout of the doubled optimizer state is measurable on the coefficient space, for the global sigma-field generated by the smooth linear statistics, on every bounded open cell of positive volume.