Suzuki's second lower interval and the Jurkat--Richert factor

This module isolates the analytic identification of Suzuki's source bracket on 4 ≤ s ≤ 6 with the production Jurkat--Richert kernel. The source amplitude is kept symbolic; identifying it with the standard dimension-one factor is explicitly conditional on A = 2 * exp γ.

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

The bracket produced by Suzuki's delay equation on the second lower interval, after separating its elementary and delayed terms.

Equations

• MathlibNt.SieveTheory.suzukiLowerSecondIntervalSourceKernel s = (Real.log 3 + ∫ (x : ℝ) in 4..s, (x - 1)⁻¹) + ∫ (x : ℝ) in 4..s, MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral (x - 1) / (x - 1)

noncomputable def MathlibNt.SieveTheory.suzukiLowerSecondIntervalSourceFactor (A s : ℝ) : ℝ

Suzuki's second-interval source factor with an abstract amplitude A.

Equations

• MathlibNt.SieveTheory.suzukiLowerSecondIntervalSourceFactor A s = A / s * MathlibNt.SieveTheory.suzukiLowerSecondIntervalSourceKernel s

theorem MathlibNt.SieveTheory.suzukiLowerSecondIntervalSourceKernel_eq_jurkatRichert {s : ℝ} (hs : 4 ≤ s) : suzukiLowerSecondIntervalSourceKernel s = Real.log (s - 1) + ∫ (u : ℝ) in 3..s - 1, SwitchingPrinciple.jurkatRichertInnerIntegral u / u

Unconditional analytic bridge: evaluate the elementary primitive and translate the delayed integral by u = x - 1.

theorem MathlibNt.SieveTheory.suzukiLowerSecondIntervalNestedBracket_eq_sourceKernel {s : ℝ} (hs₄ : 4 ≤ s) (hs₆ : s ≤ 6) : Real.log 3 + ∫ (x : ℝ) in 4..s, (x - 1)⁻¹ * (1 + ∫ (t : ℝ) in 2..x - 2, Real.log (t - 1) / t) = suzukiLowerSecondIntervalSourceKernel s

The literal nested bracket produced by the source module is the separated source kernel used by the analytic bridge.

theorem MathlibNt.SieveTheory.suzukiContinuousLowerFactor_eq_secondIntervalSourceFactor {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) {s : ℝ} (hs₄ : 4 ≤ s) (hs₆ : s ≤ 6) : suzukiContinuousLowerFactor s = suzukiLowerSecondIntervalSourceFactor SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude s

The actual production source formula, rather than a carried formula contract, feeds the separated analytic source factor.

theorem MathlibNt.SieveTheory.suzukiLowerSecondIntervalSourceFactor_eq_dimensionOne_conditional {A s : ℝ} (hA : A = 2 * Real.exp Real.eulerMascheroniConstant) (hs : 4 ≤ s) : suzukiLowerSecondIntervalSourceFactor A s = SwitchingPrinciple.dimensionOneLowerLinearSieveFactor s

Conditional amplitude-normalization bridge from Suzuki's source factor to the production dimension-one Jurkat--Richert lower factor.

theorem MathlibNt.SieveTheory.suzukiContinuousLowerFactor_eq_dimensionOne_conditional {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hA : SuzukiFiniteContinuousLayers.suzukiLowerSieveAmplitude = 2 * Real.exp Real.eulerMascheroniConstant) {s : ℝ} (hs₄ : 4 ≤ s) (hs₆ : s ≤ 6) : suzukiContinuousLowerFactor s = SwitchingPrinciple.dimensionOneLowerLinearSieveFactor s

On the second lower interval, the genuine production source factor equals the standard Jurkat--Richert factor, conditional only on amplitude normalization.