High-contrast homogenization: Provider.Response.PreYoungPrimalFluxProjectedRowBound

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

Finite projected primal flux rows

The finite cube projections of the primal flux pairing are integrable, and their annealed absolute values obey the all-earlier hatted-row estimate.

theorem HCPolySupport.HighContrast.Response.integrable_abs_primal_flux_cell_pairing_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) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k 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 (fun (a : CoeffSpace d) => |vecDot Pcen (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t (a.subSkew g hg) p r)).2|) P

Finiteness of the primal weak quantity makes every absolute flux-slot cell pairing integrable over the coefficient law.

theorem HCPolySupport.HighContrast.Response.aestrongly_measurable_primal_flux_projected_oscillation {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) (g : Mat d) (hg : IsSkewMat g) (p r Pcen : Vec d) (N : ℕ) : MeasureTheory.AEStronglyMeasurable (primalFluxProjectedOscillation hq s t g hg p r Pcen N) P

Every finite projected primal flux oscillation is almost-everywhere strongly measurable under the coefficient law.