Suzuki's finite continuous layers: source-correct normalized recursion

This file records Suzuki, §9, (9.1)--(9.2). The decisive point is that the integrand in (9.2) is the preceding normalized layer f_{n-1}(t - 1), not its unnormalized numerator.

The normalized layer is therefore defined first by structural recursion. The numerator is then defined as the right-hand side of (9.1) or (9.2), so that the source equations are available without division. Their normalization bridge is valid for every s; cancellation in the opposite direction requires a nonzero normalizing factor (below we expose the natural hypothesis 0 < s).

inductive MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.Side : Type

• upper : Side
• lower : Side

@[instance_reducible]

instance MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.instDecidableEqSide : DecidableEq Side

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.instDecidableEqSide x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.instReprSide : Repr Side

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.instReprSide = { reprPrec := MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.instReprSide.repr }

def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.instReprSide.repr : Side → ℕ → Std.Format

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.instReprSide.repr MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.Side.upper prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.Side.upper")).group prec✝
• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.instReprSide.repr MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.Side.lower prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.Side.lower")).group prec✝

def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.Side.sourceParity : Side → ℕ

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.Side.upper.sourceParity = 1
• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.Side.lower.sourceParity = 0

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.Side.sourceParity_upper : upper.sourceParity = 1

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.Side.sourceParity_lower : lower.sourceParity = 0

def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.sourceEpsilon (n : ℕ) : ℕ

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.sourceEpsilon n = n % 2

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.sourceEpsilon_even {n : ℕ} (h : Even n) : sourceEpsilon n = 0

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.sourceEpsilon_odd {n : ℕ} (h : Odd n) : sourceEpsilon n = 1

noncomputable def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.dPowDensity (κ t : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.dPowDensity κ t = κ * t ^ (κ - 1)

def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.baseLower (β s : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.baseLower β s = min s (β + 1)

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

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.recursionLower β s n = min (max s (β + ↑(MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.sourceEpsilon n))) (β + ↑n)

noncomputable def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer (κ β : ℝ) : ℕ → ℝ → ℝ

Suzuki's normalized fₙ. In the recursive case the source integrand is f_{n-1}(t-1), as in (9.2).

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer κ β 0 x✝ = 0
• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer κ β 1 x✝ = (x✝ ^ κ)⁻¹ * ∫ (t : ℝ) in MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.baseLower β x✝..β + 1, MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.dPowDensity κ t
• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer κ β n.succ.succ x✝ = (x✝ ^ κ)⁻¹ * ∫ (t : ℝ) in MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.recursionLower β x✝ (n + 2)..β + (↑n + 2), MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer κ β (n + 1) (t - 1) * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.dPowDensity κ t

noncomputable def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayerNumerator (κ β : ℝ) : ℕ → ℝ → ℝ

The source right-hand side s^κ fₙ(s) from (9.1)--(9.2). This is kept as an API in its own right, but its recursive integrand is the normalized preceding layer, not the preceding numerator.

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayerNumerator κ β 0 x✝ = 0
• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayerNumerator κ β 1 x✝ = ∫ (t : ℝ) in MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.baseLower β x✝..β + 1, MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.dPowDensity κ t
• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayerNumerator κ β n.succ.succ x✝ = ∫ (t : ℝ) in MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.recursionLower β x✝ (n + 2)..β + (↑n + 2), MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer κ β (n + 1) (t - 1) * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.dPowDensity κ t

noncomputable def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSideLayer (side : Side) (κ β : ℝ) (N : ℕ) (s : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSideLayer side κ β N s = ∑ n ∈ Finset.Icc 1 N, if n % 2 = side.sourceParity then MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer κ β n s else 0

noncomputable def MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer (κ β : ℝ) (N : ℕ) (s : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer κ β N s = ∑ n ∈ Finset.Icc 1 N, if n % 2 = N % 2 then MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer κ β n s else 0

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_zero (κ β s : ℝ) : suzukiLayer κ β 0 s = 0

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayerNumerator_zero (κ β s : ℝ) : suzukiLayerNumerator κ β 0 s = 0

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_one (κ β s : ℝ) : suzukiLayer κ β 1 s = (s ^ κ)⁻¹ * ∫ (t : ℝ) in baseLower β s..β + 1, dPowDensity κ t

Normalized form of (9.1).

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_succ_succ (κ β s : ℝ) (n : ℕ) : suzukiLayer κ β (n + 2) s = (s ^ κ)⁻¹ * ∫ (t : ℝ) in recursionLower β s (n + 2)..β + (↑n + 2), suzukiLayer κ β (n + 1) (t - 1) * dPowDensity κ t

Normalized form of (9.2), with the preceding normalized layer in the integrand.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayerNumerator_one (κ β s : ℝ) : suzukiLayerNumerator κ β 1 s = ∫ (t : ℝ) in baseLower β s..β + 1, dPowDensity κ t

Unnormalized source right-hand side in (9.1).

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayerNumerator_succ_succ (κ β s : ℝ) (n : ℕ) : suzukiLayerNumerator κ β (n + 2) s = ∫ (t : ℝ) in recursionLower β s (n + 2)..β + (↑n + 2), suzukiLayer κ β (n + 1) (t - 1) * dPowDensity κ t

Source-correct unnormalized right-hand side in (9.2).

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_eq_inv_rpow_mul_numerator (κ β : ℝ) (n : ℕ) (s : ℝ) : suzukiLayer κ β n s = (s ^ κ)⁻¹ * suzukiLayerNumerator κ β n s

The division-form bridge is total, including at s = 0.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.rpow_mul_suzukiLayer_of_ne (κ β : ℝ) (n : ℕ) (s : ℝ) (hs : s ^ κ ≠ 0) : s ^ κ * suzukiLayer κ β n s = suzukiLayerNumerator κ β n s

Cancellation is valid whenever the normalizing factor is nonzero.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.rpow_mul_suzukiLayer (κ β : ℝ) (n : ℕ) {s : ℝ} (hs : 0 < s) : s ^ κ * suzukiLayer κ β n s = suzukiLayerNumerator κ β n s

The source equation s^κ fₙ(s) = RHSₙ(s) after legal cancellation on the positive Suzuki domain.

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_at_zero (κ β : ℝ) (n : ℕ) (hκ : 0 < κ) : suzukiLayer κ β n 0 = 0

At the excluded point s = 0, positive κ makes the normalized definition zero. No theorem identifies its numerator with 0: multiplying by 0^κ cannot recover an arbitrary source right-hand side.

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.baseLower_eq_upper {β s : ℝ} (hs : β + 1 ≤ s) : baseLower β s = β + 1

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.recursionLower_eq_upper {β s : ℝ} {n : ℕ} (hs : β + ↑n ≤ s) : recursionLower β s n = β + ↑n

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayerNumerator_eq_zero_of_le (κ β : ℝ) (n : ℕ) {s : ℝ} (hs : β + ↑n ≤ s) : suzukiLayerNumerator κ β n s = 0

Proposition 9.2(i), at the level of the source RHS.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer_eq_zero_of_le (κ β : ℝ) (n : ℕ) {s : ℝ} (hs : β + ↑n ≤ s) : suzukiLayer κ β n s = 0

Proposition 9.2(i), for a normalized finite layer.

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.dPowDensity_nonneg {κ t : ℝ} (hκ : 0 ≤ κ) (ht : 0 ≤ t) : 0 ≤ dPowDensity κ t

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayerNumerator_one_nonneg {κ β s : ℝ} (hκ : 0 ≤ κ) (hβ : 1 ≤ β) (hs : β - 1 < s) : 0 ≤ suzukiLayerNumerator κ β 1 s

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayerNumerator_succ_succ_nonneg {κ β s : ℝ} {n : ℕ} (hκ : 0 ≤ κ) (hβ : 1 ≤ β) (hprev : ∀ t ∈ Set.Icc (recursionLower β s (n + 2)) (β + (↑n + 2)), 0 ≤ suzukiLayer κ β (n + 1) (t - 1)) : 0 ≤ suzukiLayerNumerator κ β (n + 2) s

One source-correct recursive positivity step: the induction hypothesis is on the preceding normalized layer.

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSideLayer_zero (side : Side) (κ β s : ℝ) : finiteSideLayer side κ β 0 s = 0

@[simp]

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer_zero (κ β s : ℝ) : finiteSourceLayer κ β 0 s = 0

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer_eq_upper_of_odd (κ β : ℝ) {N : ℕ} (hN : Odd N) (s : ℝ) : finiteSourceLayer κ β N s = finiteSideLayer Side.upper κ β N s

theorem MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer_eq_lower_of_even (κ β : ℝ) {N : ℕ} (hN : Even N) (s : ℝ) : finiteSourceLayer κ β N s = finiteSideLayer Side.lower κ β N s