High-contrast homogenization: Provider.Response.SplitReadoutIntegrability

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

Integrability of the adapted cutoff-split readouts

The terminal weak quantity controls every aligned-child mean and cutoff oscillation. Sample measurability then turns these pointwise bounds into the four integrability families used by the primal and adjoint cutoff splits.

theorem HCPolySupport.HighContrast.Response.centeredChild_readout_enorm_bounds {d : ℕ} [NeZero d] {q m0 : Mat d} (hq : Matrix.PosDef q) (hm0 : Matrix.PosDef m0) {s t : ℤ} (hst : s ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q s t) (b : CoeffSpace d) (p r : Vec d) (center : BlockVec d) (alpha : BlockCoord d) : have X := diagonalWeakState hq t b p r; have root := ENNReal.ofReal (3 ^ (-(1 / 2) * ↑t)) * adaptedWeakSeminorm q t (1 / 2) fun (x : Vec d) => blockMatVecMul (Book.Ch02.blockDiag (matSqrt m0) (matSqrt m0)⁻¹) (X x - center); have R := translateCube w (originCube d s); have cardRoot := ENNReal.ofReal √↑(descendantsAtDepth (originCube d t) (t - s).toNat).card; have metricRoot := ENNReal.ofReal √(max (Book.Ch02.matrixFrobeniusNormSq (matSqrt m0)⁻¹) (Book.Ch02.matrixFrobeniusNormSq (matSqrt m0))); have meanCoeff := ENNReal.ofReal (cubeBesovScaleWeight (-(1 / 2)) R)⁻¹ * cardRoot * ENNReal.ofReal (cubeBesovScaleWeight (-(1 / 2)) (originCube d t)) * metricRoot; have oscCoeff := ENNReal.ofReal (1024 * ↑d ^ 4 * max 1 (max smoothTransitionProfile.derivBound smoothTransitionProfile.secondDerivBound) ^ 2 * 3 ^ (-(t - s)) * (cubeBesovCircDepthWeight R (1 / 2) 1)⁻¹) * cardRoot * ENNReal.ofReal (cubeBesovScaleWeight (-(1 / 2)) (originCube d t)) * metricRoot; ENNReal.ofReal |toFullBlockVec (blockCellAverage (adaptedCellAt q s w) X) alpha - toFullBlockVec center alpha| ≤ meanCoeff * root ∧ ENNReal.ofReal |volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (X x) alpha| ≤ oscCoeff * root

The centered child mean and its cutoff oscillation are bounded pointwise by finite geometric factors times the normalized adapted weak root.

theorem HCPolySupport.HighContrast.Response.integrable_primal_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 : profilePrimalWeakQuantity 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) (diagonalWeakState 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 (diagonalWeakState hq t (a.subSkew g hg) p r x) alpha) P

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