High-contrast homogenization: Provider.Response.RecentDifferenceEnergyMeasurability

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

Sample measurability of the per-cell recent difference energies

The recent difference energy of the weak-norm estimate for the optimizer state is the doubled energy, on an aligned child cell, of the difference between the child optimizer state and the terminal optimizer state of the parent cell. Both states are aligned pairs of a gradient and its own flux, so their difference is aligned too and the doubled operator sends it to its own swap; the energy is therefore the plain coordinate pairing of the two halves of the difference, with no coefficient field left in the weight.

That pairing is a continuous quadratic functional of the ambient difference field, and the difference field is a strongly measurable function of the sample because each of its inner products against a fixed block state splits into a child readout and a parent readout localized to the child cell.

Restriction to a subcell

theorem HCPolySupport.HighContrast.Selection.memScalarL2_indicator_subset {d : ℕ} {V W : Set (Vec d)} (hV : MeasurableSet V) (hVW : V ⊆ W) {f : Vec d → ℝ} (hf : MemScalarL2 V f) : MemScalarL2 W (V.indicator f)

theorem HCPolySupport.HighContrast.Selection.memBlockL2_subset {d : ℕ} {V W : Set (Vec d)} (hV : MeasurableSet V) (hVW : V ⊆ W) {F : Vec d → BlockVec d} (hF : MemBlockL2 W F) : MemBlockL2 V F

theorem HCPolySupport.HighContrast.Selection.aeeQuantitativeEllipticSlice_subset {d : ℕ} {V W : Set (Vec d)} (hV : MeasurableSet V) (hVW : V ⊆ W) {k : ℕ} {a : CoeffField d} (h : AEEQuantitativeEllipticSlice W k a) : AEEQuantitativeEllipticSlice V k a

A quantitative ellipticity slice of a cell is one of every measurable subcell.

def HCPolySupport.HighContrast.Selection.restrictCoeffOn {d : ℕ} {V W : Book.Ch02.Domain d} (hV : MeasurableSet V.carrier) (hVW : V.carrier ⊆ W.carrier) (aW : Book.Ch02.CoeffOn W) : Book.Ch02.CoeffOn V

A coefficient object restricts to every measurable subcell.

Equations

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

The difference of two optimizer states on the subcell

noncomputable def HCPolySupport.HighContrast.Selection.optimizerDifferenceState {d : ℕ} (V W : Book.Ch02.Domain d) (aV : Book.Ch02.CoeffOn V) (aW : Book.Ch02.CoeffOn W) (p q : Vec d) : BlockState d

The difference between the optimizer state of a subcell and the optimizer state of the ambient cell.

Equations

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

theorem HCPolySupport.HighContrast.Selection.memBlockL2_optimizerDifferenceState {d : ℕ} {V W : Book.Ch02.Domain d} (hV : MeasurableSet V.carrier) (hVW : V.carrier ⊆ W.carrier) (aV : Book.Ch02.CoeffOn V) (aW : Book.Ch02.CoeffOn W) (p q : Vec d) : MemBlockL2 V.carrier (optimizerDifferenceState V W aV aW p q).eval

noncomputable def HCPolySupport.HighContrast.Selection.optimizerDifferenceL2 {d : ℕ} {V W : Book.Ch02.Domain d} (hV : MeasurableSet V.carrier) (hVW : V.carrier ⊆ W.carrier) (aV : Book.Ch02.CoeffOn V) (aW : Book.Ch02.CoeffOn W) (p q : Vec d) : ↥(HilbertBlockL2 V.carrier)

The ambient realization of the optimizer difference state.

Equations

• HCPolySupport.HighContrast.Selection.optimizerDifferenceL2 hV hVW aV aW p q = HCPolySupport.toHilbertBlockL2OfBlockField ⋯

theorem HCPolySupport.HighContrast.Selection.coeFn_optimizerDifferenceL2 {d : ℕ} {V W : Book.Ch02.Domain d} (hV : MeasurableSet V.carrier) (hVW : V.carrier ⊆ W.carrier) (aV : Book.Ch02.CoeffOn V) (aW : Book.Ch02.CoeffOn W) (p q : Vec d) : ↑↑(optimizerDifferenceL2 hV hVW aV aW p q) =ᵐ[volumeMeasureOn V.carrier] fun (x : Vec d) => HilbertBlockVec.ofBlockVec ((optimizerDifferenceState V W aV aW p q).eval x)

Inner products of the difference against fixed block states

theorem HCPolySupport.HighContrast.Selection.inner_optimizerDifferenceL2 {d : ℕ} {V W : Book.Ch02.Domain d} (hV : MeasurableSet V.carrier) (hVW : V.carrier ⊆ W.carrier) (aV : Book.Ch02.CoeffOn V) (aW : Book.Ch02.CoeffOn W) (p q : Vec d) {Y : BlockState d} (hY : MemBlockL2 V.carrier Y.eval) : inner ℝ (toHilbertBlockL2OfBlockField hY) (optimizerDifferenceL2 hV hVW aV aW p q) = ∑ alpha : BlockCoord d, ((∫ (x : Vec d) in V.carrier, toFullBlockVec (Y.eval x) alpha * toFullBlockVec (optimizerBlockState V aV p q x) alpha) - ∫ (x : Vec d) in W.carrier, V.carrier.indicator (fun (y : Vec d) => toFullBlockVec (Y.eval y) alpha) x * toFullBlockVec (optimizerBlockState W aW p q x) alpha)

Strong measurability of the ambient difference field

theorem HCPolySupport.HighContrast.Selection.stronglyMeasurable_optimizerDifferenceL2 {d : ℕ} {Om : Type u_1} [mOm : MeasurableSpace Om] {V W : Book.Ch02.Domain d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn V.carrier)] [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W.carrier)] {k : ℕ} (hVopen : IsOpen V.carrier) (hVfin : MeasureTheory.volume V.carrier ≠ ⊤) (hVvol : 0 < (MeasureTheory.volume V.carrier).toReal) (hWopen : IsOpen W.carrier) (hWfin : MeasureTheory.volume W.carrier ≠ ⊤) (hWvol : 0 < (MeasureTheory.volume W.carrier).toReal) (hV : MeasurableSet V.carrier) (hVW : V.carrier ⊆ W.carrier) {A : Om → RegCoeffField d} (hSliceW : ∀ (w : Om), AEEQuantitativeEllipticSlice W.carrier k (A w).toFun) (hEntryW : ∀ (i j : Fin d) {φ : Vec d → ℝ}, ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ W.carrier → Measurable fun (w : Om) => entryTestR i j φ (A w)) (aV : Om → Book.Ch02.CoeffOn V) (aW : Om → Book.Ch02.CoeffOn W) (haV : ∀ (w : Om), (aV w).toCoeffField = (A w).toFun) (haW : ∀ (w : Om), (aW w).toCoeffField = (A w).toFun) (p q : Vec d) : MeasureTheory.StronglyMeasurable fun (w : Om) => optimizerDifferenceL2 hV hVW (aV w) (aW w) p q

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

The difference energy is a coordinate pairing

noncomputable def HCPolySupport.HighContrast.Selection.recentDifferenceEnergy {d : ℕ} (V W : Book.Ch02.Domain d) (aV : Book.Ch02.CoeffOn V) (aW : Book.Ch02.CoeffOn W) (p q : Vec d) : ℝ

The recent difference energy of the two optimizer states.

Equations

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

theorem HCPolySupport.HighContrast.Selection.recentDifferenceEnergy_eq {d : ℕ} {V W : Book.Ch02.Domain d} (hV : MeasurableSet V.carrier) (hVW : V.carrier ⊆ W.carrier) (aV : Book.Ch02.CoeffOn V) (aW : Book.Ch02.CoeffOn W) (hfield : aV.toCoeffField = aW.toCoeffField) (p q : Vec d) : recentDifferenceEnergy V W aV aW p q = (MeasureTheory.volume V.carrier).toReal⁻¹ * ∑ i : Fin d, inner ℝ ((weightedCoordOperator ⋯ ⋯ ⋯ (Sum.inl i) (Sum.inr i)) (optimizerDifferenceL2 hV hVW aV aW p q)) (optimizerDifferenceL2 hV hVW aV aW p q)

The recent difference energy is the plain coordinate pairing of the two halves of the difference field. The difference of two aligned states is aligned, so the doubled operator returns its own swap.

The difference energy on the coefficient space

theorem HCPolySupport.HighContrast.Selection.ae_of_subset {d : ℕ} {V W : Set (Vec d)} (hV : MeasurableSet V) (hVW : V ⊆ W) {Pr : Vec d → Prop} (h : ∀ᵐ (x : Vec d) ∂volumeMeasureOn W, Pr x) : ∀ᵐ (x : Vec d) ∂volumeMeasureOn V, Pr x

theorem HCPolySupport.HighContrast.Selection.optimizerBlockState_ae_congr {d : ℕ} {U : Book.Ch02.Domain d} {aU bU : Book.Ch02.CoeffOn U} (h : aU.AEEq bU) (p q : Vec d) : (fun (x : Vec d) => optimizerBlockState U aU p q x) =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => optimizerBlockState U bU p q x

theorem HCPolySupport.HighContrast.Selection.recentDifferenceEnergy_congr {d : ℕ} {V W : Book.Ch02.Domain d} (hV : MeasurableSet V.carrier) (hVW : V.carrier ⊆ W.carrier) {aV bV : Book.Ch02.CoeffOn V} {aW bW : Book.Ch02.CoeffOn W} (hVeq : aV.AEEq bV) (hWeq : aW.AEEq bW) (p q : Vec d) : recentDifferenceEnergy V W aV aW p q = recentDifferenceEnergy V W bV bW p q

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

The coordinate pairing functional is continuous.

theorem HCPolySupport.HighContrast.Selection.measurable_recentDifferenceEnergy_slice {d : ℕ} {Om : Type u_1} [mOm : MeasurableSpace Om] {V W : Book.Ch02.Domain d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn V.carrier)] [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W.carrier)] {k : ℕ} (hVopen : IsOpen V.carrier) (hVfin : MeasureTheory.volume V.carrier ≠ ⊤) (hVvol : 0 < (MeasureTheory.volume V.carrier).toReal) (hWopen : IsOpen W.carrier) (hWfin : MeasureTheory.volume W.carrier ≠ ⊤) (hWvol : 0 < (MeasureTheory.volume W.carrier).toReal) (hV : MeasurableSet V.carrier) (hVW : V.carrier ⊆ W.carrier) {A : Om → RegCoeffField d} (hSliceW : ∀ (w : Om), AEEQuantitativeEllipticSlice W.carrier k (A w).toFun) (hEntryW : ∀ (i j : Fin d) {φ : Vec d → ℝ}, ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ W.carrier → Measurable fun (w : Om) => entryTestR i j φ (A w)) (aW : Om → Book.Ch02.CoeffOn W) (haW : ∀ (w : Om), (aW w).toCoeffField = (A w).toFun) (p q : Vec d) : Measurable fun (w : Om) => recentDifferenceEnergy V W (restrictCoeffOn hV hVW (aW w)) (aW w) p q

The recent difference energy is measurable on one ellipticity slice.

theorem HCPolySupport.HighContrast.Selection.measurable_recentDifferenceEnergy_coeffSpace {d : ℕ} {V W : Book.Ch02.Domain d} (hVopen : IsOpen V.carrier) (hVbdd : IsBoundedDomain V.carrier) (hVvol : 0 < (MeasureTheory.volume V.carrier).toReal) (hWopen : IsOpen W.carrier) (hWbdd : IsBoundedDomain W.carrier) (hWvol : 0 < (MeasureTheory.volume W.carrier).toReal) (hVW : V.carrier ⊆ W.carrier) (p q : Vec d) : Measurable fun (a : CoeffSpace d) => recentDifferenceEnergy V W (a.coeffOn V) (a.coeffOn W) p q

The recent difference energy is measurable on the coefficient space.

The recent difference energy of an aligned child cell

theorem HCPolySupport.HighContrast.Selection.aestronglyMeasurable_recentDifferenceEnergy_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) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => 1 / 2 * Book.Ch02.average (Response.adaptedDomainAt hq s w) fun (x : Vec d) => blockVecDot (Response.diagonalWeakChildState hq s w (a.subSkew g hg) p r x - Response.diagonalWeakState hq t (a.subSkew g hg) p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑(a.subSkew g hg) x)) (Response.diagonalWeakChildState hq s w (a.subSkew g hg) p r x - Response.diagonalWeakState hq t (a.subSkew g hg) p r x))) P

The measurability half of the per-cell recent difference energy binder, in the shape the profile estimate consumes.

theorem HCPolySupport.HighContrast.Selection.aestronglyMeasurable_adjointRecentDifferenceEnergy_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) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => 1 / 2 * Book.Ch02.average (Response.adaptedDomainAt hq s w) fun (x : Vec d) => blockVecDot (Response.diagonalWeakChildState hq s w (a.subSkew g hg).transpose p r x - Response.diagonalWeakState hq t (a.subSkew g hg).transpose p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑(a.subSkew g hg).transpose x)) (Response.diagonalWeakChildState hq s w (a.subSkew g hg).transpose p r x - Response.diagonalWeakState hq t (a.subSkew g hg).transpose p r x))) P

The measurability half of the adjoint per-cell recent difference energy binder, in the shape the transposed profile estimate consumes.