Suzuki Lemma 8.6 for the source-correct finite source layer

The normalized finite layer is only naturally continuous on its parity domain. A lower clamp gives a global continuous extension without changing any value on the source interval [s, σ] or at its prime coordinates.

noncomputable def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayerOneClamp (β : ℝ) (N : ℕ) (s t : ℝ) : ℝ

Global lower-clamped extension of a finite source layer.

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayerOneClamp β N s t = MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N (max s t)

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayerOneClamp_eq_of_le (β : ℝ) (N : ℕ) {s t : ℝ} (hst : s ≤ t) : finiteSourceLayerOneClamp β N s t = finiteSourceLayer 1 β N t

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayerOneClamp_continuous {β s : ℝ} (hβ : 1 < β) (N : ℕ) (hsdom : s ∈ suzukiParityDomainOne β N) : Continuous (finiteSourceLayerOneClamp β N s)

The clamp is globally continuous once its lower endpoint lies in the exact source parity domain.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayerOneClamp_nonneg_on_Icc {β s σ : ℝ} (hβ : 1 < β) (N : ℕ) (hsdom : s ∈ suzukiParityDomainOne β N) (t : ℝ) : t ∈ Set.Icc s σ → 0 ≤ finiteSourceLayerOneClamp β N s t

Nonnegativity of the clamped extension on the source interval.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayerOneClamp_weighted_antitoneOn_Icc {β s σ : ℝ} (hβ : 1 < β) (N : ℕ) (hsdom : s ∈ suzukiParityDomainOne β N) : AntitoneOn (fun (t : ℝ) => finiteSourceLayerOneClamp β N s t * t) (Set.Icc s σ)

Weighted antitonicity of the clamped extension on the unchanged interval.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLemmaEightSix_finiteSourceLayer {S : BoundingSieve} {D w z s σ K β : ℝ} {N : ℕ} (hβ : 1 < β) (hsdom : s ∈ SuzukiFiniteContinuousLayers.suzukiParityDomainOne β N) (hD : 1 < D) (hw2 : 2 ≤ w) (hs : 0 < s) (hsσ : s ≤ σ) (hz : z = D ^ (1 / s)) (hw : w = D ^ (1 / σ)) (hK : 0 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) : suzukiLemmaEightSixPrimeSum S D w z (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N) ≤ (1 / s * ∫ (t : ℝ) in s..σ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N t) + 2 * K * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s / Real.log w

Suzuki Lemma 8.6 specialized to the source-correct finite parity sum T_N. The clamp is eliminated from the public conclusion.