High-contrast homogenization: Provider.Response.PreYoungPrimalFluxPhysicalProjectionLimit #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The physical primal flux projection limit #
Finite projected primal flux pairings converge to the physical cutoff oscillation. Their common annealed row bound passes to the limit by Fatou's lemma.
theorem
HCPolySupport.HighContrast.Response.tendsto_primal_flux_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 Pcen : Vec d)
:
Filter.Tendsto (fun (n : ℕ) => primalFluxProjectedOscillation hq s t g hg p r Pcen (n + 1) a) Filter.atTop
(nhds (primalFluxPhysicalOscillation hq s t g hg p r Pcen a))
Finite-depth projected primal flux pairings converge pointwise to the physical pairing.
theorem
HCPolySupport.HighContrast.Response.primal_flux_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 Pcen : 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 Pcen (X (matVecMul q y)).2;
cubeBesovPairing R f G = ∑ i : Fin d, Pcen i * volumeAverage U fun (x : Vec d) => (cut x - volumeAverage U cut) * (X x).2 i
The physical primal flux pairing on one parent cell is its coordinate expansion.
theorem
HCPolySupport.HighContrast.Response.integrable_primal_flux_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 Pcen : Vec d)
(hweak : profilePrimalWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤)
:
MeasureTheory.Integrable (primalFluxPhysicalOscillation hq s t g hg p r Pcen) P
A finite primal weak quantity makes the physical flux cutoff oscillation integrable.