theorem MathlibNt.SieveTheory.lemma14_4_caseII_total_sameC_eventually_at_sourceSigma {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {B₀ : ℕ → ℕ → ℝ} {N : ℕ} {d Δ C K s : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hd1 : 1 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hC : 0 < C) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hs1 : 1 < s) (hs3 : s ≤ 3) (hrelative : Lemma144CaseIIOddRoundedRelativeProducer S H B₀ d Δ C K) (hnormalize : Lemma144CaseIIOddEndpointGapNormalization S H B₀ d Δ C K) (hD : ∀ᶠ (D : ℕ) in Filter.atTop, 1 < ↑D) (hdom : s ∈ SuzukiFiniteContinuousLayers.suzukiParityDomainOne 2 N) (hroot2 : ∀ᶠ (D : ℕ) in Filter.atTop, 2 ≤ ↑D ^ (1 / s)) (hN : Odd N) : Lemma144CaseIISameCEventuallyAtSourceSigma S H N d Δ C K s

def MathlibNt.SieveTheory.Lemma144UniformNatCeilRestrictedAt (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (N Dmin : ℕ) (Q : ℝ → Prop) : Prop

Equations

• MathlibNt.SieveTheory.Lemma144UniformNatCeilRestrictedAt S H C K d Δ N Dmin Q = ∀ (D : ℕ), Dmin ≤ D → 2 ≤ D → ∀ x ∈ MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N, Q x → 2 ≤ ⌈↑D ^ (1 / x)⌉₊ → MathlibNt.SieveTheory.suzukiActualT S N D ⌈↑D ^ (1 / x)⌉₊ ≤ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / x)⌉₊ * (MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N x + C * Real.exp √K * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d x * Real.log ↑D ^ (-Δ))

theorem MathlibNt.SieveTheory.lemma144UniformNatCeilAt_of_restricted_cases {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {C K d Δ : ℝ} {N DI DII : ℕ} {QI QII : ℝ → Prop} (hcover : ∀ x ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N, QI x ∨ QII x) (hI : Lemma144UniformNatCeilRestrictedAt S H C K d Δ N DI QI) (hII : Lemma144UniformNatCeilRestrictedAt S H C K d Δ N DII QII) : Lemma144UniformNatCeilAt S H C K d Δ N (max DI DII)

theorem MathlibNt.SieveTheory.lemma14_4_full_finiteDepth_final (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (depth : ℕ) (QI QII : ℕ → ℝ → Prop) (hcover : ∀ (M : ℕ), ∀ x ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 M, QI M x ∨ QII M x) (hbase : ∃ (Dmin : ℕ), 2 ≤ Dmin ∧ Lemma144UniformNatCeilAt S H C K d Δ 1 Dmin) (hcaseI : ∀ (N Dmin : ℕ), 1 ≤ N → N < depth → 2 ≤ Dmin → Lemma144GlobalDepthAt S H C K d Δ N Dmin → ∃ (DI : ℕ), Dmin ≤ DI ∧ Lemma144UniformNatCeilRestrictedAt S H C K d Δ (N + 1) DI (QI (N + 1))) (hcaseII : ∀ (N Dmin : ℕ), 1 ≤ N → N < depth → 2 ≤ Dmin → Lemma144GlobalDepthAt S H C K d Δ N Dmin → ∃ (DII : ℕ), Dmin ≤ DII ∧ Lemma144UniformNatCeilRestrictedAt S H C K d Δ (N + 1) DII (QII (N + 1))) : ∃ (Dmin : ℕ), 2 ≤ Dmin ∧ ∀ (N : ℕ), 1 ≤ N → N ≤ depth → Lemma144GlobalDepthAt S H C K d Δ N Dmin