Coarse-graining support: Support.HighContrast.EntryScale.MomentConsequences.P2

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.HighContrast.EntryScale.finset_sup_rpow_of_pos {ι : Type u_1} (s : Finset ι) (x : ι → ENNReal) {q : ℝ} (hq : 0 < q) : s.sup x ^ q = s.sup fun (i : ι) => x i ^ q

Source label M_m^st: for a positive exponent, raising a finite ENNReal maximum to that exponent commutes with the finite maximum.

theorem HCPolySupport.HighContrast.EntryScale.finset_sup_le_sum_ennreal {ι : Type u_1} (s : Finset ι) (x : ι → ENNReal) : s.sup x ≤ ∑ i ∈ s, x i

Source label l.union.bound: deterministic finite-max step for ENNReal integrands.

theorem HCPolySupport.HighContrast.EntryScale.aemeasurable_finset_sup_ennreal {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Finset ι) (X : ι → Ω → ENNReal) (hX : ∀ i ∈ s, AEMeasurable (X i) μ) : AEMeasurable (fun (ω : Ω) => s.sup fun (i : ι) => X i ω) μ

Source label l.union.bound: a.e. measurability of the finite maximum appearing in the stochastic maximal union bound.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_finset_sup_le_sum_of_lintegral_le {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (s : Finset ι) (X : ι → Ω → ENNReal) (B : ι → ENNReal) (hX : ∀ i ∈ s, AEMeasurable (X i) μ) (hB : ∀ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ ≤ B i) : ∫⁻ (ω : Ω), s.sup fun (i : ι) => X i ω ∂μ ≤ ∑ i ∈ s, B i

Source label l.union.bound: finite-max lintegral bound, the measure-theoretic core of the stochastic maximal union bound.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_finset_sup_weighted_rpow_le_sum {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (s : Finset ι) (w : ι → ENNReal) (X : ι → Ω → ENNReal) (B : ι → ENNReal) {q : ℝ} (hq_nonneg : 0 ≤ q) (hX : ∀ i ∈ s, AEMeasurable (fun (ω : Ω) => X i ω ^ q) μ) (hB : ∀ i ∈ s, ∫⁻ (ω : Ω), X i ω ^ q ∂μ ≤ B i) : ∫⁻ (ω : Ω), s.sup fun (i : ι) => (w i * X i ω) ^ q ∂μ ≤ ∑ i ∈ s, w i ^ q * B i

Source label l.union.bound: weighted real-exponent finite-maximum bound. This is the local real-Q replacement for the integer-moment finite-sup pattern available in the library, with the weights kept explicit for the paper's 3^{-\rho_M(m-j)} factors.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_sup_descendantsAtDepth_weighted_rpow_le_three_pow_mul {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (μ : MeasureTheory.Measure Ω) (Q : TriadicCube d) (n : ℕ) (w : TriadicCube d → ENNReal) (X : TriadicCube d → Ω → ENNReal) {B W : ENNReal} {q : ℝ} (hq_nonneg : 0 ≤ q) (hX : ∀ R ∈ descendantsAtDepth Q n, AEMeasurable (fun (ω : Ω) => X R ω ^ q) μ) (hB : ∀ R ∈ descendantsAtDepth Q n, ∫⁻ (ω : Ω), X R ω ^ q ∂μ ≤ B) (hwB : ∀ R ∈ descendantsAtDepth Q n, w R ^ q * B ≤ W) : ∫⁻ (ω : Ω), (descendantsAtDepth Q n).sup fun (R : TriadicCube d) => (w R * X R ω) ^ q ∂μ ≤ ↑((3 ^ d) ^ n) * W

Source label l.union.bound: weighted real-exponent finite-maximum bound over the library's triadic descendants. The factor ((3 ^ d) ^ n) is exactly the descendant count from HCPolySupport.descendantsAtDepth_card.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_sup_descendantsAtDepth_weighted_rpow_le_card_mul_of_bounds {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (μ : MeasureTheory.Measure Ω) (Q : TriadicCube d) (n : ℕ) (w : TriadicCube d → ENNReal) (X : TriadicCube d → Ω → ENNReal) {B V : ENNReal} {q : ℝ} (hq_nonneg : 0 ≤ q) (hX : ∀ R ∈ descendantsAtDepth Q n, AEMeasurable (fun (ω : Ω) => X R ω ^ q) μ) (hB : ∀ R ∈ descendantsAtDepth Q n, ∫⁻ (ω : Ω), X R ω ^ q ∂μ ≤ B) (hw : ∀ R ∈ descendantsAtDepth Q n, w R ^ q ≤ V) : ∫⁻ (ω : Ω), (descendantsAtDepth Q n).sup fun (R : TriadicCube d) => (w R * X R ω) ^ q ∂μ ≤ ↑((3 ^ d) ^ n) * (V * B)

Source label l.union.bound: one-scale descendant union estimate with the paper's two inputs kept separate: a child high-moment bound and a deterministic weight bound. This is the step producing the factor 3^{d(m-j)} 3^{-Q rho_M(m-j)} 3^{-Q gamma(j-N)} before the convolution in the proof.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_sup_descendantsAtDepth_weighted_highCenteredMoment_le {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (μ : MeasureTheory.Measure Ω) (Q : TriadicCube d) (n : ℕ) (w : TriadicCube d → ENNReal) (X : TriadicCube d → Ω → ENNReal) {B V : ENNReal} (hX : ∀ R ∈ descendantsAtDepth Q n, AEMeasurable (fun (ω : Ω) => X R ω ^ hm.Q) μ) (hB : ∀ R ∈ descendantsAtDepth Q n, ∫⁻ (ω : Ω), X R ω ^ hm.Q ∂μ ≤ B) (hw : ∀ R ∈ descendantsAtDepth Q n, w R ^ hm.Q ≤ V) : ∫⁻ (ω : Ω), (descendantsAtDepth Q n).sup fun (R : TriadicCube d) => (w R * X R ω) ^ hm.Q ∂μ ≤ ↑((3 ^ d) ^ n) * (V * B)

Source labels a.HM and l.union.bound: high-moment-parameter version of the one-scale descendant union estimate, using the real exponent Q from Assumption a.HM.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_sup_Icc_descendantsAtDepth_weighted_highCenteredMoment_le_sum {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (μ : MeasureTheory.Measure Ω) (Q : TriadicCube d) {N m : ℕ} (w : ℕ → TriadicCube d → ENNReal) (X : ℕ → TriadicCube d → Ω → ENNReal) (B V : ℕ → ENNReal) (hX : ∀ j ∈ Finset.Icc N m, ∀ R ∈ descendantsAtDepth Q (m - j), AEMeasurable (fun (ω : Ω) => X j R ω ^ hm.Q) μ) (hB : ∀ j ∈ Finset.Icc N m, ∀ R ∈ descendantsAtDepth Q (m - j), ∫⁻ (ω : Ω), X j R ω ^ hm.Q ∂μ ≤ B j) (hw : ∀ j ∈ Finset.Icc N m, ∀ R ∈ descendantsAtDepth Q (m - j), w j R ^ hm.Q ≤ V j) : ∫⁻ (ω : Ω), (Finset.Icc N m).sup fun (j : ℕ) => (descendantsAtDepth Q (m - j)).sup fun (R : TriadicCube d) => (w j R * X j R ω) ^ hm.Q ∂μ ≤ ∑ j ∈ Finset.Icc N m, ↑((3 ^ d) ^ (m - j)) * (V j * B j)

Source label l.union.bound: sum the one-scale descendant maximal estimates over manuscript scales j = N, ..., m. This is the stochastic union-bound bridge immediately before substituting the explicit decay envelopes.

theorem HCPolySupport.HighContrast.EntryScale.scale_eq_of_mem_descendantsAtDepth_terminal {d : ℕ} {Q R : TriadicCube d} {N j m : ℕ} (hj : j ∈ Finset.Icc N m) (hQ : Q.scale = ↑m) (hR : R ∈ descendantsAtDepth Q (m - j)) : R.scale = ↑j

the library's triadic geometry bridge used by l.union.bound: a descendant at depth m - j of a terminal scale-m cube is a scale-j cube.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_sup_Icc_descendantsAtDepth_weighted_highCenteredMoment_le_sum_of_estimate {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (μ : MeasureTheory.Measure Ω) (Q : TriadicCube d) {N m : ℕ} (hQ : Q.scale = ↑m) (w : ℕ → TriadicCube d → ENNReal) (X : ℕ → TriadicCube d → Ω → ENNReal) (hHM : HighCenteredMomentEstimate hm μ N X) (V : ℕ → ENNReal) (hw : ∀ j ∈ Finset.Icc N m, ∀ R ∈ descendantsAtDepth Q (m - j), w j R ^ hm.Q ≤ V j) : ∫⁻ (ω : Ω), (Finset.Icc N m).sup fun (j : ℕ) => (descendantsAtDepth Q (m - j)).sup fun (R : TriadicCube d) => (w j R * X j R ω) ^ hm.Q ∂μ ≤ ∑ j ∈ Finset.Icc N m, ↑((3 ^ d) ^ (m - j)) * (V j * highCenteredMomentEnvelope hm N j)

Source labels a.HM and l.union.bound: substitute the scale-uniform high centered-moment estimate into the scale-summed descendant union bridge. This is still before terminal normalization losses and weak-norm envelopes are specialized, so the deterministic weights remain an explicit input.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_sup_Icc_descendants_weighted_highCenteredMoment_le_sum {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (μ : MeasureTheory.Measure Ω) (Q : TriadicCube d) {N m : ℕ} (hQ : Q.scale = ↑m) (w : ℕ → TriadicCube d → ENNReal) (X : ℕ → TriadicCube d → Ω → ENNReal) (hHM : HighCenteredMomentEstimate hm μ N X) (terminalCost : ENNReal) (hw : ∀ j ∈ Finset.Icc N m, ∀ R ∈ descendantsAtDepth Q (m - j), w j R ≤ terminalCost * ENNReal.ofReal (3 ^ (-hc.rhoM * ↑(m - j)))) : ∫⁻ (ω : Ω), (Finset.Icc N m).sup fun (j : ℕ) => (descendantsAtDepth Q (m - j)).sup fun (R : TriadicCube d) => (w j R * X j R ω) ^ hm.Q ∂μ ≤ ∑ j ∈ Finset.Icc N m, ↑((3 ^ d) ^ (m - j)) * (terminalWeakMomentWeight hm terminalCost m j * highCenteredMomentEnvelope hm N j)

Source labels a.HM and l.union.bound: substitute both the one-block high-moment estimate and the deterministic terminal/weak-norm multiplier terminalCost * 3^{-rho_M(m-j)} into the scale-summed descendant union bridge.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_sup_Icc_descendants_weighted_highCenteredMoment_le_convolution {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (μ : MeasureTheory.Measure Ω) (Q : TriadicCube d) {N m : ℕ} (hNm : N ≤ m) (hQ : Q.scale = ↑m) (w : ℕ → TriadicCube d → ENNReal) (X : ℕ → TriadicCube d → Ω → ENNReal) (hHM : HighCenteredMomentEstimate hm μ N X) (terminalCost : ENNReal) (hw : ∀ j ∈ Finset.Icc N m, ∀ R ∈ descendantsAtDepth Q (m - j), w j R ≤ terminalCost * ENNReal.ofReal (3 ^ (-hc.rhoM * ↑(m - j)))) : ∫⁻ (ω : Ω), (Finset.Icc N m).sup fun (j : ℕ) => (descendantsAtDepth Q (m - j)).sup fun (R : TriadicCube d) => (w j R * X j R ω) ^ hm.Q ∂μ ≤ terminalCost ^ hm.Q * ENNReal.ofReal (hm.momentCoefficient * (↑(m - N + 1) * 3 ^ (-min (hm.Q * hc.rhoM - ↑d) (hm.Q * hm.gamma) * ↑(m - N))))

Source labels a.HM and l.union.bound: full stochastic maximal lintegral bridge through the manuscript's finite convolution envelope, still with the terminal-normalization polynomial cost left as the explicit terminalCost.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_sup_Icc_descendants_terminalBlockDeviation_le_convolution {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (μ : MeasureTheory.Measure Ω) (Q : TriadicCube d) {N m : ℕ} (hNm : N ≤ m) (hQ : Q.scale = ↑m) (weak : ℕ → TriadicCube d → ENNReal) (Y : ℕ → TriadicCube d → Ω → FullBlockMat d) (hHM : HighCenteredMomentEstimate hm μ N (intermediateCenteredFullBlockDeviation hP hStruct Y)) (hweak : ∀ j ∈ Finset.Icc N m, ∀ R ∈ descendantsAtDepth Q (m - j), weak j R ≤ ENNReal.ofReal (3 ^ (-hc.rhoM * ↑(m - j)))) : ∫⁻ (ω : Ω), (Finset.Icc N m).sup fun (j : ℕ) => (descendantsAtDepth Q (m - j)).sup fun (R : TriadicCube d) => (weak j R * terminalCenteredFullBlockDeviation hP hStruct m Y j R ω) ^ hm.Q ∂μ ≤ ENNReal.ofReal (Book.Ch05.widetildeThetaAtScale P 0 hP4) ^ hm.Q * ENNReal.ofReal (hm.momentCoefficient * (↑(m - N + 1) * 3 ^ (-min (hm.Q * hc.rhoM - ↑d) (hm.Q * hm.gamma) * ↑(m - N))))

Source labels a.HM and l.union.bound: concrete full-block version of the stochastic maximal union bound above the entry scale. The high-moment hypothesis is imposed on the intermediate-normalized centered full-block deviation, while the displayed maximum uses the terminal-normalized deviation; the deterministic comparison from DeterministicAlgebra.lean supplies the factor T = widetildeTheta_0.

theorem HCPolySupport.HighContrast.EntryScale.integral_sup_terminalDeviation_le_highMomentConvolution {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (μ : MeasureTheory.Measure Ω) (Q : TriadicCube d) {N m : ℕ} (hNm : N ≤ m) (hQ : Q.scale = ↑m) (weak : ℕ → TriadicCube d → ENNReal) (a : Ω → RegCoeffField d) (hHM : HighCenteredMomentEstimate hm μ N (intermediateCoarseBlockDeviation hP hStruct a)) (hweak : ∀ j ∈ Finset.Icc N m, ∀ R ∈ descendantsAtDepth Q (m - j), weak j R ≤ ENNReal.ofReal (3 ^ (-hc.rhoM * ↑(m - j)))) : ∫⁻ (ω : Ω), (Finset.Icc N m).sup fun (j : ℕ) => (descendantsAtDepth Q (m - j)).sup fun (R : TriadicCube d) => (weak j R * terminalCoarseBlockDeviation hP hStruct m a j R ω) ^ hm.Q ∂μ ≤ ENNReal.ofReal (Book.Ch05.widetildeThetaAtScale P 0 hP4) ^ hm.Q * ENNReal.ofReal (hm.momentCoefficient * (↑(m - N + 1) * 3 ^ (-min (hm.Q * hc.rhoM - ↑d) (hm.Q * hm.gamma) * ↑(m - N))))

Source labels a.HM and l.union.bound: the library's coarse-block specialization of the terminal-normalized stochastic maximal union bound. The high-moment hypothesis is imposed on the concrete intermediate-normalized coarse-block deviation from a.HM.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_sup_Icc_descendants_terminalBlockDeviation_le_polynomial_convolution {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (μ : MeasureTheory.Measure Ω) (Q : TriadicCube d) {N m : ℕ} (hNm : N ≤ m) (hQ : Q.scale = ↑m) (weak : ℕ → TriadicCube d → ENNReal) (a : Ω → RegCoeffField d) (hHM : HighCenteredMomentEstimate hm μ N (intermediateCoarseBlockDeviation hP hStruct a)) (hweak : ∀ j ∈ Finset.Icc N m, ∀ R ∈ descendantsAtDepth Q (m - j), weak j R ≤ ENNReal.ofReal (3 ^ (-hc.rhoM * ↑(m - j)))) : ∫⁻ (ω : Ω), (Finset.Icc N m).sup fun (j : ℕ) => (descendantsAtDepth Q (m - j)).sup fun (R : TriadicCube d) => (weak j R * terminalCoarseBlockDeviation hP hStruct m a j R ω) ^ hm.Q ∂μ ≤ ENNReal.ofReal ((2 + Book.Ch05.widetildeThetaAtScale P 0 hP4) ^ hm.Q * (hm.momentCoefficient * (↑(m - N + 1) * 3 ^ (-min (hm.Q * hc.rhoM - ↑d) (hm.Q * hm.gamma) * ↑(m - N)))))

Source labels a.HM and l.union.bound: polynomial form of the concrete terminal coarse-block union bound. The terminal normalization comparison gives the manuscript polynomial exponent A = 1.

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalStochasticWeakWeight {d : ℕ} (hc : HighContrastExponents d) (m : ℕ) : ℕ → TriadicCube d → ENNReal

Source label M_m^st: the weak-norm scale weight 3^{-rho_M(m-j)} from the stochastic maximal term.

Equations

• HCPolySupport.HighContrast.EntryScale.terminalStochasticWeakWeight hc m j _R = ENNReal.ofReal (3 ^ (-hc.rhoM * ↑(m - j)))

theorem HCPolySupport.HighContrast.EntryScale.terminalStochasticWeakWeight_inv_sq_eq {d : ℕ} (hc : HighContrastExponents d) (m j : ℕ) (R : TriadicCube d) : (terminalStochasticWeakWeight hc m j R)⁻¹ ^ 2 = ENNReal.ofReal (3 ^ (2 * hc.rhoM * ↑(m - j)))

Source label M_m^st: the square of the inverse weak stochastic weight is the expected positive power of the scale gap.

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalCoarseBlockStochasticEnvelope {Ω : Type u_1} {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (N m : ℕ) (Q : TriadicCube d) (weak : ℕ → TriadicCube d → ENNReal) (a : Ω → RegCoeffField d) : Ω → ENNReal

Source label M_m^st: the unpowered ENNReal finite maximum over scales N <= j <= m and the library's descendants of the terminal cube.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalCoarseBlockStochasticMaxOfWeak {Ω : Type u_1} {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (N m : ℕ) (Q : TriadicCube d) (weak : ℕ → TriadicCube d → ENNReal) (a : Ω → RegCoeffField d) : Ω → ℝ

Source label M_m^st: real-valued version of the terminal stochastic maximum with a supplied weak-norm weight. For the source weight terminalStochasticWeakWeight, this is the finite maximum in the note written with the library's descendants in place of 3^j Lat ∩ cu_m.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalCoarseBlockStochasticMax {Ω : Type u_1} {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hc : HighContrastExponents d) (N m : ℕ) (Q : TriadicCube d) (a : Ω → RegCoeffField d) : Ω → ℝ

Source label M_m^st: the literal terminal stochastic maximum from the note, using the source weak weight 3^{-rho_M(m-j)}.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalCoarseBlockStochasticQEnvelope {Ω : Type u_1} {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (N m : ℕ) (Q : TriadicCube d) (weak : ℕ → TriadicCube d → ENNReal) (a : Ω → RegCoeffField d) : Ω → ENNReal

Source label M_m^st: the ENNReal envelope appearing in the terminal coarse-block union bound, with the Q-th power already inside the finite max.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.EntryScale.aemeasurable_terminalCoarseBlockDeviation_origin_descendant {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) {N j m : ℕ} (hj : j ∈ Finset.Icc N m) {R : TriadicCube d} (hR : R ∈ descendantsAtDepth (originCube d ↑m) (m - j)) : AEMeasurable (fun (a : RegCoeffField d) => terminalCoarseBlockDeviation hP hStruct m (fun (x : RegCoeffField d) => x) j R a) P

Source labels M_m^st and l.S.and.J: P4 integrability and stationarity give a.e. measurability of each terminal-normalized concrete coarse-block deviation over descendants of the terminal origin cube.

theorem HCPolySupport.HighContrast.EntryScale.aemeasurable_terminalCoarseBlockStochasticEnvelope_origin {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) (hc : HighContrastExponents d) (N m : ℕ) : AEMeasurable (terminalCoarseBlockStochasticEnvelope hP hStruct N m (originCube d ↑m) (terminalStochasticWeakWeight hc m) fun (x : RegCoeffField d) => x) P

Source labels M_m^st and l.S.and.J: the source-weighted terminal ENNReal stochastic envelope over the origin terminal cube is a.e. measurable under the coefficient law.

theorem HCPolySupport.HighContrast.EntryScale.aestronglyMeasurable_terminalCoarseBlockStochasticMax_origin {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) (hc : HighContrastExponents d) (N m : ℕ) : MeasureTheory.AEStronglyMeasurable (terminalCoarseBlockStochasticMax hP hStruct hc N m (originCube d ↑m) fun (x : RegCoeffField d) => x) P

Source labels M_m^st and l.S.and.J: the literal real terminal stochastic maximum from the note is a.e. strongly measurable. This discharges the measurability surface needed for the Lyapunov step in the stochastic window estimate.

theorem HCPolySupport.HighContrast.EntryScale.finset_sup_ne_top_of_forall_ne_top {ι : Type u_1} (s : Finset ι) (f : ι → ENNReal) (h : ∀ i ∈ s, f i ≠ ⊤) : s.sup f ≠ ⊤