Coarse-graining support: Support.Book.Ch05.Theorems.Section57.BadScaleTailDenominator #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Denominator selection for the interpolated bad-scale tail #
This file removes the explicit denominator-domination side conditions from the mixed high-bottom component bound by choosing the normalizing denominator as the maximum of the two branch denominators at the correct powers.
theorem
HCPolySupport.Book.Ch05.Section57.rpow_three_div_den_rpow_le_of_exponent_le
{X Y D Den η γ : ℝ}
(hη : 0 < η)
(hγ : 0 < γ)
(hD : 0 < D)
(hDen : 0 < Den)
(hDpow : D ^ γ ≤ Den ^ η)
(hXY : X ≤ Y)
:
If the denominator for a normalized eta-tail dominates the branch
denominator after raising to the relevant powers, and the exponent in the
normalized tail is no larger than the branch exponent, then the normalized
tail parameter is bounded by the branch tail parameter.
noncomputable def
HCPolySupport.Book.Ch05.Section57.mixedBottomTailDenominator
(Dhigh Dcrude η τ σ : ℝ)
:
The denominator that dominates both branch denominators after raising to the corrected finite exponent.
Equations
Instances For
theorem
HCPolySupport.Book.Ch05.Section57.branch_denominator_le_mixedBottomTailDenominator_pow_eta
{Dhigh Dcrude η τ σ : ℝ}
(hη : 0 < η)
(hτ : 0 < τ)
(hσ : 0 < σ)
(hDhigh : 0 < Dhigh)
(hDcrude : 0 < Dcrude)
:
Dhigh ^ τ ≤ mixedBottomTailDenominator Dhigh Dcrude η τ σ ^ η ∧ Dcrude ^ σ ≤ mixedBottomTailDenominator Dhigh Dcrude η τ σ ^ η
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighTopBadScaleProbability_le_interpolated_kernel
{d : ℕ}
[NeZero d]
{σ Cfluct Centry a : ℝ}
(hσ_pos : 0 < σ)
(params : QuantitativeCoarseGrainedEllipticityParams d)
(hCfluct : 0 < Cfluct)
(hCentry : 0 < Centry)
(ha : 0 < a)
(hpair :
∀ {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 : ℕ},
have K := quenchedProbeEnvelopeConst d;
have x := αbad * ↑(m - q) - t * ↑(m - n);
have ell := ⌈(a * Real.log 3)⁻¹ * (Real.log (max (2 * K) 1) + x * Real.log 3)⌉₊;
have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry;
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω;
have D := descendantsAtScale (originCube d ↑(N0 + m)) ↑(N0 + n);
have S := Finset.univ;
have tau := min σ 2;
have scale := Cfluct * 3 ^ (-↑d / 2 * ↑(n - ell)) * hΓ.thetaHat ^ 2;
have T := Real.rpow 3 (-x);
have lam := T / (2 * K * scale);
ell < n →
n < m →
q ≤ m →
1 ≤ lam →
MeasureTheory.Measure.real P (badPairEvent Hshift t αbad q m n) ≤ ↑S.card * (↑D.card * Real.exp (-lam ^ tau)))
{t αbad Den : ℝ}
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
:
hΓ.sigma = σ →
hΓ.params = params →
∀ {q : ℕ},
have K := quenchedProbeEnvelopeConst d;
have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry;
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω;
have S := Finset.univ;
have b := ↑d / 2;
have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have c := min (t - αbad) (min (b - αbad) (min ((t - αbad) * (1 + b / a)) (b - αbad * (1 + b / a))));
have τ := finiteQuenchedTailTau σ;
have η := finiteQuenchedTailExponent d σ t;
have w := ↑(3 ^ d);
have Dhigh := 2 * K * Cfluct * hΓ.thetaHat ^ 2;
have A := 3 ^ (↑q - τ * b * (L + 1) / η) / Den;
have ρ := 3 ^ c;
0 < t →
t ≤ b →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
0 < Den →
Dhigh ^ τ ≤ Den ^ η →
1 ≤ A →
MeasureTheory.Measure.real P (highTopBadScaleEvent Hshift K a t αbad q) ≤ ↑S.card * (Real.exp (-A ^ η) * weightedLinearExpKernelConst w (ρ ^ τ))
High-top component rewritten with the corrected finite bad-scale exponent. The proof uses the same raw high-range estimate as the original high-top component and only changes the deterministic tail parameter.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedBottomBadScaleProbability_le_interpolated_kernel
{d : ℕ}
[NeZero d]
{σ Ccrude : ℝ}
(hσ_pos : 0 < σ)
(hCcrude : 0 < Ccrude)
{params : QuantitativeCoarseGrainedEllipticityParams d}
(hcomponent :
∀ {Centry 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 : ℕ},
have K := quenchedProbeEnvelopeConst d;
have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry;
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω;
have S := Finset.univ;
have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have w := ↑(3 ^ d);
have Aold := 3 ^ (t * ↑q - t * (L + 1)) / (K * Ccrude * hΓ.thetaHat ^ 2);
have ρ := 3 ^ (t - αbad);
0 < a →
0 < t →
αbad < t →
1 ≤ Aold →
MeasureTheory.Measure.real P (crudeBottomBadScaleEvent Hshift K a t αbad q) ≤ ↑(q + 1) * (↑S.card * w ^ q) * (Real.exp (-Aold ^ σ) * weightedGeometricExpKernelConst w (ρ ^ σ)))
{Centry a t αbad Den : ℝ}
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
:
hΓ.sigma = σ →
hΓ.params = params →
∀ {q : ℕ},
have K := quenchedProbeEnvelopeConst d;
have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry;
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) => quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω;
have S := Finset.univ;
have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have η := finiteQuenchedTailExponent d σ t;
have w := ↑(3 ^ d);
have Dcrude := K * Ccrude * hΓ.thetaHat ^ 2;
have A := 3 ^ (↑q - σ * t * (L + 1) / η) / Den;
have ρ := 3 ^ (t - αbad);
0 < a →
0 < t →
αbad < t →
0 < Den →
Dcrude ^ σ ≤ Den ^ η →
1 ≤ A →
MeasureTheory.Measure.real P (crudeBottomBadScaleEvent Hshift K a t αbad q) ≤ ↑(q + 1) * (↑S.card * w ^ q) * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρ ^ σ))
Crude-bottom component rewritten with the corrected finite bad-scale
exponent. This is the deterministic conversion of the crude
sigma * t endpoint into the common finite exponent.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedCrudeBottomBadScaleEvent_quenchedProbeEnvelope_le_interpolated_kernel
{d : ℕ}
[NeZero d]
{σ : ℝ}
(hσ_pos : 0 < σ)
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (Ccrude : ℝ),
0 < Ccrude ∧ ∀ {Centry a t αbad Den : ℝ} {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct),
hΓ.sigma = σ →
hΓ.params = params →
∀ {q : ℕ},
have K := quenchedProbeEnvelopeConst d;
have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry;
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) =>
quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω;
have S := Finset.univ;
have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have η := finiteQuenchedTailExponent d σ t;
have w := ↑(3 ^ d);
have Dcrude := K * Ccrude * hΓ.thetaHat ^ 2;
have A := 3 ^ (↑q - σ * t * (L + 1) / η) / Den;
have ρ := 3 ^ (t - αbad);
0 < a →
0 < t →
αbad < t →
0 < Den →
Dcrude ^ σ ≤ Den ^ η →
1 ≤ A →
MeasureTheory.Measure.real P (crudeBottomBadScaleEvent Hshift K a t αbad q) ≤ ↑(q + 1) * (↑S.card * w ^ q) * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρ ^ σ))
Public crude-bottom component bound with its tail parameter rewritten in terms of the corrected finite exponent.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedHighBottomBadScaleEvent_quenchedProbeEnvelope_le_interpolated_weighted_kernel
{d : ℕ}
[NeZero d]
{σ : ℝ}
(hσ_pos : 0 < σ)
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (Cfluct : ℝ) (Ccrude : ℝ) (Centry : ℝ) (a : ℝ),
0 < Cfluct ∧ 0 < Ccrude ∧ 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 : ℕ},
have K := quenchedProbeEnvelopeConst d;
have N0 := annealedAlgebraicEntryScale P hΓ.toQuantitativeCoarseGrainedEllipticity Centry;
have Hshift := fun (M N : ℕ) (aω : RegCoeffField d) =>
quenchedProbeEnvelope hP hStruct (N0 + M) (N0 + N) aω;
have S := Finset.univ;
have b := ↑d / 2;
have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have τ := finiteQuenchedTailTau σ;
have η := finiteQuenchedTailExponent d σ t;
have w := ↑(3 ^ d);
have Dhigh := 2 * K * Cfluct * hΓ.thetaHat ^ 2;
have Dcrude := K * Ccrude * hΓ.thetaHat ^ 2;
have Den := mixedBottomTailDenominator Dhigh Dcrude η τ σ;
have A := 3 ^ (↑q - τ * b * (L + 1) / η) / Den;
have ρ := 3 ^ (τ * (t - αbad) / η);
have Cpref := Real.exp 1 * max 1 ↑S.card;
0 < t →
t ≤ b →
αbad < t →
1 ≤ A →
MeasureTheory.Measure.real P (highBottomBadScaleEvent Hshift K a t αbad q) ≤ ↑(q + 1) * (Cpref * w ^ q) * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρ ^ η))
High-bottom component bound with the concrete mixed denominator selected.