High-contrast homogenization: Provider.Response.ProfileMaximumBadLp

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

The maximal bad event in L²

Only a Q-moment of the complete maximum is used. Hölder at exponents Q / 2 and Q / (Q - 2) separates its L² restriction from the probability of the bad event; no higher moment or independence assumption enters.

theorem HCPolySupport.HighContrast.Response.eLpNorm_indicator_gt_one_le_mul_measure {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) {Q : ℝ} (hQ : 2 < Q) {M : Ω → ENNReal} (hM : AEMeasurable M P) : MeasureTheory.eLpNorm ({a : Ω | 1 < M a}.indicator M) 2 P ≤ MeasureTheory.eLpNorm M (ENNReal.ofReal Q) P * P {a : Ω | 1 < M a} ^ (1 / 2 - Q⁻¹)

Restricting an extended-real random variable to {M > 1} costs its L^Q norm times the probability of that event to the Hölder exponent.

theorem HCPolySupport.HighContrast.Response.measure_gt_one_le_of_complete_maximum {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) {Q h beta : ℝ} (hQ : 2 < Q) (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) {M W : Ω → ENNReal} (hW : AEMeasurable W P) (hpoint : ∀ (a : Ω), M a ≤ W a + ENNReal.ofReal beta) (hmoment : ∫⁻ (a : Ω), W a ^ Q ∂P ≤ ENNReal.ofReal h) : P {a : Ω | 1 < M a} ≤ ENNReal.ofReal (h / (1 - beta) ^ Q)

The pathwise comparison M ≤ W + beta and the Q-moment of W give the small-drift probability bound for the event {M > 1}.

theorem HCPolySupport.HighContrast.Response.eLpNorm_indicator_gt_one_le_profileBadMajorant {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {Q h beta : ℝ} (hQ : 2 < Q) (hh : 0 ≤ h) (hbeta : 0 ≤ beta) {M W : Ω → ENNReal} (hM : AEMeasurable M P) (hW : AEMeasurable W P) (hpoint : ∀ (a : Ω), M a ≤ W a + ENNReal.ofReal beta) (hnorm : MeasureTheory.eLpNorm M (ENNReal.ofReal Q) P ≤ ENNReal.ofReal (h ^ Q⁻¹ + beta)) (hmoment : ∫⁻ (a : Ω), W a ^ Q ∂P ≤ ENNReal.ofReal h) : MeasureTheory.eLpNorm ({a : Ω | 1 < M a}.indicator M) 2 P ≤ ENNReal.ofReal (profileBadMajorant Q h beta)

The complete-maximum comparison gives exactly the correlated bad-event majorant used by the profile response estimate.

theorem HCPolySupport.HighContrast.Response.eLpNorm_indicator_gt_level_le_mul_measure {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) {Q : ℝ} (hQ : 2 < Q) (lam : ENNReal) {M : Ω → ENNReal} (hM : AEMeasurable M P) : MeasureTheory.eLpNorm ({a : Ω | lam < M a}.indicator M) 2 P ≤ MeasureTheory.eLpNorm M (ENNReal.ofReal Q) P * P {a : Ω | lam < M a} ^ (1 / 2 - Q⁻¹)

Companion of eLpNorm_indicator_gt_one_le_mul_measure. Restricting to {lam < M} costs the L^Q norm times the probability to the Hölder exponent — at every level, the fixed level playing no role in the argument.

Companion 2: the small-drift probability bound, at a released level

theorem HCPolySupport.HighContrast.Response.measure_gt_level_le_of_complete_maximum {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) {Q h beta lev : ℝ} (hQ : 2 < Q) (hbeta0 : 0 ≤ beta) (hbetalev : beta < lev) {M W : Ω → ENNReal} (hW : AEMeasurable W P) (hpoint : ∀ (a : Ω), M a ≤ W a + ENNReal.ofReal beta) (hmoment : ∫⁻ (a : Ω), W a ^ Q ∂P ≤ ENNReal.ofReal h) : P {a : Ω | ENNReal.ofReal lev < M a} ≤ ENNReal.ofReal (h / (lev - beta) ^ Q)

Companion of measure_gt_one_le_of_complete_maximum. The deterministic part beta need only sit below the split level, not below 1.

Companion 3: the bad-event majorant, at a released level

theorem HCPolySupport.HighContrast.Response.eLpNorm_indicator_gt_level_le_profileBadMajorantAt {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] {Q h beta lev : ℝ} (hQ : 2 < Q) (hh : 0 ≤ h) (hbeta : 0 ≤ beta) {M W : Ω → ENNReal} (hM : AEMeasurable M P) (hW : AEMeasurable W P) (hpoint : ∀ (a : Ω), M a ≤ W a + ENNReal.ofReal beta) (hnorm : MeasureTheory.eLpNorm M (ENNReal.ofReal Q) P ≤ ENNReal.ofReal (h ^ Q⁻¹ + beta)) (hmoment : ∫⁻ (a : Ω), W a ^ Q ∂P ≤ ENNReal.ofReal h) : MeasureTheory.eLpNorm ({a : Ω | ENNReal.ofReal lev < M a}.indicator M) 2 P ≤ ENNReal.ofReal (profileBadMajorantAt Q h beta lev)

Companion of eLpNorm_indicator_gt_one_le_profileBadMajorant. The complete-maximum comparison at a released split level.