High-contrast homogenization: Provider.Quenched.ScaledMaximumTail

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

Tail bound for a deterministically scaled maximum

This file records the union-bound step that combines the finite-range mixing scale and the restored microscopic source scale. The common deterministic factor cancels before either tail estimate is applied, so it does not enter the source gauge.

theorem HCPolySupport.HighContrast.Quenched.measurable_scaled_max_one {Ω : Type u_1} [MeasurableSpace Ω] {Rmix Ssrc : Ω → ℝ} (hRmix : Measurable Rmix) (hSsrc : Measurable Ssrc) (L : ℝ) : Measurable fun (ω : Ω) => L * max 1 (max (Rmix ω) (Ssrc ω))

The normalized scaled maximum used by the source is measurable.

theorem HCPolySupport.HighContrast.Quenched.one_le_scaled_max_one {Ω : Type u_1} {Rmix Ssrc : Ω → ℝ} {L : ℝ} (hL : 1 ≤ L) (ω : Ω) : 1 ≤ L * max 1 (max (Rmix ω) (Ssrc ω))

The source-normalized scaled maximum is pointwise at least one as soon as its deterministic factor is.