The genuine continuous mass of the ordinary Rosser producer

The Suzuki parity series, not the Section-13 hats, are F - 1 and 1 - f. The amplitude comes from the admitted adjoint pairing. The identification extends from the initial intervals by the integral method of steps, with no upper bound on the sieve coordinate or on the finite source depth.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.sourceTPlus_eq_jr1965F_sub_one_initial {s : ℝ} (hs1 : 1 < s) (hs3 : s ≤ 3) : suzukiProposition118SourceTPlus s = JurkatRichert1965ChenGammaOneQOne.jr1965F s - 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.sourceTMinus_eq_one_sub_jr1965f_initial {s : ℝ} (hs2 : 2 ≤ s) (hs4 : s ≤ 4) : suzukiProposition118SourceTMinus s = 1 - JurkatRichert1965ChenGammaOneQOne.jr1965f s

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.sourceParity_eq_jr1965 {s : ℝ} (hs : 2 ≤ s) : suzukiProposition118SourceTPlus s = JurkatRichert1965ChenGammaOneQOne.jr1965F s - 1 ∧ suzukiProposition118SourceTMinus s = 1 - JurkatRichert1965ChenGammaOneQOne.jr1965f s

The exact full continuous masses. In particular neither mass is a JR hat.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.finiteSourceLayer_odd_le_jr1965F_sub_one (m : ℕ) {s : ℝ} (hs : 2 ≤ s) : SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (2 * m + 1) s ≤ JurkatRichert1965ChenGammaOneQOne.jr1965F s - 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.CoarseDensity.finiteSourceLayer_even_le_one_sub_jr1965f (m : ℕ) {s : ℝ} (hs : 2 ≤ s) : SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (2 * m) s ≤ 1 - JurkatRichert1965ChenGammaOneQOne.jr1965f s