High-contrast homogenization: Provider.Response.ProfileEnergyLp

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

Optimizer-energy bounds in probability

The bad branch uses the complete maximum only through its Q-norm, its pathwise comparison with the total profile, and the total-profile moment. The good branch uses only the deterministic pointwise energy bound. The same two arguments apply to the primal and coefficient-transpose optimizers.

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

The all-scale response maximum is an a.e. measurable statistic.

theorem HCPolySupport.HighContrast.Response.ae_ne_top_of_eLpNorm_le_ofReal {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {Q c : ℝ} (hQ : 0 < Q) {M : CoeffSpace d → ENNReal} (hM : AEMeasurable M P) (hnorm : MeasureTheory.eLpNorm M (ENNReal.ofReal Q) P ≤ ENNReal.ofReal c) : ∀ᵐ (a : CoeffSpace d) ∂P, M a ≠ ⊤

A finite positive L^Q bound forces an extended-real statistic to be finite almost everywhere.

theorem HCPolySupport.HighContrast.Response.rpow_half_mul_ofReal_le_of_le_sqrt_toReal {x : ENNReal} (hx : x ≠ ⊤) {energy C : ℝ} (hC : 0 ≤ C) (henergy : energy ≤ C * √x.toReal) : x ^ (1 / 2) * ENNReal.ofReal energy ≤ ENNReal.ofReal C * x

Multiplying an energy by the square root of a finite extended-real maximum turns a real square-root estimate into a linear maximum estimate.

theorem HCPolySupport.HighContrast.Response.profileBadEnergy_le_of_complete_maximum {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {Q h beta : ℝ} (hQ : 2 < Q) (hh : 0 ≤ h) (hbeta : 0 ≤ beta) {M W : CoeffSpace d → ENNReal} (hM : AEMeasurable M P) (hW : AEMeasurable W P) (hpoint : ∀ (a : CoeffSpace d), M a ≤ W a + ENNReal.ofReal beta) (hnorm : MeasureTheory.eLpNorm M (ENNReal.ofReal Q) P ≤ ENNReal.ofReal (h ^ Q⁻¹ + beta)) (hmoment : ∫⁻ (a : CoeffSpace d), W a ^ Q ∂P ≤ ENNReal.ofReal h) {energy : CoeffSpace d → ℝ} {C : ℝ} (hC : 0 ≤ C) (henergy : ∀ (a : CoeffSpace d), M a ≠ ⊤ → 1 < M a → energy a ≤ C * √(M a).toReal) (hmeas : MeasureTheory.AEStronglyMeasurable ({a : CoeffSpace d | 1 < M a}.indicator fun (a : CoeffSpace d) => M a ^ (1 / 2) * ENNReal.ofReal (energy a)) P) : profileBadEnergy P M energy ≤ ENNReal.ofReal (C * profileBadMajorant Q h beta)

Generic bad-branch energy estimate driven by the complete maximum.

theorem HCPolySupport.HighContrast.Response.profileGoodEnergy_le_of_pointwise {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {alpha : ℝ} {H : ℕ} {M : CoeffSpace d → ENNReal} {energy : CoeffSpace d → ℝ} {C : ℝ} (henergy : ∀ (a : CoeffSpace d), M a ≤ 1 → energy a ≤ C) (hmeas : MeasureTheory.AEStronglyMeasurable ({a : CoeffSpace d | M a ≤ 1}.indicator fun (a : CoeffSpace d) => ENNReal.ofReal (energy a)) P) : profileGoodEnergy P alpha H M energy ≤ ENNReal.ofReal (3 ^ (-alpha * ↑H) * C)

Generic good-branch energy estimate.

The released split level

theorem HCPolySupport.HighContrast.Response.profileGoodEnergyAt_le_of_pointwise {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {alpha : ℝ} {H : ℕ} {lev : ENNReal} {M : CoeffSpace d → ENNReal} {energy : CoeffSpace d → ℝ} {C : ℝ} (henergy : ∀ (a : CoeffSpace d), M a ≤ lev → energy a ≤ C) (hmeas : MeasureTheory.AEStronglyMeasurable ({a : CoeffSpace d | M a ≤ lev}.indicator fun (a : CoeffSpace d) => ENNReal.ofReal (energy a)) P) : profileGoodEnergyAt P lev alpha H M energy ≤ ENNReal.ofReal (3 ^ (-alpha * ↑H) * C)

The released good-event optimizer energy from a pointwise bound on the released good event.

theorem HCPolySupport.HighContrast.Response.profileGoodEnergyAt_diagonalWeakEnergy_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {alpha rho lev : ℝ} {H : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hlev : 1 ≤ lev) (p r : Vec d) : (profileGoodEnergyAt P (ENNReal.ofReal lev) alpha H (diagonalWeakMaximum rho q t E) fun (a : CoeffSpace d) => diagonalWeakEnergy hq t a p r) ≤ ENNReal.ofReal (energyGoodConstantAtLevel lev * 3 ^ (-alpha * ↑H) * profileEnergyLoad (diagonalWeakLoadMinus E p r) p r)

The primal good optimizer energy at a released split level.

theorem HCPolySupport.HighContrast.Response.profileGoodEnergyAt_diagonalWeakAdjointEnergy_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {alpha rho lev : ℝ} {H : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hlev : 1 ≤ lev) (p r : Vec d) : (profileGoodEnergyAt P (ENNReal.ofReal lev) alpha H (diagonalWeakMaximum rho q t E) fun (a : CoeffSpace d) => diagonalWeakAdjointEnergy hq t a p r) ≤ ENNReal.ofReal (energyGoodConstantAtLevel lev * 3 ^ (-alpha * ↑H) * profileEnergyLoad (diagonalWeakLoadPlus E p r) p r)

The adjoint good optimizer energy at a released split level.