Lemma 14.4: the even Σ₁₁ endpoint #
At even depth M, the predecessor depth M-1 is odd. Its source domain is
open at 1, but the κ=1 layers are regular on the closed envelope. We use that
closed-envelope regularity only to run Lemma 8.7 and the finite recursion at the
endpoint. The prime carrier itself is strict, so no prime coordinate is added.
theorem
MathlibNt.SieveTheory.finiteSourceLayer_continuousOn_closedDomain
{β : ℝ}
(hβ : 1 < β)
(N : ℕ)
:
Finite source layers are continuous on the closed parity domain for beta > 1.
theorem
MathlibNt.SieveTheory.sigma11_finiteSourceLayer_lemma8_7_even_endpoint
{S : BoundingSieve}
{D z v w σ K : ℝ}
{M : ℕ}
(hM : Even M)
(hM2 : 2 ≤ M)
(hσ : 2 ≤ σ)
(hD : 1 < D)
(hz2 : 2 ≤ z)
(hv2 : 2 ≤ v)
(hw2 : 2 ≤ w)
(hwv : w ≤ v)
(hvz : v ≤ z)
(hz : z = D ^ (1 / 2))
(hv : v = D ^ (1 / 2))
(hw : w = D ^ (1 / σ))
(hK : 2 ≤ K)
(hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K)
:
(SwitchingPrinciple.suzukiLemmaEightSevenPrimeSum S D w v z fun (t : ℝ) =>
SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) (t - 1)) ≤ (1 / 2 * ∫ (t : ℝ) in 2..σ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) (t - 1)) + 6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (M - 1) 1 / Real.log w
Lemma 8.7 at s=τ=2, using closed-envelope regularity at the one
formal boundary point. Its prime sum remains on the original strict carrier.
theorem
MathlibNt.SieveTheory.caseI_evenEndpointSigma11Edge
(S : BoundingSieve)
{M D : ℕ}
{K σ : ℝ}
(hM : Even M)
(hM2 : 2 ≤ M)
(hσ : 2 ≤ σ)
(hD : 1 < ↑D)
(hroot2 : 2 ≤ ↑D ^ (1 / 2))
(hw2 : 2 ≤ ↑D ^ (1 / σ))
(hwroot : ↑D ^ (1 / σ) ≤ ↑D ^ (1 / 2))
(hK : 2 ≤ K)
(hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K)
:
CaseIEvenEndpointSigma11Edge S M D K σ
Production closure of the even Case-I Σ₁₁ endpoint, with no predecessor
open-domain hypothesis.