High-contrast homogenization: Provider.Response.PreYoungPrimalPhysicalProjectionLimit #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The physical primal projection limit #
Finite projected primal pairings converge to the physical cutoff oscillation. Their common annealed row bound passes to that limit by Fatou's lemma.
theorem
HCPolySupport.HighContrast.Response.tendsto_primal_projected_oscillation
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
{s t : ℤ}
(hst : s ≤ t)
(g : Mat d)
(hg : IsSkewMat g)
(a : CoeffSpace d)
(p r Qcen : Vec d)
:
Filter.Tendsto (fun (n : ℕ) => primalProjectedOscillation hq s t g hg p r Qcen (n + 1) a) Filter.atTop
(nhds (primalPhysicalOscillation hq s t g hg p r Qcen a))
Finite-depth projected primal pairings converge pointwise to the physical pairing.
theorem
HCPolySupport.HighContrast.Response.primal_physical_parent_pairing_eq_coordinate_sum
{d : ℕ}
[NeZero 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)
(a : CoeffSpace d)
(p r Qcen : Vec d)
:
have U := adaptedCellAt q s z;
have cut := adaptedPreYoungCutoff q hq t;
have X := diagonalWeakState hq t (a.subSkew g hg) p r;
have R := translateCube z (originCube d s);
have phi := fun (y : Vec d) => cut (matVecMul q y);
have f := fun (y : Vec d) => phi y - cubeAverage R phi;
have G := fun (y : Vec d) => vecDot Qcen (X (matVecMul q y)).1;
cubeBesovPairing R f G = ∑ i : Fin d, Qcen i * volumeAverage U fun (x : Vec d) => (cut x - volumeAverage U cut) * (X x).1 i
The physical primal pairing on one parent cell is its coordinate expansion.
theorem
HCPolySupport.HighContrast.Response.integrable_primal_physical_oscillation_of_weak
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{q m0 : Mat d}
(hq : Matrix.PosDef q)
(hm0 : Matrix.PosDef m0)
{s t : ℤ}
(hst : s ≤ t)
(g : Mat d)
(hg : IsSkewMat g)
(p r Qcen : Vec d)
(hweak : profilePrimalWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤)
:
MeasureTheory.Integrable (primalPhysicalOscillation hq s t g hg p r Qcen) P
A finite primal weak quantity makes the physical cutoff oscillation integrable.