Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiLowerSieveFactorFirstInterval

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.

source
noncomputable def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude :
ℝ

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

Equations
Instances For
    source
    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
    Instances For
      source
      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.

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

      The source amplitude is strictly positive.

      source
      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.

      source
      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.

      source
      @[simp]
      theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_one_one_two_eq_zero_of_three_le {s : ℝ} (hs : 3 ≤ s) :
      suzukiLayer 1 2 1 s = 0
      source
      @[simp]
      theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_two_one_two_eq_zero_of_four_le {s : ℝ} (hs : 4 ≤ s) :
      suzukiLayer 1 2 2 s = 0
      source
      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.

      source
      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.

      source
      @[simp]
      theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval_two :
      suzukiLowerSieveFactorFirstInterval 2 = 0
      source
      theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval_pos {s : ℝ} (hs₂ : 2 < s) (hs₄ : s ≤ 4) :
      0 < suzukiLowerSieveFactorFirstInterval s
      source
      theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLowerSieveFactorFirstInterval_eleven_fifths_pos :
      0 < suzukiLowerSieveFactorFirstInterval (11 / 5)