High-contrast homogenization: Provider.Response.LocalizedOptimizerObservables

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

Localized observables of the doubled optimizer state

The weak-norm estimates for the optimizer state read the doubled optimizer state of a parent cell through localized averages: an average of one doubled coordinate over an aligned child cell, and a localized oscillation average against the pre-Young cutoff. Both are weighted coordinate readouts of the optimizer state of the parent cell, with a weight supported in the child cell, so both are measurable functions of the sample.

The constant skew shift of the coefficient field acts on the coefficient space by translating each generating linear statistic by a constant, so it is measurable and the observables of the shifted sample are measurable as well.

The constant skew shift is measurable

theorem HCPolySupport.HighContrast.Selection.coeffPairing_subSkew {d : ℕ} (e e' : Vec d) {V : Set (Vec d)} {φ : Vec d → ℝ} (hφ : IsLocalTest V φ) (g : Mat d) (hg : IsSkewMat g) (a : CoeffSpace d) : coeffPairing e e' φ (a.subSkew g hg) = coeffPairing e e' φ a - vecDot e' (matVecMul g e) * ∫ (x : Vec d), φ x

A generating linear statistic of a constant skew shift is the statistic of the sample, translated by a constant.

theorem HCPolySupport.HighContrast.Selection.measurable_subSkew {d : ℕ} (g : Mat d) (hg : IsSkewMat g) : Measurable fun (a : CoeffSpace d) => a.subSkew g hg

The constant skew shift is measurable on the coefficient space: it pulls each generating linear statistic back to a translate of itself.

The adjoint sample is measurable

theorem HCPolySupport.HighContrast.Selection.coeffPairing_transpose {d : ℕ} (e e' : Vec d) (φ : Vec d → ℝ) (a : CoeffSpace d) : coeffPairing e e' φ a.transpose = coeffPairing e' e φ a

A generating linear statistic of the adjoint sample is the statistic of the sample with its two directions exchanged.

theorem HCPolySupport.HighContrast.Selection.measurable_transpose {d : ℕ} : Measurable CoeffSpace.transpose

The adjoint sample is measurable on the coefficient space: transposition exchanges the two direction vectors of each generating linear statistic.

Square integrability of a bounded localized weight

theorem HCPolySupport.HighContrast.Selection.memScalarL2_indicator_of_bounded {d : ℕ} {U V : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hV : MeasurableSet V) {w : Vec d → ℝ} (hw : Continuous w) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (x : Vec d), |w x| ≤ C) : MemScalarL2 U (V.indicator w)

A bounded continuous weight, restricted to a measurable subset and extended by zero, is square integrable on a cell of finite measure.

theorem HCPolySupport.HighContrast.Selection.memScalarL2_indicator_cutoffOscillation {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) {U V : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hV : MeasurableSet V) : MemScalarL2 U (V.indicator fun (x : Vec d) => Response.adaptedPreYoungCutoff q hq t x - volumeAverage V (Response.adaptedPreYoungCutoff q hq t))

The localized oscillation of the pre-Young cutoff is square integrable on the parent cell.

Localized weighted averages of the optimizer state

theorem HCPolySupport.HighContrast.Selection.setIntegral_indicator_mul {d : ℕ} {V U : Set (Vec d)} (hV : MeasurableSet V) (hVU : V ⊆ U) (w F : Vec d → ℝ) : ∫ (x : Vec d) in U, V.indicator w x * F x = ∫ (x : Vec d) in V, w x * F x

Restricting a weighted integral to a subset is testing against the extension of the weight by zero.

theorem HCPolySupport.HighContrast.Selection.volumeAverage_weighted_optimizerBlockState {d : ℕ} {U : Book.Ch02.Domain d} (aU : Book.Ch02.CoeffOn U) (p q : Vec d) (alpha : BlockCoord d) {V : Set (Vec d)} (hV : MeasurableSet V) (hVU : V ⊆ U.carrier) (w : Vec d → ℝ) : (volumeAverage V fun (x : Vec d) => w x * toFullBlockVec (optimizerBlockState U aU p q x) alpha) = (MeasureTheory.volume V).toReal⁻¹ * optimizerStateReadout U aU p q alpha (V.indicator w)

A localized weighted average of one doubled coordinate of the optimizer state is a weighted coordinate readout on the whole cell.

theorem HCPolySupport.HighContrast.Selection.measurable_volumeAverage_weighted_optimizerBlockState_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) {V : Set (Vec d)} (hV : MeasurableSet V) (hVU : V ⊆ U.carrier) {w : Vec d → ℝ} (hw : MemScalarL2 U.carrier (V.indicator w)) : Measurable fun (a : CoeffSpace d) => volumeAverage V fun (x : Vec d) => w x * toFullBlockVec (optimizerBlockState U (a.coeffOn U) p q x) alpha

A localized weighted average of one doubled coordinate of the optimizer state is measurable on the coefficient space.

The observables of the diagonal weak estimate

theorem HCPolySupport.HighContrast.Selection.diagonalWeakState_eq_optimizerBlockState {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : Response.diagonalWeakState hq t a p r = optimizerBlockState (Response.adaptedDomain hq t) (a.coeffOn (Response.adaptedDomain hq t)) p r

The doubled optimizer state of the diagonal weak estimate is the doubled optimizer state of its adapted parent cell.

theorem HCPolySupport.HighContrast.Selection.toFullBlockVec_blockCellAverage {d : ℕ} (V : Set (Vec d)) (F : Vec d → BlockVec d) (alpha : BlockCoord d) : toFullBlockVec (Response.blockCellAverage V F) alpha = volumeAverage V fun (x : Vec d) => toFullBlockVec (F x) alpha

One doubled coordinate of a block cell average is the localized average of that coordinate.

theorem HCPolySupport.HighContrast.Selection.measurable_volumeAverage_weighted_diagonalWeakState_subSkew {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) (alpha : BlockCoord d) {V : Set (Vec d)} (hV : MeasurableSet V) (hVU : V ⊆ adaptedCell q t) {w : Vec d → ℝ} (hw : MemScalarL2 (adaptedCell q t) (V.indicator w)) : Measurable fun (a : CoeffSpace d) => volumeAverage V fun (x : Vec d) => w x * toFullBlockVec (Response.diagonalWeakState hq t (a.subSkew g hg) p r x) alpha

The localized oscillation readout of the terminal optimizer state on an aligned child cell is measurable, for the sample sigma-field of the coefficient space.

theorem HCPolySupport.HighContrast.Selection.measurable_toFullBlockVec_blockCellAverage_diagonalWeakState_subSkew {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) (alpha : BlockCoord d) {V : Set (Vec d)} (hV : MeasurableSet V) (hVU : V ⊆ adaptedCell q t) (hVfin : MeasureTheory.volume V ≠ ⊤) : Measurable fun (a : CoeffSpace d) => toFullBlockVec (Response.blockCellAverage V (Response.diagonalWeakState hq t (a.subSkew g hg) p r)) alpha

The block cell average of the terminal optimizer state on an aligned child cell is measurable, in every doubled coordinate.

The observables on an aligned child cell

theorem HCPolySupport.HighContrast.Selection.aestronglyMeasurable_blockCellAverage_diagonalWeakState_subSkew_alignedIndex {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) (P : MeasureTheory.Measure (CoeffSpace d)) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) {w : Fin d → ℤ} (hw : w ∈ Response.alignedIndex q s t) (alpha : BlockCoord d) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockVec (Response.blockCellAverage (adaptedCellAt q s w) (Response.diagonalWeakState hq t (a.subSkew g hg) p r)) alpha) P

The measurability half of the per-child block-average observable of the cutoff split.

theorem HCPolySupport.HighContrast.Selection.aestronglyMeasurable_volumeAverage_weighted_diagonalWeakState_subSkew_alignedIndex {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) (P : MeasureTheory.Measure (CoeffSpace d)) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) {w : Fin d → ℤ} (hw : w ∈ Response.alignedIndex q s t) (alpha : BlockCoord d) {eta : Vec d → ℝ} (heta : MemScalarL2 (adaptedCell q t) ((adaptedCellAt q s w).indicator eta)) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => eta x * toFullBlockVec (Response.diagonalWeakState hq t (a.subSkew g hg) p r x) alpha) P

The measurability half of the localized cutoff-oscillation observable of the cutoff split. The weight is the oscillation of any fixed profile on the child cell, extended by zero.

theorem HCPolySupport.HighContrast.Selection.aestronglyMeasurable_alignedCellAverage_diagonalAdjointState {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) (P : MeasureTheory.Measure (CoeffSpace d)) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) {w : Fin d → ℤ} (hw : w ∈ Response.alignedIndex q s t) (alpha : BlockCoord d) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockVec (Response.blockCellAverage (adaptedCellAt q s w) (Response.diagonalWeakAdjointState hq t (a.subSkew g hg) p r)) alpha) P

The adjoint block cell average of the terminal optimizer state on an aligned child cell is measurable.

theorem HCPolySupport.HighContrast.Selection.aestronglyMeasurable_weightedCellAverage_diagonalAdjointState {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) (P : MeasureTheory.Measure (CoeffSpace d)) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) {w : Fin d → ℤ} (hw : w ∈ Response.alignedIndex q s t) (alpha : BlockCoord d) {eta : Vec d → ℝ} (heta : MemScalarL2 (adaptedCell q t) ((adaptedCellAt q s w).indicator eta)) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => eta x * toFullBlockVec (Response.diagonalWeakAdjointState hq t (a.subSkew g hg) p r x) alpha) P

The adjoint localized oscillation readout of the terminal optimizer state on an aligned child cell is measurable.