def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.eps (n : ℕ) : ℕ

Suzuki's ε_n (zero for even n, one for odd n).

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.eps n = n % 2

def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.closedDomain (β : ℝ) (n : ℕ) : Set ℝ

Closed envelope of Suzuki's parity domain. For odd n this includes the left endpoint β-1; the exact source domain below removes it.

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.closedDomain β n = Set.Ici (β - ↑(MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.eps n))

def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain (β : ℝ) (n : ℕ) : Set ℝ

The exact parity domain I_n from Suzuki: (β-1,∞) for odd n and [β,∞) for even n.

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β n = if n % 2 = 1 then Set.Ioi (β - 1) else Set.Ici β

def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.lower (β s : ℝ) (n : ℕ) : ℝ

Clipped lower endpoint, implementing the empty-interval convention.

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.lower β s n = min (max s (β + ↑(MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.eps n))) (β + ↑n)

noncomputable def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.layer (β : ℝ) : ℕ → ℝ → ℝ

Correct normalized κ=1 layers. In the recursive clause the integrand is layer β (n+1), not its weighted numerator.

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.layer β 0 x✝ = 0
• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.layer β 1 x✝ = x✝⁻¹ * ∫ (_t : ℝ) in min x✝ (β + 1)..β + 1, 1
• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.layer β n.succ.succ x✝ = x✝⁻¹ * ∫ (t : ℝ) in MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.lower β x✝ (n + 2)..β + (↑n + 2), MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.layer β (n + 1) (t - 1)

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.eps_succ_add (n : ℕ) : eps (n + 1) + eps n = 1

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.eps_succ_succ_add (n : ℕ) : eps (n + 2) + eps (n + 1) = 1

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain_subset_closedDomain (β : ℝ) (n : ℕ) : parityDomain β n ⊆ closedDomain β n

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.closedDomain_pos {β : ℝ} (hβ : 1 < β) {n : ℕ} {s : ℝ} (hs : s ∈ closedDomain β n) : 0 < s

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.lower_mem (β s : ℝ) (n : ℕ) : lower β s n ∈ Set.Icc (β + ↑(eps n)) (β + ↑n)

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.lower_mono (β : ℝ) (n : ℕ) : Monotone fun (s : ℝ) => lower β s n

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.lower_continuous (β : ℝ) (n : ℕ) : Continuous fun (s : ℝ) => lower β s n

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.continuousOn_integral_to_const {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) : ContinuousOn (fun (x : ℝ) => ∫ (t : ℝ) in x..b, f t) (Set.Icc a b)

Continuity of a variable-lower-endpoint integral, requiring continuity only on the compact interval actually traversed.

structure MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.Regular (β : ℝ) (n : ℕ) : Prop

• continuous : ContinuousOn (layer β n) (closedDomain β n)
• nonneg (s : ℝ) : s ∈ closedDomain β n → 0 ≤ layer β n s
• weighted_antitone : AntitoneOn (fun (s : ℝ) => s * layer β n s) (closedDomain β n)

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.shifted_mem_previous {β : ℝ} {n : ℕ} {t : ℝ} (ht : β + ↑(eps (n + 2)) ≤ t) : t - 1 ∈ closedDomain β (n + 1)

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.regular_zero (β : ℝ) : Regular β 0

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.regular_one {β : ℝ} (hβ : 1 < β) : Regular β 1

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.regular_step {β : ℝ} (hβ : 1 < β) (n : ℕ) (ih : Regular β (n + 1)) : Regular β (n + 2)

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.regular {β : ℝ} (hβ : 1 < β) (n : ℕ) : Regular β n

κ=1 basic regularity on the closed envelope; hence, in particular, on the exact source parity domain.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.continuousOn_parityDomain {β : ℝ} (hβ : 1 < β) (n : ℕ) : ContinuousOn (layer β n) (parityDomain β n)

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.nonneg_on_parityDomain {β : ℝ} (hβ : 1 < β) (n : ℕ) (s : ℝ) : s ∈ parityDomain β n → 0 ≤ layer β n s

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.weighted_antitoneOn_parityDomain {β : ℝ} (hβ : 1 < β) (n : ℕ) : AntitoneOn (fun (s : ℝ) => s * layer β n s) (parityDomain β n)

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.antitoneOn_parityDomain {β : ℝ} (hβ : 1 < β) (n : ℕ) : AntitoneOn (layer β n) (parityDomain β n)

The unweighted assertion in Proposition 9.2(iii) follows from weighted antitonicity, positivity of the domain, and nonnegativity of the layer.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.layer_eq_zero_of_upper (β : ℝ) (n : ℕ) {s : ℝ} (hs : β + ↑n ≤ s) : layer β n s = 0

Proposition 9.2(i): clipping the lower endpoint makes the layer vanish once s ≥ β+n. This statement does not require a domain hypothesis.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.layer_eq_suzukiLayer (β : ℝ) (n : ℕ) (s : ℝ) : layer β n s = suzukiLayer 1 β n s

The specialized κ=1 model is definitionally the source-correct general layer.

@[reducible, inline]

abbrev MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiParityDomainOne (β : ℝ) (n : ℕ) : Set ℝ

Exact parity domain for the dimension-one finite layer.

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiParityDomainOne = MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_one_continuousOn_parityDomain {β : ℝ} (hβ : 1 < β) (n : ℕ) : ContinuousOn (suzukiLayer 1 β n) (suzukiParityDomainOne β n)

Proposition 9.2(ii), continuity on the exact parity domain, for κ=1.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_one_nonneg_on_parityDomain {β : ℝ} (hβ : 1 < β) (n : ℕ) (s : ℝ) : s ∈ suzukiParityDomainOne β n → 0 ≤ suzukiLayer 1 β n s

Proposition 9.2(ii), nonnegativity on the exact parity domain, for κ=1.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_one_weighted_antitoneOn_parityDomain {β : ℝ} (hβ : 1 < β) (n : ℕ) : AntitoneOn (fun (s : ℝ) => s * suzukiLayer 1 β n s) (suzukiParityDomainOne β n)

Proposition 9.2(iii), weighted antitonicity on the exact parity domain.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_one_antitoneOn_parityDomain {β : ℝ} (hβ : 1 < β) (n : ℕ) : AntitoneOn (suzukiLayer 1 β n) (suzukiParityDomainOne β n)

Proposition 9.2(iii), ordinary antitonicity on the exact parity domain.