Suzuki's source lower factor on its first explicit interval

This module specializes Suzuki §9 to κ = 1, β = 2. Suzuki (9.5) and the paragraph following it define T⁺ as the odd limiting layer sum and F⁻ = 1 - T⁻. Proposition 9.4(vii)--(viii), with the Section 15.2 normalization B = 0, gives on the first lower interval 2 ≤ s ≤ 4

F⁻(s) = (A / s) ∫ t in 2..s, 1 / (t - 1),

where A = 3 * T⁺(3) + 3. The definition below records this source formula; its identification with 1 - T⁻ remains a separate theorem obligation. It is independent of the nonstandard placeholder LinearSieve.sieveFunctionf.

noncomputable def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude : ℝ

Suzuki's constant A at κ = 1, β = 2, written in terms of his odd normalized source layers.

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude = 3 * (1 + ∑' (k : ℕ), MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * k + 1) 3)

noncomputable def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval (s : ℝ) : ℝ

The source formula for the lower limiting factor on its first interval. Identification with the even-layer limit is intentionally not asserted here.

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval s = MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude / s * ∫ (t : ℝ) in 2..s, (t - 1)⁻¹

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzuki_oddLayer_at_three_nonneg (k : ℕ) : 0 ≤ suzukiLayer 1 2 (2 * k + 1) 3

Every odd layer entering Suzuki's amplitude is nonnegative.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude_pos : 0 < suzukiLowerSieveAmplitude

The source amplitude is strictly positive.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_one_one_two {s : ℝ} (hs₀ : 0 < s) (hs₃ : s ≤ 3) : suzukiLayer 1 2 1 s = (3 - s) / s

Direct evaluation of (9.1) at κ = 1, β = 2.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_two_one_two {s : ℝ} (hs₂ : 2 ≤ s) (hs₄ : s ≤ 4) : suzukiLayer 1 2 2 s = s⁻¹ * ∫ (t : ℝ) in s..4, (4 - t) / (t - 1)

Direct specialization of (9.2) for the first even layer.

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_one_one_two_eq_zero_of_three_le {s : ℝ} (hs : 3 ≤ s) : suzukiLayer 1 2 1 s = 0

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_two_one_two_eq_zero_of_four_le {s : ℝ} (hs : 4 ≤ s) : suzukiLayer 1 2 2 s = 0

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.integral_inv_sub_one_two {s : ℝ} (hs : 2 ≤ s) : ∫ (t : ℝ) in 2..s, (t - 1)⁻¹ = Real.log (s - 1)

The elementary integral in Suzuki's first lower interval.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval_eq_log {s : ℝ} (hs₂ : 2 ≤ s) (_hs₄ : s ≤ 4) : suzukiLowerSieveFactorFirstInterval s = suzukiLowerSieveAmplitude * Real.log (s - 1) / s

Suzuki's explicit first-interval formula, with both source endpoints exact.

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval_two : suzukiLowerSieveFactorFirstInterval 2 = 0

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval_pos {s : ℝ} (hs₂ : 2 < s) (hs₄ : s ≤ 4) : 0 < suzukiLowerSieveFactorFirstInterval s

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval_eleven_fifths_pos : 0 < suzukiLowerSieveFactorFirstInterval (11 / 5)