High-contrast homogenization: Provider.Response.ProfileWeakFullLp

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

Full annealed-centered weak estimates

The random optimizer average is replaced by its annealed center before the pointwise diagonal estimate is integrated. A sample map is retained so the result applies directly to constant-skew recentering.

theorem HCPolySupport.HighContrast.Response.eLpNorm_profilePrimalWeakRoot_sample_le {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho alpha : ℝ} (hrho : 0 < rho) (hrho1 : rho < 1) (halpha : alpha = (1 - rho) / 2) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (hU : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakCellSum q t H (1 / 2) E (sample a)) P) (hV : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakAverageSum q t H (1 / 2) rho E (sample a)) P) (hM : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t E (sample a)) P) (hEn : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakEnergy hq t (sample a) p r) P) (havg : AEMeasurable (fun (a : CoeffSpace d) => blockCellAverage (adaptedCell q t) (diagonalWeakState hq t (sample a) p r)) P) (hfinite : ∀ᵐ (a : CoeffSpace d) ∂P, diagonalWeakMaximum rho q t E (sample a) ≠ ⊤) (hroot : MeasureTheory.AEStronglyMeasurable (profilePrimalWeakRoot m hq t sample p r (profilePrimalCenter P hq t sample p r)) P) : MeasureTheory.eLpNorm (profilePrimalWeakRoot m hq t sample p r (profilePrimalCenter P hq t sample p r)) 2 P ≤ ENNReal.ofReal (16 * diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r) * (MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => diagonalWeakCellSum q t H (1 / 2) E (sample a)) 2 P + MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => diagonalWeakAverageSum q t H (1 / 2) rho E (sample a)) 2 P) + ENNReal.ofReal (16 * diagonalWeakMetricFactor m E / (2 * alpha)) * ((profileBadEnergy P (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t E (sample a)) fun (a : CoeffSpace d) => diagonalWeakEnergy hq t (sample a) p r) + profileGoodEnergy P alpha H (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t E (sample a)) fun (a : CoeffSpace d) => diagonalWeakEnergy hq t (sample a) p r) + ENNReal.ofReal constantSeminormCoefficient * profilePrimalCenterVariance P m hq t sample p r

The full primal weak root for an arbitrary coefficient sample map has the recent, optimizer-event, and exact centering-variance bound.

theorem HCPolySupport.HighContrast.Response.eLpNorm_profileAdjointWeakRoot_sample_le {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho alpha : ℝ} (hrho : 0 < rho) (hrho1 : rho < 1) (halpha : alpha = (1 - rho) / 2) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (hU : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakCellSum q t H (1 / 2) E (sample a)) P) (hV : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakAverageSum q t H (1 / 2) rho E (sample a)) P) (hM : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t E (sample a)) P) (hEn : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakAdjointEnergy hq t (sample a) p r) P) (havg : AEMeasurable (fun (a : CoeffSpace d) => blockCellAverage (adaptedCell q t) (diagonalWeakAdjointState hq t (sample a) p r)) P) (hfinite : ∀ᵐ (a : CoeffSpace d) ∂P, diagonalWeakMaximum rho q t E (sample a) ≠ ⊤) (hroot : MeasureTheory.AEStronglyMeasurable (profileAdjointWeakRoot m hq t sample p r (profileAdjointCenter P hq t sample p r)) P) : MeasureTheory.eLpNorm (profileAdjointWeakRoot m hq t sample p r (profileAdjointCenter P hq t sample p r)) 2 P ≤ ENNReal.ofReal (16 * diagonalWeakMetricFactor m E * diagonalWeakLoadPlus E p r) * (MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => diagonalWeakCellSum q t H (1 / 2) E (sample a)) 2 P + MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => diagonalWeakAverageSum q t H (1 / 2) rho E (sample a)) 2 P) + ENNReal.ofReal (16 * diagonalWeakMetricFactor m E / (2 * alpha)) * ((profileBadEnergy P (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t E (sample a)) fun (a : CoeffSpace d) => diagonalWeakAdjointEnergy hq t (sample a) p r) + profileGoodEnergy P alpha H (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t E (sample a)) fun (a : CoeffSpace d) => diagonalWeakAdjointEnergy hq t (sample a) p r) + ENNReal.ofReal constantSeminormCoefficient * profileAdjointCenterVariance P m hq t sample p r

The full adjoint weak root retains its independent plus load under the same arbitrary sample map.

The released split level

theorem HCPolySupport.HighContrast.Response.eLpNorm_profilePrimalWeakRoot_sample_at_level_le {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho alpha lev : ℝ} (hrho : 0 < rho) (hrho1 : rho < 1) (hlev : 0 < lev) (halpha : alpha = (1 - rho) / 2) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (hU : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakCellSum q t H (1 / 2) E (sample a)) P) (hV : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakAverageSum q t H (1 / 2) rho E (sample a)) P) (hM : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t E (sample a)) P) (hEn : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakEnergy hq t (sample a) p r) P) (havg : AEMeasurable (fun (a : CoeffSpace d) => blockCellAverage (adaptedCell q t) (diagonalWeakState hq t (sample a) p r)) P) (hfinite : ∀ᵐ (a : CoeffSpace d) ∂P, diagonalWeakMaximum rho q t E (sample a) ≠ ⊤) (hroot : MeasureTheory.AEStronglyMeasurable (profilePrimalWeakRoot m hq t sample p r (profilePrimalCenter P hq t sample p r)) P) : MeasureTheory.eLpNorm (profilePrimalWeakRoot m hq t sample p r (profilePrimalCenter P hq t sample p r)) 2 P ≤ ENNReal.ofReal (recentConstantAtLevel lev * diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r) * (MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => diagonalWeakCellSum q t H (1 / 2) E (sample a)) 2 P + MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => diagonalWeakAverageSum q t H (1 / 2) rho E (sample a)) 2 P) + ENNReal.ofReal (maxGroupConstantAtLevel lev * diagonalWeakMetricFactor m E / (2 * alpha)) * ((profileBadEnergyAt P (ENNReal.ofReal lev) (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t E (sample a)) fun (a : CoeffSpace d) => diagonalWeakEnergy hq t (sample a) p r) + profileGoodEnergyAt P (ENNReal.ofReal lev) alpha H (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t E (sample a)) fun (a : CoeffSpace d) => diagonalWeakEnergy hq t (sample a) p r) + ENNReal.ofReal constantSeminormCoefficient * profilePrimalCenterVariance P m hq t sample p r

The full primal weak root at a released split level.

theorem HCPolySupport.HighContrast.Response.eLpNorm_profileAdjointWeakRoot_sample_at_level_le {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho alpha lev : ℝ} (hrho : 0 < rho) (hrho1 : rho < 1) (hlev : 0 < lev) (halpha : alpha = (1 - rho) / 2) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (hU : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakCellSum q t H (1 / 2) E (sample a)) P) (hV : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakAverageSum q t H (1 / 2) rho E (sample a)) P) (hM : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t E (sample a)) P) (hEn : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakAdjointEnergy hq t (sample a) p r) P) (havg : AEMeasurable (fun (a : CoeffSpace d) => blockCellAverage (adaptedCell q t) (diagonalWeakAdjointState hq t (sample a) p r)) P) (hfinite : ∀ᵐ (a : CoeffSpace d) ∂P, diagonalWeakMaximum rho q t E (sample a) ≠ ⊤) (hroot : MeasureTheory.AEStronglyMeasurable (profileAdjointWeakRoot m hq t sample p r (profileAdjointCenter P hq t sample p r)) P) : MeasureTheory.eLpNorm (profileAdjointWeakRoot m hq t sample p r (profileAdjointCenter P hq t sample p r)) 2 P ≤ ENNReal.ofReal (recentConstantAtLevel lev * diagonalWeakMetricFactor m E * diagonalWeakLoadPlus E p r) * (MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => diagonalWeakCellSum q t H (1 / 2) E (sample a)) 2 P + MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => diagonalWeakAverageSum q t H (1 / 2) rho E (sample a)) 2 P) + ENNReal.ofReal (maxGroupConstantAtLevel lev * diagonalWeakMetricFactor m E / (2 * alpha)) * ((profileBadEnergyAt P (ENNReal.ofReal lev) (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t E (sample a)) fun (a : CoeffSpace d) => diagonalWeakAdjointEnergy hq t (sample a) p r) + profileGoodEnergyAt P (ENNReal.ofReal lev) alpha H (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t E (sample a)) fun (a : CoeffSpace d) => diagonalWeakAdjointEnergy hq t (sample a) p r) + ENNReal.ofReal constantSeminormCoefficient * profileAdjointCenterVariance P m hq t sample p r

The full adjoint weak root at a released split level.