Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiContinuousLowerFactorSecondInterval

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.

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

The genuine even source tail T⁻.

Equations
Instances For
    Inspect dependencies

    MathlibNt.SieveTheory.suzukiContinuousLowerTail · compiled type and proof/definition references.

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

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

    Equations
    Instances For
      Inspect dependencies

      MathlibNt.SieveTheory.suzukiContinuousLowerFactor · compiled type and proof/definition references.

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

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

      Equations
      Instances For
        Inspect dependencies

        MathlibNt.SieveTheory.suzukiContinuousUpperFactor · compiled type and proof/definition references.

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

        Inspect dependencies

        MathlibNt.SieveTheory.suzukiLowerSieveAmplitude_eq_three_mul_upperFactor · compiled type and proof/definition references.

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

        Inspect dependencies

        MathlibNt.SieveTheory.suzukiContinuousUpperFactor_eq_second_source_formula · compiled type and proof/definition references.

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

        Inspect dependencies

        MathlibNt.SieveTheory.suzukiContinuousLowerFactor_eq_second_source_formula · compiled type and proof/definition references.