High-contrast homogenization: Provider.Response.PreYoungAdjointGradientProjectedRowBound

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

Finite projected adjoint gradient rows

The finite cube projections of the adjoint gradient pairing are integrable, and their annealed absolute values obey the transposed all-earlier row bound.

theorem HCPolySupport.HighContrast.Response.integrable_abs_adjoint_gradient_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 Qcen : Vec d) (hweak : profileAdjointWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => |vecDot Qcen (blockCellAverage (adaptedCellAt q k w) (diagonalWeakAdjointState hq t (a.subSkew g hg) p r)).1|) P

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

theorem HCPolySupport.HighContrast.Response.aestrongly_measurable_adjoint_gradient_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 Qcen : Vec d) (N : ℕ) : MeasureTheory.AEStronglyMeasurable (adjointGradientProjectedOscillation hq s t g hg p r Qcen N) P

Every finite projected adjoint gradient oscillation is almost-everywhere strongly measurable under the coefficient law.