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

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

Absolute quantitative minimal scale

This file converts the absolute bad-tail estimate into the corresponding localized quenched estimate above an explicit absolute minimal scale.

theorem HCPolySupport.Book.Ch05.Section57.exists_quantitative_absolute_quenchedLocalizedEstimate_interpolated {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) / η; ⋯

theorem HCPolySupport.Book.Ch05.Section57.exists_quantitative_absolute_quenchedLocalizedEstimate_interpolated_uniformAnnealedExponent {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_absolute_quenchedLocalizedEstimate_interpolated.