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

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

Bad-pair tail estimates

This file contains the one-pair tail estimates used by the quantitative minimal-scale proof.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_le_exp_of_subset_upperTail_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {E : Set Ω} {A σ s : ℝ} (hX : IndependentSums.IsBigOWith μ (IndependentSums.gammaSigma σ) X A) (hs : 1 ≤ s) (hE : E ⊆ IndependentSums.upperTailEvent X (A * s)) : μ.real E ≤ Real.exp (-s ^ σ)

A Γ-tail controls any event contained in the corresponding upper-tail event.

theorem HCPolySupport.Book.Ch05.Section57.thresholdEvent_subset_centered_upperTail {Ω : Type u_1} {H : Ω → ℝ} {A c T s : ℝ} (hcenter : c ≤ T / 2) (hscale : A * s ≤ T / 2) : {ω : Ω | T < H ω} ⊆ IndependentSums.upperTailEvent (fun (ω : Ω) => H ω - c) (A * s)

If the deterministic center and stochastic Γ-scale each fit into half of the target threshold, then the threshold exceedance is a centered upper-tail event.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_discounted_badPair_le_exp_of_isBigOWith_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : Ω → ℝ} {A c T s σ discount R : ℝ} (hX : IndependentSums.IsBigOWith μ (IndependentSums.gammaSigma σ) (fun (ω : Ω) => H ω - c) A) (hs : 1 ≤ s) (hdiscount_pos : 0 < discount) (hthreshold : discount * T ≤ R) (hcenter : c ≤ T / 2) (hscale : A * s ≤ T / 2) : μ.real {ω : Ω | R < discount * H ω} ≤ Real.exp (-s ^ σ)

One-pair bad-event estimate for a discounted observable. The hypothesis discount * T ≤ R says that T is a post-discount threshold below the bad event threshold R.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_discounted_badPair_le_exp_of_isBigO_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {H : Ω → ℝ} {A T s σ discount R : ℝ} (hX : IndependentSums.IsBigO μ (IndependentSums.gammaSigma σ) H A) (hs : 1 ≤ s) (hdiscount_pos : 0 < discount) (hthreshold : discount * T ≤ R) (hscale : A * s ≤ T) : μ.real {ω : Ω | R < discount * H ω} ≤ Real.exp (-s ^ σ)

One-pair bad-event estimate from a symmetric Γ-bound, used for the crude bottom-scale contribution.

def HCPolySupport.Book.Ch05.Section57.badPairEvent {Ω : Type u_2} (H : ℕ → ℕ → Ω → ℝ) (t α : ℝ) (N m n : ℕ) : Set Ω

The fixed-pair component of badScaleEvent.

Equations

• HCPolySupport.Book.Ch05.Section57.badPairEvent H t α N m n = {ω : Ω | n < m ∧ N ≤ m ∧ 3 ^ (-t * ↑(m - n)) * H m n ω > 3 ^ (-α * ↑(m - N))}

def HCPolySupport.Book.Ch05.Section57.badScaleEvent {Ω : Type u_2} (H : ℕ → ℕ → Ω → ℝ) (t α : ℝ) (N : ℕ) : Set Ω

The bad event used in the quantitative minimal-scale theorem: at scale N, some larger pair (m,n) violates the discounted algebraic estimate.

Equations

• HCPolySupport.Book.Ch05.Section57.badScaleEvent H t α N = {ω : Ω | ∃ (m : ℕ), ∃ n < m, N ≤ m ∧ 3 ^ (-t * ↑(m - n)) * H m n ω > 3 ^ (-α * ↑(m - N))}

theorem HCPolySupport.Book.Ch05.Section57.badScaleEvent_eq_iUnion_badPairEvent {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {t α : ℝ} {N : ℕ} : badScaleEvent H t α N = ⋃ (p : ℕ × ℕ), badPairEvent H t α N p.1 p.2

theorem HCPolySupport.Book.Ch05.Section57.localizedFirstQuenchedEstimate_quenchedProbeEnvelope {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Centry : ℝ) (α : ℝ), 0 < Cfluct ∧ 0 < Centry ∧ 0 < α ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {ℓ n m : ℕ}, ℓ < n → n < m → have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; IndependentSums.IsBigOWith P (IndependentSums.gammaSigma (min σ 2)) (fun (a : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + m) (N0 + n) a - quenchedProbeEnvelopeConst d * Real.rpow 3 (-α * ↑ℓ)) (quenchedProbeEnvelopeConst d * ((3 * Real.log ↑S.card) ^ (min σ 2)⁻¹ * ((3 * Real.log ↑D.card) ^ (min σ 2)⁻¹ * (Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + n) - ↑(N0 + ℓ)).toNat) * hΓ.thetaHat ^ 2))))

Localized first-quenched estimate for the concrete finite-probe envelope.

The only change from localizedFirstQuenchedEstimate_normalizedProbeJMax is the deterministic multiplication by the dimension-only envelope constant.

theorem HCPolySupport.Book.Ch05.Section57.isBigO_quenchedProbeEnvelope {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {m n : ℕ}, n < m → have D := descendantsAtScale (originCube d ↑m) ↑n; have S := Finset.univ; IndependentSums.IsBigO P (IndependentSums.gammaSigma σ) (quenchedProbeEnvelope hP hStruct m n) (quenchedProbeEnvelopeConst d * ((3 * Real.log ↑S.card) ^ σ⁻¹ * ((3 * Real.log ↑D.card) ^ σ⁻¹ * (C * hΓ.thetaHat ^ 2))))

Crude Γσ estimate for the concrete finite-probe envelope.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHigh_badPairEvent_quenchedProbeEnvelope_le_exp {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Cfluct : ℝ) (Centry : ℝ) (a : ℝ), 0 < Cfluct ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t αbad : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {q m n ℓ : ℕ} {s T : ℝ}, ℓ < n → n < m → q ≤ m → 1 ≤ s → have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry; have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n); have S := Finset.univ; have A := quenchedProbeEnvelopeConst d * ((3 * Real.log ↑S.card) ^ (min σ 2)⁻¹ * ((3 * Real.log ↑D.card) ^ (min σ 2)⁻¹ * (Cfluct * 3 ^ (-↑d / 2 * ↑(↑(N0 + n) - ↑(N0 + ℓ)).toNat) * hΓ.thetaHat ^ 2))); have c := quenchedProbeEnvelopeConst d * Real.rpow 3 (-a * ↑ℓ); have discount := 3 ^ (-t * ↑(m - n)); have R := 3 ^ (-αbad * ↑(m - q)); discount * T ≤ R → c ≤ T / 2 → A * s ≤ T / 2 → MeasureTheory.Measure.real P (badPairEvent (fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω) t αbad q m n) ≤ Real.exp (-s ^ min σ 2)

Fixed-pair high-scale bad-event estimate, after shifting the deterministic entry scale to zero. The three threshold hypotheses are deterministic and are where the later interpolation choice of ℓ is used.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_crude_badPairEvent_quenchedProbeEnvelope_le_exp {d : ℕ} [NeZero d] {σ t αbad : ℝ} (hσ_pos : 0 < σ) (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∀ {N m n : ℕ} {s T : ℝ}, n < m → N ≤ m → 1 ≤ s → have D := descendantsAtScale (originCube d ↑m) ↑n; have S := Finset.univ; have A := quenchedProbeEnvelopeConst d * ((3 * Real.log ↑S.card) ^ σ⁻¹ * ((3 * Real.log ↑D.card) ^ σ⁻¹ * (C * hΓ.thetaHat ^ 2))); have discount := 3 ^ (-t * ↑(m - n)); have R := 3 ^ (-αbad * ↑(m - N)); discount * T ≤ R → A * s ≤ T → MeasureTheory.Measure.real P (badPairEvent (quenchedProbeEnvelope hP hStruct) t αbad N m n) ≤ Real.exp (-s ^ σ)

Fixed-pair crude bad-event estimate for the concrete envelope.