High-contrast homogenization: Provider.Response.CutoffEnergyObservables

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

The cutoff-weighted terminal optimizer energy

The terminal cutoff energy of the weak-norm estimate for the optimizer state is the localized optimizer energy of the adapted parent cell at the pre-Young cutoff weight, minus the response functional of the same cell. The cutoff is smooth and bounded, so both terms are measurable functions of the sample, in the primal and in the adjoint orientation.

The cutoff is a bounded smooth weight

theorem HCPolySupport.HighContrast.Selection.measurable_adaptedPreYoungCutoff {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) : Measurable (Response.adaptedPreYoungCutoff q hq t)

theorem HCPolySupport.HighContrast.Selection.abs_adaptedPreYoungCutoff_le_two {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (x : Vec d) : |Response.adaptedPreYoungCutoff q hq t x| ≤ 2

The cutoff-energy defect of the adapted parent cell

theorem HCPolySupport.HighContrast.Selection.measurable_cutoffOptimizerEnergyDefect {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (p r : Vec d) : Measurable fun (b : CoeffSpace d) => weightedOptimizerEnergy (Response.adaptedDomain hq t) (b.coeffOn (Response.adaptedDomain hq t)) p r (Response.adaptedPreYoungCutoff q hq t) - Book.Ch02.responseJ (Response.adaptedDomain hq t) (b.coeffOn (Response.adaptedDomain hq t)) p r

The cutoff-weighted terminal optimizer energy defect is measurable on the coefficient space.

theorem HCPolySupport.HighContrast.Selection.aestronglyMeasurable_affineSubSkewCutoffEnergyDefect {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (P : MeasureTheory.Measure (CoeffSpace d)) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => (Book.Ch02.average (Response.adaptedDomain hq t) fun (x : Vec d) => Response.adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((Response.centeredResponseOptimizer (Response.adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).coeffOn (Response.adaptedDomain hq t)).toCoeffField x) ((Response.centeredResponseOptimizer (Response.adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) - Book.Ch02.responseJ (Response.adaptedDomain hq t) ((a.subSkew g hg).coeffOn (Response.adaptedDomain hq t)) p r) P

The measurability half of the primal cutoff-energy binder, in the shape the terminal component consumes.

theorem HCPolySupport.HighContrast.Selection.aestronglyMeasurable_affineAdjointSubSkewCutoffEnergyDefect {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (P : MeasureTheory.Measure (CoeffSpace d)) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => (Book.Ch02.average (Response.adaptedDomain hq t) fun (x : Vec d) => Response.adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((Response.centeredAdjointOptimizer (Response.adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).transpose.coeffOn (Response.adaptedDomain hq t)).toCoeffField x) ((Response.centeredAdjointOptimizer (Response.adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) - Book.Ch02.responseJ (Response.adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (Response.adaptedDomain hq t)) p r) P

The measurability half of the adjoint cutoff-energy binder, in the shape the transposed terminal component consumes.