Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiLemma144ActualRecurrence

Suzuki Lemma 14.4: the actual discrete recurrence and (14.9) #

This file works with the source-faithful natural-valued layers suzukiSourceV. The quotient in every recursive layer is therefore literally D ⌈/⌉ p.

source
noncomputable def MathlibNt.SieveTheory.suzukiActualT (S : BoundingSieve) :
ℕ → ℕ → ℕ → ℝ

The actual finite parity aggregate: V_N + V_{N-2} + ..., stopping at V₁ or V₂. In particular depth zero is not inserted into a positive-depth Suzuki sum.

Equations
Instances For
    source
    @[simp]
    theorem MathlibNt.SieveTheory.suzukiActualT_zero (S : BoundingSieve) (D z : ℕ) :
    suzukiActualT S 0 D z = 0
    source
    @[simp]
    theorem MathlibNt.SieveTheory.suzukiActualT_one (S : BoundingSieve) (D z : ℕ) :
    suzukiActualT S 1 D z = suzukiSourceV S 1 D z
    source
    @[simp]
    theorem MathlibNt.SieveTheory.suzukiActualT_add_two (S : BoundingSieve) (n D z : ℕ) :
    suzukiActualT S (n + 2) D z = suzukiSourceV S (n + 2) D z + suzukiActualT S n D z
    source
    def MathlibNt.SieveTheory.suzukiActualParityCarrier (N : ℕ) :
    Finset ℕ

    The literal finite carrier 1 ≤ n ≤ N, n ≡ N (mod 2).

    Equations
    Instances For
      source
      theorem MathlibNt.SieveTheory.suzukiActualT_eq_parity_sum (S : BoundingSieve) (N D z : ℕ) :
      suzukiActualT S N D z = ∑ n ∈ suzukiActualParityCarrier N, suzukiSourceV S n D z

      The recursive presentation above is exactly Suzuki's displayed finite parity sum, not an unbounded series or a depth scan.

      source
      theorem MathlibNt.SieveTheory.suzukiSourceV_eq_zero_of_pow_le_allDepth (S : BoundingSieve) (n D z : ℕ) (hzD : z ^ (n + 2) ≤ D) :
      suzukiSourceV S n D z = 0

      The elementary support cutoff used to erase Suzuki's lower outer cutoff. It includes the natural boundary with ≤: strictness comes from p < z.

      source
      theorem MathlibNt.SieveTheory.suzukiSourceV_succ_eq_unrestricted (S : BoundingSieve) {n D z : ℕ} (hn : 0 < n) (hOddBoundary : Odd (n + 1) → z ^ 3 ≤ D) :
      suzukiSourceV S (n + 1) D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * suzukiSourceV S n (D ⌈/⌉ p) p

      For a positive predecessor, the lower carrier may be erased by support vanishing. In odd outer depth the Case-I boundary z³ ≤ D also makes the source upper cutoff automatic.

      source
      theorem MathlibNt.SieveTheory.suzukiActualT_caseI_recurrence (S : BoundingSieve) {N D z : ℕ} (hN : 2 ≤ N) (hOddBoundary : Odd N → z ^ 3 ≤ D) :
      suzukiActualT S N D z = ∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p * suzukiActualT S (N - 1) (D ⌈/⌉ p) p

      Case I's exact discrete recurrence. The hypothesis is needed only in odd parity; for even N it is vacuous. The assumptions 2 ≤ N and the natural ceiling quotient are explicit.

      source
      noncomputable def MathlibNt.SieveTheory.suzukiSigmaZero (S : BoundingSieve) (N D z : ℕ) (a : ℝ) :
      ℝ

      The three finite pieces in Suzuki (14.9). The support already contains p < z; a and b are respectively D^(1/σ) and D^(1/τ).

      Equations
      Instances For
        source
        noncomputable def MathlibNt.SieveTheory.suzukiSigmaOne (S : BoundingSieve) (N D z : ℕ) (a b : ℝ) :
        ℝ
        Equations
        Instances For
          source
          noncomputable def MathlibNt.SieveTheory.suzukiSigmaTwo (S : BoundingSieve) (N D z : ℕ) (b : ℝ) :
          ℝ
          Equations
          Instances For
            source
            theorem MathlibNt.SieveTheory.suzuki_equation14_9 (S : BoundingSieve) {N D z : ℕ} (hN : 2 ≤ N) (hOddBoundary : Odd N → z ^ 3 ≤ D) {a b : ℝ} (hab : a ≤ b) :
            suzukiActualT S N D z = suzukiSigmaZero S N D z a + suzukiSigmaOne S N D z a b + suzukiSigmaTwo S N D z b

            Equation (14.9), before substituting the two real-power endpoints. This is an equality of finite sums, including all boundary choices (<, ≤) exactly.