Case I, (14.23): endpoint source bounds

The published predicate CaseI1423EndpointSourceBounds omits the source hypotheses (and even quantifies over C = 0), so it is not a valid unconditional statement. This file proves the source-faithful version used in Case I. The source bounds are imported from their proved production producers. In particular, neither endpoint inequality is assumed in this module.

def MathlibNt.SieveTheory.CaseI1423EndpointSourceBoundsUniform (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) : Prop

Honest endpoint-source statement with a D threshold uniform in N and s. Both constants and the eventual threshold precede the pointwise Case-I source-window hypotheses.

Equations

• MathlibNt.SieveTheory.CaseI1423EndpointSourceBoundsUniform S H C K d Δ = ∃ (A11 : ℝ) (A12 : ℝ), 0 ≤ A11 ∧ 0 ≤ A12 ∧ ∀ᶠ (D : ℕ) in Filter.atTop, ∀ (N : ℕ) (s : ℝ), 2 ≤ N → 2 ≤ s → s - 1 ∈ MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → s ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → have σ := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; have z := ⌈↑D ^ (1 / s)⌉₊; have B := MathlibNt.SieveTheory.sigma12InheritedBudget S H N D z C K d Δ s; MathlibNt.SieveTheory.caseI1423Sigma11Endpoint S N D z K s σ ≤ A11 * MathlibNt.SieveTheory.caseI1423RemainderUnit B (↑D) σ ∧ MathlibNt.SieveTheory.caseI1423Sigma12Endpoint S H N D z C K d Δ s σ ≤ A12 * MathlibNt.SieveTheory.caseI1423RemainderUnit B (↑D) σ

theorem MathlibNt.SieveTheory.caseI1423EndpointSourceBoundsUniform (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hC : 0 < C) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) : CaseI1423EndpointSourceBoundsUniform S H C K d Δ

Closure of the two endpoint source bounds.