Suzuki's continuous lower factor on the second interval

The factors here are the genuine Proposition 11.8 source series. The source integral identities and the already proved first lower interval determine the upper factor on [3,5] and then the lower factor on [4,6]. Suzuki's source amplitude remains symbolic throughout.

noncomputable def MathlibNt.SieveTheory.suzukiContinuousLowerTail (s : ℝ) : ℝ

The genuine even source tail T⁻.

Equations

• MathlibNt.SieveTheory.suzukiContinuousLowerTail s = MathlibNt.SieveTheory.suzukiProposition118SourceTMinus s

noncomputable def MathlibNt.SieveTheory.suzukiContinuousLowerFactor (s : ℝ) : ℝ

The continuous lower factor F⁻ = 1 - T⁻.

Equations

• MathlibNt.SieveTheory.suzukiContinuousLowerFactor s = 1 - MathlibNt.SieveTheory.suzukiContinuousLowerTail s

noncomputable def MathlibNt.SieveTheory.suzukiContinuousUpperFactor (s : ℝ) : ℝ

The continuous upper factor F⁺ = 1 + T⁺.

Equations

• MathlibNt.SieveTheory.suzukiContinuousUpperFactor s = 1 + MathlibNt.SieveTheory.suzukiProposition118SourceTPlus s

theorem MathlibNt.SieveTheory.suzukiLowerSieveAmplitude_eq_three_mul_upperFactor : SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude = 3 * suzukiContinuousUpperFactor 3

The source amplitude is the weighted upper factor at the first upper endpoint.

theorem MathlibNt.SieveTheory.suzukiContinuousUpperFactor_eq_second_source_formula {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {u : ℝ} (hu₃ : 3 ≤ u) (hu₅ : u ≤ 5) : suzukiContinuousUpperFactor u = SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude / u * (1 + ∫ (t : ℝ) in 2..u - 1, Real.log (t - 1) / t)

The production source identity and the first lower interval give the explicit upper factor on 3 ≤ u ≤ 5.

theorem MathlibNt.SieveTheory.suzukiContinuousLowerFactor_eq_second_source_formula {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs₄ : 4 ≤ s) (hs₆ : s ≤ 6) : suzukiContinuousLowerFactor s = SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude / s * (Real.log 3 + ∫ (x : ℝ) in 4..s, (x - 1)⁻¹ * (1 + ∫ (t : ℝ) in 2..x - 2, Real.log (t - 1) / t))

Suzuki's explicit second lower interval, with the genuine source amplitude kept symbolic.