Case-I endpoint consumer under the source parameter packet #
This endpoint consumer discharges the literal (14.23) scalar with the sharpened
uniform theorem. Its assumptions are exactly Suzuki's source packet, rather
than the stronger artificial condition
7 / (1 - (Δ + 2 / Θ)) < d.
theorem
MathlibNt.SieveTheory.exists_caseI1423EndpointSourceBounds_sourceLargeLog_uniform_of_source
(S : BoundingSieve)
(H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers)
{d Δ Θ : ℝ}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H)
(hsrc : SuzukiClaim145SourceParameters d Δ Θ)
:
∃ (C1min : ℝ),
1 ≤ C1min ∧ ∀ (C1 C K : ℝ),
C1min ≤ C1 →
0 < C →
2 ≤ K →
∃ (A11 : ℝ) (A12 : ℝ),
0 ≤ A11 ∧ 0 ≤ A12 ∧ ∀ (N D : ℕ) (s : ℝ),
3 ≤ D →
C1 * K ^ Θ < Real.log ↑D →
2 ≤ N →
2 ≤ s →
s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) →
s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d →
have σ := SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d;
have z := ⌈↑D ^ (1 / s)⌉₊;
have B := sigma12InheritedBudget S H N D z C K d Δ s;
caseI1423Sigma11Endpoint S N D z K s σ ≤ A11 * caseI1423RemainderUnit B (↑D) σ ∧ caseI1423Sigma12Endpoint S H N D z C K d Δ s σ ≤ A12 * caseI1423RemainderUnit B (↑D) σ
Source-large-log endpoint bounds with the cutoff before C, K, depth, and
coordinate, under exactly the source parameter packet.