High-contrast homogenization: Provider.Response.PreYoungPrimalPhysicalRow

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The physical primal cutoff row

The physical projection limit is rewritten as the literal cutoff-oscillation row appearing in the decomposition of the primal cutoff mean.

theorem HCPolySupport.HighContrast.Response.integral_primal_physical_oscillation_eq_cutoff_row {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 ≠ ⊤) : ∫ (a : CoeffSpace d), primalPhysicalOscillation hq s t g hg p r Qcen a ∂P = avsum (alignedIndex q s t) fun (z : Fin d → ℤ) => ∑ i : Fin d, Qcen i * ∫ (a : CoeffSpace d), volumeAverage (adaptedCellAt q s z) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s z) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (diagonalWeakState hq t (a.subSkew g hg) p r x) (Sum.inl i) ∂P

Annealed integration of the physical primal pairing equals the coordinate cutoff-oscillation row on the terminal parent partition.