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.

theorem MathlibNt.SieveTheory.endpoint_sigma11_core (V K F logD σ L R logσ E0 logPow logLog C E : ℝ) (hlog : 0 < logD) (hσ : 0 < σ) (hC : 0 < C) (hE : 0 < E) (hll : 0 < logLog) (hV : 0 ≤ V) (hL : 0 ≤ L) (hR : 0 ≤ R) (hE0 : 0 ≤ E0) (htransport : F ≤ L * R * (σ * logσ) * E0) (hnorm : K ^ 2 * σ ^ 2 * logσ / logD ≤ logPow / (logLog * σ)) : V * (6 * K ^ 2 * F / (logD / σ)) ≤ 6 * L * R / (C * E) * (C * E * V * logPow * E0 / (logLog * σ))

Transport and normalize the sigma-eleven scalar estimate into its budget.

theorem MathlibNt.SieveTheory.caseI1423_endpoint_sigma11_bound (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ L R : ℝ) (N D : ℕ) (s : ℝ) (hC : 0 < C) (hD : 0 < ↑D) (hlog : 0 < Real.log ↑D) (hll : 0 < Real.log (Real.log ↑D)) (hσ0 : 0 < SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) (hL : 0 ≤ L) (hR : 0 ≤ R) (hE0 : 0 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s) (htransport : SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (s - 1) ≤ L * R * (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d * Real.log (Real.exp 1 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)) * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s) (hscalarMul : K ^ 2 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ^ 3 * Real.log (Real.exp 1 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) * Real.log (Real.log ↑D) ≤ Real.log ↑D ^ (1 - Δ)) (hpowe : Real.log ↑D ^ (-Δ) * Real.log ↑D = Real.log ↑D ^ (1 - Δ)) : caseI1423Sigma11Endpoint S N D ⌈↑D ^ (1 / s)⌉₊ K s (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ 6 * L * R / (C * Real.exp √K) * caseI1423RemainderUnit (sigma12InheritedBudget S H N D ⌈↑D ^ (1 / s)⌉₊ C K d Δ s) (↑D) (SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)

Pointwise sigma-eleven endpoint bound from transport and scalar estimates.

theorem MathlibNt.SieveTheory.caseI1423_endpoint_sigma12_final_algebra (q V K R σ logσ E0 logLog logD : ℝ) (hR : 0 ≤ R) (hσ : 0 < σ) (hE0 : 0 ≤ E0) (hV : 0 ≤ V) (hLogLog : 0 ≤ logLog) (hfront : V * q ≤ V * 2 * R * σ * logσ * E0) (hscalar : K ^ 2 * σ ^ 3 * logσ * logLog ≤ logD) : q * σ * V * 6 * K ^ 2 * logLog ≤ R * E0 * V * logD * 12 / σ

Convert the sigma-twelve front estimate and scalar bound into the final budget.

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

Honest endpoint-source statement. Both constants precede N and s; the pointwise hypotheses are exactly the Case-I source window.

Equations

• MathlibNt.SieveTheory.CaseI1423EndpointSourceBoundsFinal S H C K d Δ = ∃ (A11 : ℝ) (A12 : ℝ), 0 ≤ A11 ∧ 0 ≤ A12 ∧ ∀ (N : ℕ) (s : ℝ), 2 ≤ N → 2 ≤ s → s - 1 ∈ MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → ∀ᶠ (D : ℕ) in Filter.atTop, 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.caseI1423EndpointSourceBoundsFinal (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) : CaseI1423EndpointSourceBoundsFinal S H C K d Δ

Closure of the two endpoint source bounds.