High-contrast homogenization: Provider.Response.ProfileRecentMeasurability

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

Measurability of the recent weak-norm sums

The two recent sums are finite combinations of coarse-block observables. The cell term uses two random blocks on the same sample, while the averaged term uses the positive averaged-defect measurability theorem.

theorem HCPolySupport.HighContrast.Response.aemeasurable_blockSize_coarseBlock_sub_coarseBlock {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U V : Set (Vec d)} (hU : HasMeasurableCoarseBlock P U) (hV : HasMeasurableCoarseBlock P V) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : AEMeasurable (fun (a : CoeffSpace d) => blockSize (blockSub (coarseBlock U a) (coarseBlock V a)) E) P

The normalized size of the difference of two random coarse blocks is almost everywhere measurable.

theorem HCPolySupport.HighContrast.Response.aemeasurable_diagonalWeakCellDefect {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : AEMeasurable (diagonalWeakCellDefect q k t E) P

One recent cell defect is almost everywhere measurable.

theorem HCPolySupport.HighContrast.Response.aemeasurable_diagonalWeakCellSum {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) (s : ℝ) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : AEMeasurable (diagonalWeakCellSum q t H s E) P

The recent cell sum is almost everywhere measurable.