High-contrast homogenization: Provider.Response.PreYoungPrimalProjectionMeasurability #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.Response.measurable_cubeProjection
{d : ℕ}
(Q : TriadicCube d)
(N : ℕ)
(f : Vec d → ℝ)
:
Measurable (cubeProjection Q N f)
theorem
HCPolySupport.HighContrast.Response.memScalarL2_indicator_pulled_cubeProjection_cutoff
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
{s t : ℤ}
(z : Fin d → ℤ)
(N : ℕ)
:
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 eta := fun (x : Vec d) => cubeProjection R N f (matVecMul q⁻¹ x);
MemScalarL2 (adaptedCell q t) ((adaptedCellAt q s z).indicator eta)
theorem
HCPolySupport.HighContrast.Response.cutoff_projected_primal_pairing_eq_weighted_average
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(s t : ℤ)
(z : Fin d → ℤ)
(F : Vec d → BlockVec d)
(Qcen : Vec d)
(N : ℕ)
(hGInt :
MeasureTheory.IntegrableOn (fun (y : Vec d) => vecDot Qcen (F (matVecMul q y)).1)
(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 Qcen (F (matVecMul q y)).1;
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 Qcen (F x).1
theorem
HCPolySupport.HighContrast.Response.measurable_volumeAverage_weighted_vecDot_primal
{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))
:
Measurable fun (a : CoeffSpace d) =>
volumeAverage (adaptedCellAt q s z) fun (x : Vec d) =>
eta x * vecDot Qcen (diagonalWeakState hq t (a.subSkew g hg) p r x).1
theorem
HCPolySupport.HighContrast.Response.aestronglyMeasurable_cutoff_projected_primal_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 := diagonalWeakState 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