High-contrast homogenization: Provider.Response.PreYoungPrimalFluxProjectionMeasurability #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Measurability of projected primal flux pairings #
Finite cube projections of the cutoff pull back to bounded scalar weights on each adapted parent cell. The measurable-selection API for the optimizer therefore makes the projected scalar flux pairing measurable in the coefficient sample.
theorem
HCPolySupport.HighContrast.Response.cutoff_projected_primal_flux_pairing_eq_weighted_average
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(s t : ℤ)
(z : Fin d → ℤ)
(F : Vec d → BlockVec d)
(Pcen : Vec d)
(N : ℕ)
(hGInt :
MeasureTheory.IntegrableOn (fun (y : Vec d) => vecDot Pcen (F (matVecMul q y)).2)
(cubeSet (translateCube z (originCube d s))) MeasureTheory.volume)
:
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 G := fun (y : Vec d) => vecDot Pcen (F (matVecMul q y)).2;
have eta := fun (x : Vec d) => cubeProjection R N f (matVecMul q⁻¹ x);
cubeBesovPairing R f (cubeProjection R N G) = volumeAverage (adaptedCellAt q s z) fun (x : Vec d) => eta x * vecDot Pcen (F x).2
A projected scalar flux pairing is its weighted physical-cell average.
theorem
HCPolySupport.HighContrast.Response.measurable_volumeAverage_weighted_vecDot_primal_flux
{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))
:
Measurable fun (a : CoeffSpace d) =>
volumeAverage (adaptedCellAt q s z) fun (x : Vec d) =>
eta x * vecDot Pcen (diagonalWeakState hq t (a.subSkew g hg) p r x).2
A weighted primal flux average over an aligned cell is measurable in the coefficient sample.
theorem
HCPolySupport.HighContrast.Response.aestronglyMeasurable_cutoff_projected_primal_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 := diagonalWeakState 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 primal flux pairing is strongly measurable in the coefficient sample.