High-contrast homogenization: Provider.Quenched.ScaledMaximumStrictSource #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
A scaled-maximum tail with a strict source event #
The source-tail assumption in CoarseEllipticityDagger is strict. This
variant uses the strict slack cSrc < C from the half-threshold argument
instead of strengthening that input to a closed tail event.
theorem
HCPolySupport.HighContrast.Quenched.measureReal_scaled_max_one_tail_le_of_source_lt
{Ω : Type u_1}
[MeasurableSpace Ω]
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{Rmix Ssrc : Ω → ℝ}
{L C cMix cSrc cd η t : ℝ}
{Ψ : ℝ → ℝ}
(hL : 0 < L)
(ht : 1 ≤ t)
(hC : 1 < C)
(hcMix : cMix ≤ C)
(hcSrc : cSrc < C)
(hmix : P.real {ω : Ω | cMix * t ≤ Rmix ω} ≤ Real.exp (-cd * t ^ η))
(hsrc : P.real (IndependentSums.upperTailEvent Ssrc (cSrc * t)) ≤ (Ψ (cSrc * t))⁻¹)
:
Union bound for a scaled normalized maximum, with a closed mixing tail and a strict source tail. No independence between the random scales is needed.