noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.finiteSourceLayerShiftClamp (β : ℝ) (M : ℕ) (τ t : ℝ) : ℝ

Global continuous extension of t ↦ T_M(t-1), clamped at the left source coordinate τ-1.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.finiteSourceLayerShiftClamp β M τ t = MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayerOneClamp β M (τ - 1) (t - 1)

@[simp]

theorem MathlibNt.SieveTheory.SwitchingPrinciple.finiteSourceLayerShiftClamp_eq_of_le (β : ℝ) (M : ℕ) {τ t : ℝ} (hτt : τ ≤ t) : finiteSourceLayerShiftClamp β M τ t = SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β M (t - 1)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.finiteSourceLayerShiftClamp_lemmaEightSeven_conditions {β τ σ : ℝ} (hβ : 1 < β) (M : ℕ) (hτdom : τ - 1 ∈ SuzukiFiniteContinuousLayers.suzukiParityDomainOne β M) (_hτσ : τ ≤ σ) : Continuous (finiteSourceLayerShiftClamp β M τ) ∧ (∀ t ∈ Set.Icc τ σ, 0 ≤ finiteSourceLayerShiftClamp β M τ t) ∧ AntitoneOn (fun (t : ℝ) => finiteSourceLayerShiftClamp β M τ t * t) (Set.Icc τ σ)

The shifted clamp supplies exactly the global continuity, nonnegativity, and t H(t) antitonicity required by Lemma 8.7.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLemmaEightSeven_finiteSourceLayer_shift {S : BoundingSieve} {D z v w s τ σ K β : ℝ} {N : ℕ} (hβ : 1 < β) (hτdom : τ - 1 ∈ SuzukiFiniteContinuousLayers.suzukiParityDomainOne β (N - 1)) (hτσ : τ ≤ σ) (hD : 1 < D) (hz2 : 2 ≤ z) (hv2 : 2 ≤ v) (hw2 : 2 ≤ w) (hwv : w ≤ v) (hvz : v ≤ z) (hz : z = D ^ (1 / s)) (hv : v = D ^ (1 / τ)) (hw : w = D ^ (1 / σ)) (hK : 2 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) : (suzukiLemmaEightSevenPrimeSum S D w v z fun (t : ℝ) => SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (t - 1)) ≤ (1 / s * ∫ (t : ℝ) in τ..σ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (t - 1)) + 6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (τ - 1) / Real.log w * (τ / s)

Lemma 8.7 instantiated with Suzuki's preceding finite source layer H(t)=T_{N-1}(t-1). The only extra analytic device is the global clamp, which disappears from the prime sum, integral, and endpoint value.

def MathlibNt.SieveTheory.SwitchingPrinciple.finiteSourceRecursionIndices (N : ℕ) : Finset ℕ

Source indices whose (9.2) predecessors comprise T_{N-1}.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.finiteSourceRecursionIndices N = {n ∈ Finset.Icc 2 N | n % 2 = N % 2}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.finiteSourceRecursionIntegrand (β : ℝ) (N : ℕ) (t : ℝ) : ℝ

The sum of the normalized predecessor integrands appearing in (9.2) for all source indices selected by T_N.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.finiteSourceRecursionIntegrand β N t = ∑ n ∈ MathlibNt.SieveTheory.SwitchingPrinciple.finiteSourceRecursionIndices N, MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer 1 β (n - 1) (t - 1)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.finiteSourceRecursionIntegrand_eq (β : ℝ) (N : ℕ) (t : ℝ) : finiteSourceRecursionIntegrand β N t = SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (t - 1)

Exact index shift: the (9.2) recursion integrand for the T_N source indices is precisely T_{N-1}(t-1).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.integral_finiteSourceLayer_shift_eq_recursionIntegrand (β : ℝ) (N : ℕ) (τ σ : ℝ) : ∫ (t : ℝ) in τ..σ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (t - 1) = ∫ (t : ℝ) in τ..σ, finiteSourceRecursionIntegrand β N t

The main integral in the specialized Lemma 8.7 is exactly the aggregate continuous-recursion increment: every summand is one predecessor integrand from source equation (9.2).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLayerNumerator_eq_sourceRecursion_of_two_le (β s : ℝ) {n : ℕ} (hn : 2 ≤ n) : SuzukiFiniteContinuousLayers.suzukiLayerNumerator 1 β n s = ∫ (t : ℝ) in SuzukiFiniteContinuousLayers.recursionLower β s n..β + ↑n, SuzukiFiniteContinuousLayers.suzukiLayer 1 β (n - 1) (t - 1)

Each term selected in the aggregate recursion integrand is literally the normalized predecessor occurring on the right side of source equation (9.2).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiLemmaEightSeven_finiteSourceLayer_recursionIncrement {S : BoundingSieve} {D z v w s τ σ K β : ℝ} {N : ℕ} (hβ : 1 < β) (hτdom : τ - 1 ∈ SuzukiFiniteContinuousLayers.suzukiParityDomainOne β (N - 1)) (hτσ : τ ≤ σ) (hD : 1 < D) (hz2 : 2 ≤ z) (hv2 : 2 ≤ v) (hw2 : 2 ≤ w) (hwv : w ≤ v) (hvz : v ≤ z) (hz : z = D ^ (1 / s)) (hv : v = D ^ (1 / τ)) (hw : w = D ^ (1 / σ)) (hK : 2 ≤ K) (hlocal : HasDimensionOneLocalProductBound S K) : (suzukiLemmaEightSevenPrimeSum S D w v z fun (t : ℝ) => SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (t - 1)) ≤ (1 / s * ∫ (t : ℝ) in τ..σ, finiteSourceRecursionIntegrand β N t) + 6 * K ^ 2 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (τ - 1) / Real.log w * (τ / s)

Lemma 8.7 with its main term rewritten as the aggregate (9.2) recursion increment for the source indices of T_N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.parityDomain_upperClosed {β : ℝ} {m : ℕ} {x y : ℝ} : x ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β m → x ≤ y → y ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β m

The exact Suzuki parity domain is closed under increasing its real argument.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.Sigma11FiniteLayerMajorization {β s τ σ : ℝ} {N : ℕ} (hβ : 1 < β) (hsdom : s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β N) (hτdom : τ - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1)) (hsτ : s ≤ τ) (hτσ : τ ≤ σ) : 1 / s * ∫ (t : ℝ) in τ..σ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (t - 1) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β N s

The truncated middle-range recursion integral is bounded by the full finite source layer. Equality need not hold when the lower endpoint is larger than s or when the upper endpoint truncates source support.