High-contrast homogenization: Provider.Response.ProfileWeakLp #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Probabilistic random-centered weak estimates #
The pointwise diagonal estimate is integrated after its maximum is known to be finite almost everywhere. The two maximum events remain correlated with the optimizer energy throughout this step.
theorem
HCPolySupport.HighContrast.Response.eLpNorm_weakRoot_le_profileMajorant
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{root : CoeffSpace d → ENNReal}
{U V En : CoeffSpace d → ℝ}
{M : CoeffSpace d → ENNReal}
(hU0 : ∀ (a : CoeffSpace d), 0 ≤ U a)
(hV0 : ∀ (a : CoeffSpace d), 0 ≤ V a)
(hU : AEMeasurable U P)
(hV : AEMeasurable V P)
(hM : AEMeasurable M P)
(hEn : AEMeasurable En P)
{A B alpha : ℝ}
{H : ℕ}
(hfinite : ∀ᵐ (a : CoeffSpace d) ∂P, M a ≠ ⊤)
(hpoint :
∀ᵐ (a : CoeffSpace d) ∂P, root a ≤ ENNReal.ofReal A * (ENNReal.ofReal (U a) + ENNReal.ofReal (V a)) + ENNReal.ofReal B * if 1 < M a then M a ^ (1 / 2) * ENNReal.ofReal (En a)
else ENNReal.ofReal (3 ^ (-alpha * ↑H)) * ENNReal.ofReal (En a))
(hroot : MeasureTheory.AEStronglyMeasurable root P)
:
MeasureTheory.eLpNorm root 2 P ≤ ENNReal.ofReal A * (MeasureTheory.eLpNorm U 2 P + MeasureTheory.eLpNorm V 2 P) + ENNReal.ofReal B * (profileBadEnergy P M En + profileGoodEnergy P alpha H M En)
A pointwise weak-root majorant with the exact recent and optimizer-event
terms passes to the corresponding L² bound.
The released split level #
theorem
HCPolySupport.HighContrast.Response.eLpNorm_weakRoot_le_profileMajorantAt
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{root : CoeffSpace d → ENNReal}
{U V En : CoeffSpace d → ℝ}
{M : CoeffSpace d → ENNReal}
(hU0 : ∀ (a : CoeffSpace d), 0 ≤ U a)
(hV0 : ∀ (a : CoeffSpace d), 0 ≤ V a)
(hU : AEMeasurable U P)
(hV : AEMeasurable V P)
(hM : AEMeasurable M P)
(hEn : AEMeasurable En P)
{A B alpha : ℝ}
{H : ℕ}
{lev : ENNReal}
(hfinite : ∀ᵐ (a : CoeffSpace d) ∂P, M a ≠ ⊤)
(hpoint :
∀ᵐ (a : CoeffSpace d) ∂P, root a ≤ ENNReal.ofReal A * (ENNReal.ofReal (U a) + ENNReal.ofReal (V a)) + ENNReal.ofReal B * if lev < M a then M a ^ (1 / 2) * ENNReal.ofReal (En a)
else ENNReal.ofReal (3 ^ (-alpha * ↑H)) * ENNReal.ofReal (En a))
(hroot : MeasureTheory.AEStronglyMeasurable root P)
:
MeasureTheory.eLpNorm root 2 P ≤ ENNReal.ofReal A * (MeasureTheory.eLpNorm U 2 P + MeasureTheory.eLpNorm V 2 P) + ENNReal.ofReal B * (profileBadEnergyAt P lev M En + profileGoodEnergyAt P lev alpha H M En)
The L² weak-root majorant at a released split level.