High-contrast homogenization: Provider.Response.PreYoungGapAPartial #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Integrability from measurable response observables #
The optimizer-energy and optimizer-readout observables used by the adapted pre-Young decomposition are strongly measurable in the random coefficient. This module combines those facts with explicit response domination. The terminal and recent-energy families build their integrable response majorants from finite adapted means; the localized split readouts retain an abstract integrable majorant until their quantitative weak-norm bounds are supplied.
Terminal cutoff-energy defects #
theorem
HCPolySupport.HighContrast.Response.integrable_affineSubSkewCutoffEnergyDefect_of_responseJ_domination
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{q : Mat d}
(hq : Matrix.PosDef q)
(t : ℤ)
(hint : HasFiniteAdaptedMean P q t)
(g : Mat d)
(hg : IsSkewMat g)
(p r : Vec d)
(hdom :
∀ (a : CoeffSpace d),
(0 ≤ Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) =>
adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)
(matVecMul (((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField x)
((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) ∧ (Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) =>
adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)
(matVecMul (((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField x)
((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) ≤ 2 * Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r)
:
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) =>
adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)
(matVecMul (((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField x)
((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) - Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r)
P
Measurability of the primal terminal cutoff defect and its pointwise response domination give the literal integrability premise of the terminal component.
theorem
HCPolySupport.HighContrast.Response.integrable_affineAdjointSubSkewCutoffEnergyDefect_of_responseJ_domination
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{q : Mat d}
(hq : Matrix.PosDef q)
(t : ℤ)
(hint : HasFiniteAdaptedMean P q t)
(g : Mat d)
(hg : IsSkewMat g)
(p r : Vec d)
(hdom :
∀ (a : CoeffSpace d),
(0 ≤ Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) =>
adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)
(matVecMul (((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x)
((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) ∧ (Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) =>
adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)
(matVecMul (((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x)
((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) ≤ 2 * Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r)
:
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) =>
adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)
(matVecMul (((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x)
((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) - Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r)
P
Measurability and response domination give the independently transposed terminal cutoff-defect integrability premise.