High-contrast homogenization: Provider.Response.SplitReadoutAdjointIntegrability

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

Integrability of adjoint adapted cutoff-split readouts

The adjoint terminal weak quantity controls the child means and cutoff oscillations required by the adjoint five-term split.

theorem HCPolySupport.HighContrast.Response.integrable_adjoint_adaptedFiveTermSplit_readouts {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 : Vec d) (hweak : profileAdjointWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) : (∀ w ∈ alignedIndex q s t, ∀ (alpha : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (diagonalWeakAdjointState hq t (a.subSkew g hg) p r)) alpha) P) ∧ ∀ w ∈ alignedIndex q s t, ∀ (alpha : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (diagonalWeakAdjointState hq t (a.subSkew g hg) p r x) alpha) P

Every adjoint child mean and cutoff-oscillation readout required by the adapted five-term split is integrable under finiteness of the adjoint profile weak quantity.