theorem
MathlibNt.SieveTheory.caseI_total_le_concrete_finiteSourceLayer_add_qD
(S : BoundingSieve)
(H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers)
{N D z : ℕ}
{β σ s C C1 K ΘK Δ d B0 : ℝ}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H β)
(hN2 : 2 ≤ N)
(hbase : Odd N → suzukiSourceV S 1 D z = 0)
(hcube : ∀ n ∈ sourceParityIndices N, 2 ≤ n → Odd n → ∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, p ^ 3 < D)
(hdom : CaseIThreeRangeDomain D z σ s)
(hcaseITau : caseITau (↑D) s = s)
(hz : ↑D ^ (1 / s) = ↑z)
(hcaseI : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5CaseI β N s σ)
(hEndpoint :
SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_5Regime β (↑D) σ C1 K ΘK σ →
∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S ⌈↑D ^ (1 / σ)⌉₊,
S.nu p * ∑ m ∈ sourceParityIndices (N - 1), suzukiSourceV S m (D ⌈/⌉ p) p ≤ B0)
(hnu :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s,
0 ≤ S.nu p)
(hC : 0 ≤ C)
(hlog :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s,
0 ≤ Real.log ↑(D ⌈/⌉ p))
(hSourceDomain :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s,
SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1) ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1))
(hClaim14_6_i :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s,
SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneLambdaPremise H (↑(D ⌈/⌉ p)) d σ)
(hErrorDomain :
∀
p ∈
SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier (SwitchingPrinciple.suzukiSupportedBelow S z) D σ s,
SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p ∈ Set.Icc (H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)).epsilon) σ ∧ SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate D p ∈ Set.Icc (H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)).epsilon) σ)
(hIH :
SwitchingPrinciple.SuzukiLemma144Equation1410.NaturalCeilPointwiseInductionContract
(SwitchingPrinciple.suzukiSupportedBelow S z)
(fun (n D' p : ℕ) => ∑ m ∈ sourceParityIndices n, suzukiSourceV S m D' p)
(fun (p : ℕ) => SwitchingPrinciple.suzukiVProduct S ↑p)
(fun (n D' : ℕ) (x : ℝ) => SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D') d x) β C K Δ N D σ s)
(hsdom : s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β N)
(hsm1dom : s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1))
(hD : 1 < ↑D)
(hz2 : 2 ≤ ↑z)
(hv2 : 2 ≤ ↑D ^ (1 / s))
(hw2 : 2 ≤ ↑D ^ (1 / σ))
(hwv : ↑D ^ (1 / σ) ≤ ↑D ^ (1 / s))
(hvz : ↑D ^ (1 / s) ≤ ↑z)
(hErrorThreshold : H.betaHat + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon < s)
(hK : 2 ≤ K)
(hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K)
(hClaim14_6_ii : SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_6_MonotoneQPremise H (↑D) d Δ σ)
(hΔ : 0 ≤ Δ)
(hCeilFull : ∀ p ∈ S.prodPrimes.primeFactors, ↑D ^ (1 / σ) ≤ ↑p → ↑p < ↑D ^ (1 / s) → 2 ≤ p ∧ 2 * p ≤ D)
(hT :
∀ p ∈ S.prodPrimes.primeFactors,
↑D ^ (1 / σ) ≤ ↑p →
↑p < ↑D ^ (1 / s) →
0 ≤ H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1))
(SwitchingPrinciple.SuzukiLemma144Equation1410.inheritedCoordinate D p))
(hClaim14_13 :
∀ p ∈ S.prodPrimes.primeFactors,
↑D ^ (1 / σ) ≤ ↑p →
↑p < ↑D ^ (1 / s) →
SwitchingPrinciple.SuzukiLemma144KappaOne.Claim14_13PointwisePremise H N (↑D) d Δ (Real.log ↑D / Real.log ↑p)
(↑D / ↑p))
:
∑ n ∈ sourceParityIndices N, suzukiSourceV S n D z ≤ B0 + (SwitchingPrinciple.suzukiVProduct S ↑z * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s + 6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (s - 1) / Real.log (↑D ^ (1 / σ)) * (s / s)) + C * Real.exp √K * SwitchingPrinciple.suzukiVProduct S ↑z * Real.log ↑D ^ (-Δ) * ((1 / s * ∫ (t : ℝ) in s..σ, SwitchingPrinciple.SuzukiLemma144KappaOne.qD H
(SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ t) + 6 * K ^ 2 * SwitchingPrinciple.SuzukiLemma144KappaOne.qD H
(SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (↑D) d Δ s / Real.log (↑D ^ (1 / σ)) * (s / s)))
Final concrete finite Case-I assembly. The total source inequality is
specialized to Suzuki's Euler product, while the exact carrier equality moves
the full-support sigmaTwelve estimate onto the supported carrier required by
the recurrence assembly.