Coarse-graining support: Support.Book.Ch05.Theorems.Section57.QuenchedLocalizedEstimate #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Localized estimate above the quantitative minimal scale #
This file connects the abstract bad-tail minimal scale to the concrete
finite-probe envelope. The stochastic input is the almost-sure good-tail
event for the bad scales; the tail estimate for the same scale is supplied in
MinimalScaleTail.
theorem
HCPolySupport.Book.Ch05.Section57.quenchedLocalizedEstimate_shifted_above_quenchedMinimalScale
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
{t α : ℝ}
{Nentry Nmin : ℕ}
(hgoodAE :
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (Nentry + M) (Nentry + N) aω;
∀ᵐ (aω : RegCoeffField d) ∂P, hasGoodTailFrom Nmin (badScaleEvent Hshift t α) aω)
:
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (Nentry + M) (Nentry + N) aω;
have Bad := badScaleEvent Hshift t α;
have X := quenchedMinimalScale Nmin Bad;
(∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ (e : FullBlockVec d),
e ⬝ᵥ e ≤ 1 →
∀ᵐ (aω : RegCoeffField d) ∂P, ∀ {m n : ℕ},
X aω ≤ 3 ^ m →
n < m →
3 ^ (-t * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct (Nentry + m) (Nentry + n) e aω ≤ (3 ^ m / X aω) ^ (-α)
Shifted localized quenched estimate above the tail-based minimal scale.
theorem
HCPolySupport.Book.Ch05.Section57.quenchedLocalizedEstimate_shifted_from_badTailBounds
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
{t α η B : ℝ}
{Nentry Nmin : ℕ}
(hη_pos : 0 < η)
(hB : 1 ≤ B)
(hsmall :
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (Nentry + M) (Nentry + N) aω;
have Bad := badScaleEvent Hshift t α;
∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), Nmin ≤ N ∧ MeasureTheory.Measure.real P (badTailEvent Bad N) ≤ ε)
(htail :
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (Nentry + M) (Nentry + N) aω;
have Bad := badScaleEvent Hshift t α;
∀ (N : ℕ),
Nmin ≤ N → MeasureTheory.Measure.real P (badTailEvent Bad N) ≤ Real.exp (-(Real.rpow 3 ↑(N - Nmin) / B) ^ η))
:
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (Nentry + M) (Nentry + N) aω;
have Bad := badScaleEvent Hshift t α;
have X := quenchedMinimalScale Nmin Bad;
IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (3 * 3 ^ Nmin * B) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ (e : FullBlockVec d),
e ⬝ᵥ e ≤ 1 →
∀ᵐ (aω : RegCoeffField d) ∂P, ∀ {m n : ℕ},
X aω ≤ 3 ^ m →
n < m →
3 ^ (-t * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct (Nentry + m) (Nentry + n) e aω ≤ (3 ^ m / X aω) ^ (-α)
Tail-bound form of the shifted localized estimate. The two hypotheses on
badTailEvent are the exact quantitative inputs produced by the bad-scale
summation step: one gives the stochastic integrability of X, the other
removes the null exceptional set with no good tail.
theorem
HCPolySupport.Book.Ch05.Section57.quenchedLocalizedEstimate_shifted_from_badScaleBounds
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
{t α η B : ℝ}
{Nentry Nmin : ℕ}
(hα_nonneg : 0 ≤ α)
(hη_pos : 0 < η)
(hB : 1 ≤ B)
(hsmall :
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (Nentry + M) (Nentry + N) aω;
have Bad := badScaleEvent Hshift t α;
∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), Nmin ≤ N ∧ MeasureTheory.Measure.real P (Bad N) ≤ ε)
(htail :
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (Nentry + M) (Nentry + N) aω;
have Bad := badScaleEvent Hshift t α;
∀ (N : ℕ), Nmin ≤ N → MeasureTheory.Measure.real P (Bad N) ≤ Real.exp (-(Real.rpow 3 ↑(N - Nmin) / B) ^ η))
:
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (Nentry + M) (Nentry + N) aω;
have Bad := badScaleEvent Hshift t α;
have X := quenchedMinimalScale Nmin Bad;
IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (3 * 3 ^ Nmin * B) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ (e : FullBlockVec d),
e ⬝ᵥ e ≤ 1 →
∀ᵐ (aω : RegCoeffField d) ∂P, ∀ {m n : ℕ},
X aω ≤ 3 ^ m →
n < m →
3 ^ (-t * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct (Nentry + m) (Nentry + n) e aω ≤ (3 ^ m / X aω) ^ (-α)
Version of quenchedLocalizedEstimate_shifted_from_badTailBounds whose
quantitative input is stated directly for the manuscript bad-scale events.
Since badScaleEvent H t α is antitone in the bad scale for 0 ≤ α, the
tail event over all later bad scales is contained in the bad-scale event at
the first level.
theorem
HCPolySupport.Book.Ch05.Section57.quenchedLocalizedEstimate_shifted_from_badTailBound
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
{t α η B : ℝ}
{Nentry Nmin : ℕ}
(hη_pos : 0 < η)
(hB : 1 ≤ B)
(htail :
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (Nentry + M) (Nentry + N) aω;
have Bad := badScaleEvent Hshift t α;
∀ (N : ℕ),
Nmin ≤ N → MeasureTheory.Measure.real P (badTailEvent Bad N) ≤ Real.exp (-(Real.rpow 3 ↑(N - Nmin) / B) ^ η))
:
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (Nentry + M) (Nentry + N) aω;
have Bad := badScaleEvent Hshift t α;
have X := quenchedMinimalScale Nmin Bad;
IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (3 * 3 ^ Nmin * B) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ (e : FullBlockVec d),
e ⬝ᵥ e ≤ 1 →
∀ᵐ (aω : RegCoeffField d) ∂P, ∀ {m n : ℕ},
X aω ≤ 3 ^ m →
n < m →
3 ^ (-t * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct (Nentry + m) (Nentry + n) e aω ≤ (3 ^ m / X aω) ^ (-α)
Tail-bound-only version of
quenchedLocalizedEstimate_shifted_from_badTailBounds. The epsilon-smallness
input needed to remove the exceptional no-good-tail set follows from the same
stretched-exponential tail bound.