High-contrast homogenization: Provider.Response.ProfileMaximumLp

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

Moments of the complete terminal maximum

The below-start maximum is rewritten over the countable aligned labels before measurability is proved. Minkowski then compares the complete history with the centered history and source moment, without an independence assumption.

theorem HCPolySupport.HighContrast.Response.aemeasurable_blockSize_adaptedResponse {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : AEMeasurable (fun (a : CoeffSpace d) => blockSize (adaptedResponse q k w a) F) P

The scalar size of one adapted response against a positive reference is an almost-everywhere measurable statistic.

theorem HCPolySupport.HighContrast.Response.aemeasurable_source_excess_term {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {rhoMax : ℝ} {q : Mat d} (hq : Matrix.PosDef q) (t k : ℤ) (w : Fin d → ℤ) {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : AEMeasurable (fun (a : CoeffSpace d) => ENNReal.ofReal (3 ^ (-rhoMax * (↑t - ↑k)) * blockExcess (adaptedResponse q k w a) F)) P

One weighted source-excess term is almost-everywhere measurable.

theorem HCPolySupport.HighContrast.Response.eLpNorm_profileTotalMaximum_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {Q rhoMax : ℝ} (hQ : 0 < Q) (q : Mat d) (jStar t : ℤ) (F : BlockMat d) (hW : AEMeasurable (profileTotalMaximum P rhoMax q jStar t F) P) : MeasureTheory.eLpNorm (profileTotalMaximum P rhoMax q jStar t F) (ENNReal.ofReal Q) P = profileTotalHistory P Q rhoMax q jStar t F ^ Q⁻¹

The L^Q seminorm of the complete maximum is the Q-th root of its defining history.