High-contrast homogenization: Provider.Response.ProfileEnergyLpBadAtLevel

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

The bad optimizer energy at a released split level

The bad branch of the optimizer-energy estimate, with the bad-event level a parameter. The fixed-level statements are these at lev = 1: the carrier profileBadEnergyAt and the majorant profileBadMajorantAt are both the fixed-level objects on the nose there, so nothing is lost by stating the estimate here and specializing.

The proofs are the fixed-level ones with the complete-maximum comparison read at the released level. Both use the released pointwise energy bounds, whose level hypothesis is the printed range's left endpoint 1 ≤ lev.

theorem HCPolySupport.HighContrast.Response.profileBadEnergyAt_le_of_complete_maximum {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {Q h beta lev : ℝ} (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 ≠ ⊤ → ENNReal.ofReal lev < M a → energy a ≤ C * √(M a).toReal) (hmeas : MeasureTheory.AEStronglyMeasurable ({a : CoeffSpace d | ENNReal.ofReal lev < M a}.indicator fun (a : CoeffSpace d) => M a ^ (1 / 2) * ENNReal.ofReal (energy a)) P) : profileBadEnergyAt P (ENNReal.ofReal lev) M energy ≤ ENNReal.ofReal (C * profileBadMajorantAt Q h beta lev)

The generic bad-branch estimate at a released level. The complete-maximum comparison, the energy's pathwise bound on the bad event and the total-profile moment, all read at the level lev.

theorem HCPolySupport.HighContrast.Response.profileBadEnergyAt_diagonalWeakEnergy_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {Q h beta lev rho : ℝ} (hQ : 2 < Q) (hh : 0 ≤ h) (hbeta : 0 ≤ beta) (hlev : 1 ≤ lev) {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {W : CoeffSpace d → ENNReal} (hW : AEMeasurable W P) (hpoint : ∀ (a : CoeffSpace d), diagonalWeakMaximum rho q t E a ≤ W a + ENNReal.ofReal beta) (hnorm : MeasureTheory.eLpNorm (diagonalWeakMaximum rho q t E) (ENNReal.ofReal Q) P ≤ ENNReal.ofReal (h ^ Q⁻¹ + beta)) (hmoment : ∫⁻ (a : CoeffSpace d), W a ^ Q ∂P ≤ ENNReal.ofReal h) (p r : Vec d) : (profileBadEnergyAt P (ENNReal.ofReal lev) (diagonalWeakMaximum rho q t E) fun (a : CoeffSpace d) => diagonalWeakEnergy hq t a p r) ≤ ENNReal.ofReal (√2 * profileEnergyLoad (diagonalWeakLoadMinus E p r) p r * profileBadMajorantAt Q h beta lev)

The primal bad optimizer energy at a released level.

theorem HCPolySupport.HighContrast.Response.profileBadEnergyAt_diagonalWeakAdjointEnergy_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {Q h beta lev rho : ℝ} (hQ : 2 < Q) (hh : 0 ≤ h) (hbeta : 0 ≤ beta) (hlev : 1 ≤ lev) {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {W : CoeffSpace d → ENNReal} (hW : AEMeasurable W P) (hpoint : ∀ (a : CoeffSpace d), diagonalWeakMaximum rho q t E a ≤ W a + ENNReal.ofReal beta) (hnorm : MeasureTheory.eLpNorm (diagonalWeakMaximum rho q t E) (ENNReal.ofReal Q) P ≤ ENNReal.ofReal (h ^ Q⁻¹ + beta)) (hmoment : ∫⁻ (a : CoeffSpace d), W a ^ Q ∂P ≤ ENNReal.ofReal h) (p r : Vec d) : (profileBadEnergyAt P (ENNReal.ofReal lev) (diagonalWeakMaximum rho q t E) fun (a : CoeffSpace d) => diagonalWeakAdjointEnergy hq t a p r) ≤ ENNReal.ofReal (√2 * profileEnergyLoad (diagonalWeakLoadPlus E p r) p r * profileBadMajorantAt Q h beta lev)

The adjoint bad optimizer energy at a released level.