High-contrast homogenization: Provider.Response.PreYoungAdjointProjectionMeasurability #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Measurability of projected adjoint pairings #
The pulled-back finite cutoff projection is a bounded scalar weight. Applying the adjoint measurable-selection readout on each coordinate and recombining the finite coordinate sum proves strong measurability of both scalar adjoint pairings.
theorem
HCPolySupport.HighContrast.Response.aestronglyMeasurable_volumeAverage_weighted_vecDot_adjoint_gradient
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
(hq : Matrix.PosDef q)
{s t : ℤ}
(hst : s ≤ t)
{z : Fin d → ℤ}
(hz : z ∈ alignedIndex q s t)
(g : Mat d)
(hg : IsSkewMat g)
(p r Qcen : Vec d)
{eta : Vec d → ℝ}
(heta : MemScalarL2 (adaptedCell q t) ((adaptedCellAt q s z).indicator eta))
:
MeasureTheory.AEStronglyMeasurable
(fun (a : CoeffSpace d) =>
volumeAverage (adaptedCellAt q s z) fun (x : Vec d) =>
eta x * vecDot Qcen (diagonalWeakAdjointState hq t (a.subSkew g hg) p r x).1)
P
A weighted adjoint gradient average is strongly measurable in the coefficient sample.
theorem
HCPolySupport.HighContrast.Response.aestronglyMeasurable_volumeAverage_weighted_vecDot_adjoint_flux
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
(hq : Matrix.PosDef q)
{s t : ℤ}
(hst : s ≤ t)
{z : Fin d → ℤ}
(hz : z ∈ alignedIndex q s t)
(g : Mat d)
(hg : IsSkewMat g)
(p r Pcen : Vec d)
{eta : Vec d → ℝ}
(heta : MemScalarL2 (adaptedCell q t) ((adaptedCellAt q s z).indicator eta))
:
MeasureTheory.AEStronglyMeasurable
(fun (a : CoeffSpace d) =>
volumeAverage (adaptedCellAt q s z) fun (x : Vec d) =>
eta x * vecDot Pcen (diagonalWeakAdjointState hq t (a.subSkew g hg) p r x).2)
P
A weighted adjoint flux average is strongly measurable in the coefficient sample.
theorem
HCPolySupport.HighContrast.Response.aestronglyMeasurable_cutoff_projected_adjoint_gradient_pairing_subSkew
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
(hq : Matrix.PosDef q)
{s t : ℤ}
(hst : s ≤ t)
{z : Fin d → ℤ}
(hz : z ∈ alignedIndex q s t)
(g : Mat d)
(hg : IsSkewMat g)
(p r Qcen : Vec d)
(N : ℕ)
:
MeasureTheory.AEStronglyMeasurable
(fun (a : CoeffSpace d) =>
have R := translateCube z (originCube d s);
have phi := fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y);
have f := fun (y : Vec d) => phi y - cubeAverage R phi;
have F := diagonalWeakAdjointState hq t (a.subSkew g hg) p r;
have G := fun (y : Vec d) => vecDot Qcen (F (matVecMul q y)).1;
cubeBesovPairing R f (cubeProjection R N G))
P
The finite-depth adjoint gradient pairing is strongly measurable in the coefficient sample.
theorem
HCPolySupport.HighContrast.Response.aestronglyMeasurable_cutoff_projected_adjoint_flux_pairing_subSkew
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
(hq : Matrix.PosDef q)
{s t : ℤ}
(hst : s ≤ t)
{z : Fin d → ℤ}
(hz : z ∈ alignedIndex q s t)
(g : Mat d)
(hg : IsSkewMat g)
(p r Pcen : Vec d)
(N : ℕ)
:
MeasureTheory.AEStronglyMeasurable
(fun (a : CoeffSpace d) =>
have R := translateCube z (originCube d s);
have phi := fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y);
have f := fun (y : Vec d) => phi y - cubeAverage R phi;
have F := diagonalWeakAdjointState hq t (a.subSkew g hg) p r;
have G := fun (y : Vec d) => vecDot Pcen (F (matVecMul q y)).2;
cubeBesovPairing R f (cubeProjection R N G))
P
The finite-depth adjoint flux pairing is strongly measurable in the coefficient sample.