theorem MathlibNt.SieveTheory.caseIIPositiveDeltaIntegralPart_source_exact_relative (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N : ℕ} {D d Δ σ C K s : ℝ} (hD : 1 < D) (hs : 0 < s) (hC : 0 ≤ C) (hK : 0 ≤ K) (hcut : 0 ≤ (1 - 1 / σ) ^ (1 - Δ)) (hiii : ∫ (t : ℝ) in 3..σ, SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite D d Δ t ≤ (1 - 1 / σ) ^ (1 - Δ) * SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) D d 0 3) (hcubic : SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) D d 0 3 ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation D d 0 3 * SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) D d 0 s) : caseIIPositiveDeltaIntegralPart H N D (D ^ (1 / 3)) d Δ σ C K s ≤ C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d s * Real.log D ^ (-Δ) * ((1 + 3 * K / Real.log D) * (1 - 1 / σ) ^ (1 - Δ) * SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation D d 0 3)

At the exact source point y = D^(1/3), the integral contribution pays both the cubic lambda comparison and the product-ratio excess.

theorem MathlibNt.SieveTheory.perturbation_three_le_one_add_seven_ratio {D d : ℝ} (hlog : 0 < Real.log D) (_hd : 0 ≤ d) (hsmall : 3 ^ d ≤ Real.log D) : SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation D d 0 3 ≤ 1 + 7 * (3 ^ d / Real.log D)

The cubic perturbation has linear excess when 3^d is at most log D.

theorem MathlibNt.SieveTheory.exists_integral_transport_relative_excess_threshold (Δ d K : ℝ) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hd : 7 / (1 - Δ) < d) (hK : 0 ≤ K) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → (1 + 3 * K / Real.log D) * (1 - 1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) ^ (1 - Δ) * SwitchingPrinciple.SuzukiLemma144KappaOne.perturbation D d 0 3 - (1 - 1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) ^ (1 - Δ) ≤ (1 - Δ) / (32 * SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d)

Eventually the transported relative integral coefficient pays both the cubic perturbation and the local product-ratio excess.