Coarse-graining support: Support.Book.Ch05.Theorems.Section57.AbsoluteBadScaleTail #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Absolute bad-scale tail #
This file assembles the shifted tail above the annealed entry scale with the small-bottom tail below it. The result is an absolute bad-tail estimate for the unshifted finite-probe envelope.
theorem
HCPolySupport.Book.Ch05.Section57.exists_quantitative_threshold_absoluteBadTail_quenchedProbeEnvelope_le_interpolated_tail
{d : ℕ}
[NeZero d]
{σ : ℝ}
(hσ_pos : 0 < σ)
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (Cfluct : ℝ) (CcrudeShift : ℝ) (Csmall : ℝ) (Centry : ℝ) (a : ℝ),
0 < Cfluct ∧ 0 < CcrudeShift ∧ 0 < Csmall ∧ 0 < Centry ∧ 0 < a ∧ ∀ {t α : ℝ},
have K := quenchedProbeEnvelopeConst d;
have S := Finset.univ;
have b := ↑d / 2;
have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have ctop := min (t - α) (min (b - α) (min ((t - α) * (1 + b / a)) (b - α * (1 + b / a))));
have τ := finiteQuenchedTailTau σ;
have η := finiteQuenchedTailExponent d σ t;
have w := ↑(3 ^ d);
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (τ * (t - α) / η);
have ρcrude := 3 ^ (t - α);
have Cbottom := Real.exp 1 * max 1 ↑S.card;
have Ctop := ↑S.card * weightedLinearExpKernelConst w (ρtop ^ τ);
have Kbottom := weightedGeometricExpKernelConst w (ρbottom ^ η);
have Kcrude := weightedGeometricExpKernelConst w (ρcrude ^ σ);
have Mshift := max 1 (max 0 Ctop + max 0 (Cbottom * Kbottom) + max 0 (↑S.card * Kcrude));
have ρgap := 3 ^ η;
0 < t →
t ≤ b →
0 ≤ α →
α < t →
α < b →
α * (1 + b / a) < b →
α < a →
∃ (Rshift : ℕ) (Rsmall : ℕ) (Runion : ℕ),
∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct),
hΓ.sigma = σ →
hΓ.params = params →
have N0 :=
annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry;
have H := quenchedProbeEnvelope hP hStruct;
have Dhigh := 2 * K * Cfluct * hΓ.thetaHat ^ 2;
have Dcrude := K * CcrudeShift * hΓ.thetaHat ^ 2;
have DenShift := mixedBottomTailDenominator Dhigh Dcrude η τ σ;
have Ohigh := τ * b * (L + 1) / η;
have Ocrude := σ * t * (L + 1) / η;
⋯
Quantitative absolute bad-tail bound. The entry scale is still explicit;
the following layer compresses the displayed scale to the manuscript
exp(C log^2(2 + thetaHat)) envelope.
theorem
HCPolySupport.Book.Ch05.Section57.exists_threshold_absoluteBadTail_le_interpolatedAnnealedTailExponent
{d : ℕ}
[NeZero d]
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (Centry : ℝ) (a : ℝ),
0 < Centry ∧ 0 < a ∧ ∀ {σ : ℝ},
0 < σ →
∃ (Cfluct : ℝ) (CcrudeShift : ℝ) (Csmall : ℝ),
0 < Cfluct ∧ 0 < CcrudeShift ∧ 0 < Csmall ∧ ∀ {t α : ℝ},
have K := quenchedProbeEnvelopeConst d;
have S := Finset.univ;
have b := ↑d / 2;
have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have ctop := min (t - α) (min (b - α) (min ((t - α) * (1 + b / a)) (b - α * (1 + b / a))));
have τ := finiteQuenchedTailTau σ;
have η := finiteQuenchedTailExponent d σ t;
have w := ↑(3 ^ d);
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (τ * (t - α) / η);
have ρcrude := 3 ^ (t - α);
have Cbottom := Real.exp 1 * max 1 ↑S.card;
have Ctop := ↑S.card * weightedLinearExpKernelConst w (ρtop ^ τ);
have Kbottom := weightedGeometricExpKernelConst w (ρbottom ^ η);
have Kcrude := weightedGeometricExpKernelConst w (ρcrude ^ σ);
have Mshift := max 1 (max 0 Ctop + max 0 (Cbottom * Kbottom) + max 0 (↑S.card * Kcrude));
have ρgap := 3 ^ η;
0 < t →
t ≤ b →
0 ≤ α →
α < t →
α < b →
α * (1 + b / a) < b →
α < a →
∃ (Rshift : ℕ) (Rsmall : ℕ) (Runion : ℕ),
∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct),
hΓ.sigma = σ →
hΓ.params = params →
have N0 :=
annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity
Centry;
have H := quenchedProbeEnvelope hP hStruct;
have Dhigh := 2 * K * Cfluct * hΓ.thetaHat ^ 2;
have Dcrude := K * CcrudeShift * hΓ.thetaHat ^ 2;
have DenShift := mixedBottomTailDenominator Dhigh Dcrude η τ σ;
⋯
Uniform-in-σ version of
exists_quantitative_threshold_absoluteBadTail_quenchedProbeEnvelope_le_interpolated_tail.