Coarse-graining support: Support.Book.Ch05.Theorems.Section57.LocalizedMaxTail

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

Probability-level localized maximum tails

These lemmas are the no-loss replacements for the logarithmically inflated O_{\Gamma} maximum packaging. The cardinality of the finite family remains as an explicit probability prefactor.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_localizedLimitNormalizedJMax_sub_const_tail_le_card_mul_exp {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hstat : Ch04.RestrictionStationaryLaw Pμ) {σ A c lam : ℝ} (hlam : 1 ≤ lam) {m n : ℕ} (hnm : n < m) (e : FullBlockVec d) (hOrigin : IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma σ) (fun (a : RegCoeffField d) => limitNormalizedBlockJObservable hP hStruct (originCube d ↑n) e a - c) A) : have D := descendantsAtScale (originCube d ↑m) ↑n; MeasureTheory.Measure.real Pμ {a : RegCoeffField d | c + A * lam < localizedLimitNormalizedJMax hP hStruct m n e a} ≤ ↑D.card * Real.exp (-lam ^ σ)

Direct finite-union tail for the localized descendant maximum, for one fixed probe vector.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_localizedNormalizedProbeJMax_sub_const_tail_le_card_mul_card_mul_exp {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hstat : Ch04.RestrictionStationaryLaw Pμ) {σ A c lam : ℝ} (hlam : 1 ≤ lam) {m n : ℕ} (hnm : n < m) (hOrigin : ∀ (i : NormalizedProbeIndex d), IndependentSums.IsBigOWith Pμ (IndependentSums.gammaSigma σ) (fun (a : RegCoeffField d) => limitNormalizedBlockJObservable hP hStruct (originCube d ↑n) (normalizedProbeVec i) a - c) A) : have D := descendantsAtScale (originCube d ↑m) ↑n; have S := Finset.univ; MeasureTheory.Measure.real Pμ {a : RegCoeffField d | c + A * lam < localizedNormalizedProbeJMax hP hStruct m n a} ≤ ↑S.card * (↑D.card * Real.exp (-lam ^ σ))

Direct finite-union tail for the normalized finite-probe maximum.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_localizedLimitNormalizedJMax_tail_le_card_mul_exp_of_isBigO {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hstat : Ch04.RestrictionStationaryLaw Pμ) {σ A lam : ℝ} (hlam : 1 ≤ lam) {m n : ℕ} (hnm : n < m) (e : FullBlockVec d) (hOrigin : IndependentSums.IsBigO Pμ (IndependentSums.gammaSigma σ) (limitNormalizedBlockJObservable hP hStruct (originCube d ↑n) e) A) : have D := descendantsAtScale (originCube d ↑m) ↑n; MeasureTheory.Measure.real Pμ {a : RegCoeffField d | A * lam < localizedLimitNormalizedJMax hP hStruct m n e a} ≤ ↑D.card * Real.exp (-lam ^ σ)

Direct finite-union tail for the localized descendant maximum, using symmetric Γσ tails.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_localizedNormalizedProbeJMax_tail_le_card_mul_card_mul_exp_of_isBigO {d : ℕ} [NeZero d] {Pμ : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier Pμ) (hStruct : Ch04.RestrictionStructuralLaw Pμ) (hstat : Ch04.RestrictionStationaryLaw Pμ) {σ A lam : ℝ} (hlam : 1 ≤ lam) {m n : ℕ} (hnm : n < m) (hOrigin : ∀ (i : NormalizedProbeIndex d), IndependentSums.IsBigO Pμ (IndependentSums.gammaSigma σ) (limitNormalizedBlockJObservable hP hStruct (originCube d ↑n) (normalizedProbeVec i)) A) : have D := descendantsAtScale (originCube d ↑m) ↑n; have S := Finset.univ; MeasureTheory.Measure.real Pμ {a : RegCoeffField d | A * lam < localizedNormalizedProbeJMax hP hStruct m n a} ≤ ↑S.card * (↑D.card * Real.exp (-lam ^ σ))

Direct finite-union tail for the normalized finite-probe maximum, using symmetric Γσ tails and no logarithmic maximum packaging.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_localizedFirstQuenchedEstimate_normalizedProbeJMax_tail_noLog {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Centry : ℝ) (alpha : ℝ), 0 < Cfluct ∧ 0 < Centry ∧ 0 < alpha ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {ell n m : ℕ} {lam : ℝ}, 1 ≤ lam → ell < n → n < m → have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; have tau := min σ 2; have center := Real.rpow 3 (-alpha * ↑ell); have scale := Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + n) - ↑(N0 + ell)).toNat) * hΓ.thetaHat ^ 2; MeasureTheory.Measure.real P {aω : RegCoeffField d | center + scale * lam < localizedNormalizedProbeJMax hP hStruct (N0 + m) (N0 + n) aω} ≤ ↑S.card * (↑D.card * Real.exp (-lam ^ tau))

Localized first-quenched estimate for the finite-probe maximum, kept as a probability-level finite union bound rather than a logarithmically inflated O_{\Gamma} estimate.

theorem HCPolySupport.Book.Ch05.Section57.localizedQuenchedEstimate_probeTail_noLog_of_uniformExponent {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Centry : ℝ) (a : ℝ), 0 < Centry ∧ 0 < a ∧ ∀ {σ : ℝ}, 0 < σ → ∃ (Cfluct : ℝ), 0 < Cfluct ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {ell n m : ℕ} {lam : ℝ}, 1 ≤ lam → ell < n → n < m → have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; have tau := min σ 2; have center := Real.rpow 3 (-a * ↑ell); have scale := Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + n) - ↑(N0 + ell)).toNat) * hΓ.thetaHat ^ 2; MeasureTheory.Measure.real P {aω : RegCoeffField d | center + scale * lam < localizedNormalizedProbeJMax hP hStruct (N0 + m) (N0 + n) aω} ≤ ↑S.card * (↑D.card * Real.exp (-lam ^ tau))

Uniform-in-σ version of measureReal_localizedFirstQuenchedEstimate_normalizedProbeJMax_tail_noLog.