Equation (10.56): eventual strict scalar absorption #

theorem Section10Equation1056ScalarAbsorption.kappaOneLogSlope_antitoneOn :

AntitoneOn Section10Equation1053NonCircular.kappaOneLogSlope (Set.Ici 2)

Inspect dependencies

Section10Equation1056ScalarAbsorption.kappaOneLogSlope_antitoneOn · compiled type and proof/definition references.

theorem Section10Equation1056ScalarAbsorption.psiMinus_kappaOne_hasDerivAt_local {c s : ℝ} (hs : 1 ≤ s) :

HasDerivAt (Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus Section10CanonicalXi.xi c) (Section10CanonicalXi.xi s - c - Section10Equation1053NonCircular.kappaOneLogSlope s) s

Inspect dependencies

Section10Equation1056ScalarAbsorption.psiMinus_kappaOne_hasDerivAt_local · compiled type and proof/definition references.

source

theorem Section10Equation1056ScalarAbsorption.psiMinus_secant_lower {c s t : ℝ} (hs : 3 ≤ s) (ht : t ∈ Set.Icc (s - 1) s) :

(Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)) * (t - (s - 1)) ≤ Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus Section10CanonicalXi.xi c t - Section10Equation1053.psiMinus Section10Equation1053NonCircular.explicitKappaOneAdjointPlus Section10CanonicalXi.xi c (s - 1)

Inspect dependencies

Section10Equation1056ScalarAbsorption.psiMinus_secant_lower · compiled type and proof/definition references.

source

theorem Section10Equation1056ScalarAbsorption.normalized_kernel_le {c s : ℝ} (hs : 3 ≤ s) (hm : 0 < Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)) :

Inspect dependencies

Section10Equation1056ScalarAbsorption.normalized_kernel_le · compiled type and proof/definition references.

source

theorem Section10Equation1056ScalarAbsorption.scalar_absorption_of_elementary_bounds {c s : ℝ} (hs : 3 ≤ s) (hm : 0 < Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)) (hA : 0 < Section10CanonicalXi.xi s - c - 2 / s) (hgap : Section10CanonicalXi.xi s - c - 2 / s - (Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)) < (Section10CanonicalXi.xi s - c - 2 / s) * Real.exp (-(Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)))) :

Section10Equation1053KernelExpansion.Equation1053EarliestScalarInequality Section10CanonicalXi.xi c s

Inspect dependencies

Section10Equation1056ScalarAbsorption.scalar_absorption_of_elementary_bounds · compiled type and proof/definition references.

source

theorem Section10Equation1056ScalarAbsorption.xi_nonneg (s : ℝ) :

0 ≤ Section10CanonicalXi.xi s

Inspect dependencies

Section10Equation1056ScalarAbsorption.xi_nonneg · compiled type and proof/definition references.

source

theorem Section10Equation1056ScalarAbsorption.xi_tendsto_atTop_local :

Filter.Tendsto Section10CanonicalXi.xi Filter.atTop Filter.atTop

Inspect dependencies

Section10Equation1056ScalarAbsorption.xi_tendsto_atTop_local · compiled type and proof/definition references.

source

theorem Section10Equation1056ScalarAbsorption.xi_unit_increment_le {s : ℝ} (hs : 4 ≤ s) (hx : 2 ≤ Section10CanonicalXi.xi (s - 1)) :

Section10CanonicalXi.xi s - Section10CanonicalXi.xi (s - 1) ≤ 2 / (s - 1)

Inspect dependencies

Section10Equation1056ScalarAbsorption.xi_unit_increment_le · compiled type and proof/definition references.

source

theorem Section10Equation1056ScalarAbsorption.kappaOneLogSlope_nonneg {u : ℝ} (hu : 2 ≤ u) :

0 ≤ Section10Equation1053NonCircular.kappaOneLogSlope u

Inspect dependencies

Section10Equation1056ScalarAbsorption.kappaOneLogSlope_nonneg · compiled type and proof/definition references.

source

theorem Section10Equation1056ScalarAbsorption.kappaOneLogSlope_le_three_div {u : ℝ} (hu : 2 ≤ u) :

Section10Equation1053NonCircular.kappaOneLogSlope u ≤ 3 / u

Inspect dependencies

Section10Equation1056ScalarAbsorption.kappaOneLogSlope_le_three_div · compiled type and proof/definition references.

source

theorem Section10Equation1056ScalarAbsorption.eventual_elementary_absorption (c : ℝ) (hc : 1152 ≤ c) :

∃ (S : ℝ), ∀ (s : ℝ), S ≤ s → 3 ≤ s ∧ 0 < Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1) ∧ 0 < Section10CanonicalXi.xi s - c - 2 / s ∧ Section10CanonicalXi.xi s - c - 2 / s - (Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)) < (Section10CanonicalXi.xi s - c - 2 / s) * Real.exp (-(Section10CanonicalXi.xi (s - 1) - c - Section10Equation1053NonCircular.kappaOneLogSlope (s - 1)))

Inspect dependencies

Section10Equation1056ScalarAbsorption.eventual_elementary_absorption · compiled type and proof/definition references.

source

theorem Section10Equation1056ScalarAbsorption.equation1056_eventually_strict (c : ℝ) (hc : 1152 ≤ c) :

∃ (S : ℝ), ∀ (s : ℝ), S ≤ s → Section10Equation1053KernelExpansion.Equation1053EarliestScalarInequality Section10CanonicalXi.xi c s

Final source-(10.56) scalar absorption: for every fixed c ≥ 1152, the canonical ξ makes the normalized scalar product strictly less than one for all sufficiently large s.

Inspect dependencies

Section10Equation1056ScalarAbsorption.equation1056_eventually_strict · compiled type and proof/definition references.

source

theorem Section10Equation1056ScalarAbsorption.equation1056_eventually_contradiction (c : ℝ) (hc : 1152 ≤ c) :

∃ (S : ℝ), ∀ (s : ℝ), S ≤ s → 1 ≤ Section10Equation1053KernelExpansion.equation1056ScalarRatio Section10CanonicalXi.xi c s → False

The literal final contradiction in (10.56): the source-side lower bound 1 ≤ ratio is incompatible with the eventual strict absorption.

Inspect dependencies

Section10Equation1056ScalarAbsorption.equation1056_eventually_contradiction · compiled type and proof/definition references.

Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiEquation1056ScalarAbsorption

Equation (10.56): eventual strict scalar absorption #