High-contrast homogenization: Provider.Response.CutoffTerminalEnergyIntegrability #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Integrability of the terminal cutoff energy #
The adapted cutoff lies between zero and two. Its weighted optimizer energy is therefore bounded by twice the full optimizer energy, whose value is the response functional. A finite terminal coarse-block moment then supplies the integrable majorant for both the primal and independently transposed problems.
theorem
HCPolySupport.HighContrast.Response.cutoffWeightedTerminalEnergy_nonneg_le_two_responseJ
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(t : ℤ)
(a : CoeffSpace d)
(p r : Vec 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 p r).toH1.grad x)
(matVecMul ((a.coeffOn (adaptedDomain hq t)).toCoeffField x)
((centeredResponseOptimizer (adaptedDomain hq t) a 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 p r).toH1.grad x)
(matVecMul ((a.coeffOn (adaptedDomain hq t)).toCoeffField x)
((centeredResponseOptimizer (adaptedDomain hq t) a p r).toH1.grad x)))) ≤ 2 * Book.Ch02.responseJ (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) p r
The cutoff-weighted primal terminal energy lies between zero and twice the terminal response value.
theorem
HCPolySupport.HighContrast.Response.cutoffWeightedTerminalAdjointEnergy_nonneg_le_two_responseJ
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(t : ℤ)
(a : CoeffSpace d)
(p r : Vec 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 p r).toH1.grad x)
(matVecMul ((a.transpose.coeffOn (adaptedDomain hq t)).toCoeffField x)
((centeredAdjointOptimizer (adaptedDomain hq t) a 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 p r).toH1.grad x)
(matVecMul ((a.transpose.coeffOn (adaptedDomain hq t)).toCoeffField x)
((centeredAdjointOptimizer (adaptedDomain hq t) a p r).toH1.grad x)))) ≤ 2 * Book.Ch02.responseJ (adaptedDomain hq t) (a.transpose.coeffOn (adaptedDomain hq t)) p r
The independently transposed cutoff-weighted terminal energy has the same response-value domination.
theorem
HCPolySupport.HighContrast.Response.integrable_cutoffWeightedTerminalEnergyDefect_subSkew
{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)
:
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
A terminal coarse-block moment gives the exact primal cutoff-defect integrability premise of the cutoff component.
theorem
HCPolySupport.HighContrast.Response.integrable_cutoffWeightedTerminalAdjointEnergyDefect_subSkew
{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)
:
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
The same terminal moment gives the literal independently transposed cutoff-defect integrability.