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)
:
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 ^ (-Δ))
Instances For
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)))
: