Coarse-graining support: Support.Book.Ch05.Theorems.Section57.BadScaleTailJoint #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Joint bad-scale component assembly with synchronized constants #
The estimates in this file choose the raw high and crude constants once and then feed the top, mixed-bottom, and crude-bottom branches into the deterministic bad-scale split. The large-scale cutoff and denominator lower bounds are still explicit side conditions; later files discharge them by choosing a threshold.
theorem
HCPolySupport.Book.Ch05.Section57.measureReal_shiftedBadScaleEvent_quenchedProbeEnvelope_le_interpolated_component_sum
{d : ℕ}
[NeZero d]
{σ : ℝ}
(hσ_pos : 0 < σ)
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (Cfluct : ℝ) (Ccrude : ℝ) (Centry : ℝ) (a : ℝ),
0 < Cfluct ∧ 0 < Ccrude ∧ 0 < Centry ∧ 0 < 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 b := ↑d / 2;
have L := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
have ctop :=
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 Dcrude := K * Ccrude * hΓ.thetaHat ^ 2;
have A := 3 ^ (↑q - τ * b * (L + 1) / η) / Den;
have Acrude := 3 ^ (↑q - σ * t * (L + 1) / η) / Den;
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (τ * (t - αbad) / η);
have ρcrude := 3 ^ (t - αbad);
have Cbottom := Real.exp 1 * max 1 ↑S.card;
0 < t →
t ≤ b →
0 ≤ αbad →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
αbad < a →
0 < Den →
Dhigh ^ τ ≤ Den ^ η →
Dcrude ^ σ ≤ Den ^ η →
1 ≤ A →
1 ≤ Acrude →
(have Lcut := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
Lcut + 1 < (1 - αbad / a) * ↑q) →
MeasureTheory.Measure.real P (badScaleEvent Hshift t αbad q) ≤ ↑S.card * (Real.exp (-A ^ η) * weightedLinearExpKernelConst w (ρtop ^ τ)) + ↑(q + 1) * (Cbottom * w ^ q) * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρbottom ^ η)) + ↑(q + 1) * (↑S.card * w ^ q) * (Real.exp (-Acrude ^ η) * weightedGeometricExpKernelConst w (ρcrude ^ σ))
Synchronized three-component bad-scale tail bound, before the deterministic threshold and prefactor absorption steps.
theorem
HCPolySupport.Book.Ch05.Section57.shiftedBadScaleProbability_le_interpolated_component_sum_uniformAnnealedExponent
{d : ℕ}
[NeZero d]
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (Centry : ℝ) (a : ℝ),
0 < Centry ∧ 0 < a ∧ ∀ {σ : ℝ},
0 < σ →
∃ (Cfluct : ℝ) (Ccrude : ℝ),
0 < Cfluct ∧ 0 < Ccrude ∧ ∀ {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 ctop :=
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 Dcrude := K * Ccrude * hΓ.thetaHat ^ 2;
have A := 3 ^ (↑q - τ * b * (L + 1) / η) / Den;
have Acrude := 3 ^ (↑q - σ * t * (L + 1) / η) / Den;
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (τ * (t - αbad) / η);
have ρcrude := 3 ^ (t - αbad);
have Cbottom := Real.exp 1 * max 1 ↑S.card;
0 < t →
t ≤ b →
0 ≤ αbad →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
αbad < a →
0 < Den →
Dhigh ^ τ ≤ Den ^ η →
Dcrude ^ σ ≤ Den ^ η →
1 ≤ A →
1 ≤ Acrude →
(have Lcut := (a * Real.log 3)⁻¹ * ⋯;
Lcut + 1 < (1 - αbad / a) * ↑q) →
MeasureTheory.Measure.real P (badScaleEvent Hshift t αbad q) ≤ ⋯ + ↑(q + 1) * (↑S.card * w ^ q) * (Real.exp (-Acrude ^ η) * weightedGeometricExpKernelConst w (ρcrude ^ σ))
Uniform-in-σ synchronized three-component bad-scale tail bound.
The annealed entry constant and exponent are fixed before σ; the high and
crude fluctuation constants are still chosen after the finite moment exponent.
theorem
HCPolySupport.Book.Ch05.Section57.shiftedBadScaleProbability_le_interpolated_component_sum_selected_denominator
{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 ctop :=
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 Dcrude := K * Ccrude * hΓ.thetaHat ^ 2;
have Den := mixedBottomTailDenominator Dhigh Dcrude η τ σ;
have A := 3 ^ (↑q - τ * b * (L + 1) / η) / Den;
have Acrude := 3 ^ (↑q - σ * t * (L + 1) / η) / Den;
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (τ * (t - αbad) / η);
have ρcrude := 3 ^ (t - αbad);
have Cbottom := Real.exp 1 * max 1 ↑S.card;
0 < t →
t ≤ b →
0 ≤ αbad →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
αbad < a →
1 ≤ A →
1 ≤ Acrude →
(have Lcut := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
Lcut + 1 < (1 - αbad / a) * ↑q) →
MeasureTheory.Measure.real P (badScaleEvent Hshift t αbad q) ≤ ↑S.card * (Real.exp (-A ^ η) * weightedLinearExpKernelConst w (ρtop ^ τ)) + ↑(q + 1) * (Cbottom * w ^ q) * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρbottom ^ η)) + ↑(q + 1) * (↑S.card * w ^ q) * (Real.exp (-Acrude ^ η) * weightedGeometricExpKernelConst w (ρcrude ^ σ))
Same synchronized component-sum bound after selecting the common denominator that dominates both raw branch denominators.
theorem
HCPolySupport.Book.Ch05.Section57.badScaleProbability_le_interpolatedSum_selectedDenominator_annealedExponent
{d : ℕ}
[NeZero d]
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (Centry : ℝ) (a : ℝ),
0 < Centry ∧ 0 < a ∧ ∀ {σ : ℝ},
0 < σ →
∃ (Cfluct : ℝ) (Ccrude : ℝ),
0 < Cfluct ∧ 0 < Ccrude ∧ ∀ {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 ctop :=
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 Dcrude := K * Ccrude * hΓ.thetaHat ^ 2;
have Den := mixedBottomTailDenominator Dhigh Dcrude η τ σ;
have A := 3 ^ (↑q - τ * b * (L + 1) / η) / Den;
have Acrude := 3 ^ (↑q - σ * t * (L + 1) / η) / Den;
have ρtop := 3 ^ ctop;
have ρbottom := 3 ^ (τ * (t - αbad) / η);
have ρcrude := 3 ^ (t - αbad);
have Cbottom := Real.exp 1 * max 1 ↑S.card;
0 < t →
t ≤ b →
0 ≤ αbad →
αbad < t →
αbad < b →
αbad * (1 + b / a) < b →
αbad < a →
1 ≤ A →
1 ≤ Acrude →
(have Lcut := (a * Real.log 3)⁻¹ * Real.log (max (2 * K) 1);
Lcut + 1 < (1 - αbad / a) * ↑q) →
MeasureTheory.Measure.real P (badScaleEvent Hshift t αbad q) ≤ ↑S.card * (Real.exp (-A ^ η) * weightedLinearExpKernelConst w (ρtop ^ τ)) + ↑(q + 1) * (Cbottom * w ^ q) * (Real.exp (-A ^ η) * weightedGeometricExpKernelConst w (ρbottom ^ η)) + ↑(q + 1) * (↑S.card * w ^ q) * (Real.exp (-Acrude ^ η) * weightedGeometricExpKernelConst w (ρcrude ^ σ))
Uniform-in-σ selected-denominator component-sum bound.