Periodicity of \(G_9\) in multiples of \(18900\) to The continuous Breusch function vanishes at small ratios

LemmaPeriodicity of \(G_9\) in multiples of \(18900\)#✓fully proved

For all natural numbers \(o\) and \(r\), the grid \(G\)-function for \(k = 9\) satisfies \(G_9(18900\,o + r) = G_9(r)\).

lemma G9_period_iter (o r : ℕ) : G9 (18900*o + r) = G9 r

Uses 2 · Used by 1

Statement usesBreusch grid function for \(k = 9\)

Proof usesOne-period shift of \(G_9\)

Used by\(G_9\) depends only on the residue modulo \(18900\)

Lemma\(G_9\) depends only on the residue modulo \(18900\)#✓fully proved

For every natural number \(j\), the grid \(G\)-function for \(k = 9\) satisfies \(G_9(j) = G_9(j \bmod 18900)\).

lemma G9_eq_mod (j : ℕ) : G9 j = G9 (j % 18900)

Uses 2 · Used by 4

Statement usesBreusch grid function for \(k = 9\)

Proof usesPeriodicity of \(G_9\) in multiples of \(18900\)

Used byThe continuous Breusch function is at most 3 · Level-\(1\) threshold for the continuous Breusch function · Level-\(2\) threshold for the continuous Breusch function · Level-\(3\) threshold for the continuous Breusch function

LemmaThe continuous Breusch function agrees with the grid function#✓fully proved

For every real \(x \ge 0\), the continuous Breusch function \(G\) and the Breusch grid function \(G_9\) satisfy \(G(x) = G_9(\lfloor 18900x \rfloor)\).

lemma G9r_eq_grid (x : ℝ) (hx : 0 ≤ x) : G9r x = G9 ⌊(18900:ℝ)*x⌋₊

Uses 10 · Used by 5

Statement usesBreusch grid function for \(k = 9\) · Continuous Breusch function

Proof usesSummand of the Breusch grid function · The modulus \(Q_9 = 210\) · Value of Q₉ · Real floors at divisors of 210 agree with grid floors · Sum over a duplicate-free list · The Möbius divisor table for \(210\) · Entries of the divisor table for \(210\) divide \(210\) · The divisor table for \(210\) has no repeated entries

Used byThe continuous Breusch function is at most 3 · Level-\(1\) threshold for the continuous Breusch function · Level-\(2\) threshold for the continuous Breusch function · Level-\(3\) threshold for the continuous Breusch function · The continuous Breusch function vanishes near zero

TheoremThe Breusch grid function vanishes below 9#✓fully proved

For every natural number \(j < 9\), the Breusch grid function \(G_9\) satisfies \(G_9(j) = 0\).

theorem G9_zero9 : ∀ j < 9, G9 j = 0

Uses 1 · Used by 2

Statement usesBreusch grid function for \(k = 9\)

Used byLevel-\(1\) threshold for the continuous Breusch function · The continuous Breusch function vanishes near zero

TheoremValue of \(G_9\) at \(9\)#✓fully proved

The grid \(G\)-function for \(k = 9\) satisfies \(G_9(9) = 1\).

theorem G9_at9 : G9 9 = 1

Uses 1

Statement usesBreusch grid function for \(k = 9\)

TheoremBound \(G_9 \le 1\) below \(10\)#✓fully proved

For every natural number \(j < 10\), the grid \(G\)-function for \(k = 9\) satisfies \(G_9(j) \le 1\).

theorem G9_small_le1 : ∀ j < 10, G9 j ≤ 1

Uses 1 · Used by 2

Statement usesBreusch grid function for \(k = 9\)

Used byLevel-\(2\) threshold for the continuous Breusch function · Level-\(3\) threshold for the continuous Breusch function

TheoremThe continuous Breusch function is at most 3#✓fully proved

For every real \(x \ge 0\), the continuous Breusch function \(G\) satisfies \(G(x) \le 3\).

theorem G9r_le3 (x : ℝ) (hx : 0 ≤ x) : G9r x ≤ 3

Uses 5 · Used by 2

Statement usesContinuous Breusch function

Proof usesBreusch grid function for \(k = 9\) · \(G_9\) depends only on the residue modulo \(18900\) · The continuous Breusch function agrees with the grid function · Grid bound \(G_9 \le 3\)

Used byThe truncated continuous Breusch function is at most 3 · Bound for one small-square prime term

TheoremThe continuous Breusch function vanishes near zero#✓fully proved

For every real \(x\) with \(0 \le x < 1/2100\), the continuous Breusch function \(G\) satisfies \(G(x) = 0\).

theorem G9r_vanish (x : ℝ) (hx0 : 0 ≤ x) (hx : x < 1 / ((10 * Q9 : ℕ) : ℝ)) :
    G9r x = 0

Uses 6 · Used by 1

Statement usesContinuous Breusch function · The modulus \(Q_9 = 210\)

Proof usesBreusch grid function for \(k = 9\) · The Breusch grid function vanishes below 9 · The continuous Breusch function agrees with the grid function · Value of Q₉

Used byThe continuous Breusch function vanishes at small ratios

TheoremLevel-\(1\) threshold for the continuous Breusch function#✓fully proved

Let \(Q_9 = 210\). For every real \(x \ge 1/(9 Q_9) = 1/1890\), if the continuous Breusch function \(G\) satisfies \(G(x) \ge 1\), then \(x \ge 279/18900\).

theorem G9r_level1 (x : ℝ) (hx : 1 / ((9 * Q9 : ℕ) : ℝ) ≤ x) (h : 1 ≤ G9r x) :
    (279 : ℝ) / 18900 ≤ x

Uses 8 · Used by 1

Statement usesContinuous Breusch function · The modulus \(Q_9 = 210\)

Proof usesBreusch grid function for \(k = 9\) · \(G_9\) depends only on the residue modulo \(18900\) · The Breusch grid function vanishes below 9 · The continuous Breusch function agrees with the grid function · Value of Q₉ · First index from \(10\) where the grid function reaches \(1\)

Used byUpper bound for primes where a Möbius-weighted floor sum is at least 1

TheoremLevel-\(2\) threshold for the continuous Breusch function#✓fully proved

Let \(Q_9 = 210\). For every real \(x \ge 1/(9 Q_9) = 1/1890\), if the continuous Breusch function \(G\) satisfies \(G(x) \ge 2\), then \(x \ge 657/18900\).

theorem G9r_level2 (x : ℝ) (hx : 1 / ((9 * Q9 : ℕ) : ℝ) ≤ x) (h : 2 ≤ G9r x) :
    (657 : ℝ) / 18900 ≤ x

Uses 8 · Used by 1

Statement usesContinuous Breusch function · The modulus \(Q_9 = 210\)

Proof usesBreusch grid function for \(k = 9\) · \(G_9\) depends only on the residue modulo \(18900\) · Bound \(G_9 \le 1\) below \(10\) · The continuous Breusch function agrees with the grid function · Value of Q₉ · First index from \(10\) where the grid function reaches \(2\)

Used byUpper bound for primes where a Möbius-weighted floor sum is at least 2

TheoremLevel-\(3\) threshold for the continuous Breusch function#✓fully proved

Let \(Q_9 = 210\). For every real \(x \ge 1/(9 Q_9) = 1/1890\), if the continuous Breusch function \(G\) satisfies \(G(x) \ge 3\), then \(x \ge 963/18900\).

theorem G9r_level3 (x : ℝ) (hx : 1 / ((9 * Q9 : ℕ) : ℝ) ≤ x) (h : 3 ≤ G9r x) :
    (963 : ℝ) / 18900 ≤ x

Uses 8 · Used by 1

Statement usesContinuous Breusch function · The modulus \(Q_9 = 210\)

Proof usesBreusch grid function for \(k = 9\) · \(G_9\) depends only on the residue modulo \(18900\) · Bound \(G_9 \le 1\) below \(10\) · The continuous Breusch function agrees with the grid function · Value of Q₉ · First index from 10 on with grid value at least 3

Used byUpper bound for primes where a Möbius-weighted floor sum is at least 3

LemmaInteger cast of the floor of a quotient of natural numbers#✓fully proved

For natural numbers \(t\) and \(d\), the floor of the real number \(t/d\), as an integer, equals the natural-number quotient of \(t\) by \(d\) (rounded down), as an integer. Both sides are \(0\) when \(d = 0\), since division by zero is \(0\) for both real numbers and natural numbers.

lemma intFloor_cast (t d : ℕ) :
    (Int.ofNat ⌊((t : ℕ) : ℝ) / ((d : ℕ) : ℝ)⌋₊ : ℤ) = ((t / d : ℕ) : ℤ)

Uses 1 · Used by 3

Proof usesFloor of a quotient of natural numbers

Used byLegendre terms of \(N_1\) as real floors · Legendre terms of \(N_{10}\) as real floors · Legendre terms of \(N_9\) as real floors

LemmaLegendre terms of \(N_{10}\) as real floors#✓fully proved

Let \(m \ge 1\) divide \(Q_9 = 210\), and let \(p \ge 2\), \(n\) and \(j\) be natural numbers. Write \(N_{10}(m, n) = 10n \cdot (Q_9/m)\). Then \(\lfloor N_{10}(m, n)/p^j \rfloor\) equals the floor of the real number \(10 Q_9 (n/p^j)/m\).

lemma floor_N10 {m n p j : ℕ} (hm : 1 ≤ m) (hd : m ∣ Q9) (hp2 : 2 ≤ p) :
    ((N10m m n / p ^ j : ℕ) : ℤ)
      = Int.ofNat ⌊((10*Q9:ℕ):ℝ)*((n : ℝ) / (((p ^ j : ℕ)) : ℝ))/((m : ℕ) : ℝ)⌋₊

Uses 4 · Used by 1

Statement usesScaled factorial argument \(N_{10}\) · The modulus \(Q_9 = 210\)

Proof usesExact formula for the scaled factorial argument \(N_{10}\) · Integer cast of the floor of a quotient of natural numbers

Used byValuation identity for the weighted product

LemmaLegendre terms of \(N_9\) as real floors#✓fully proved

Let \(m \ge 1\) divide \(Q_9 = 210\), and let \(p \ge 2\), \(n\) and \(j\) be natural numbers. Write \(N_9(m, n) = 9n \cdot (Q_9/m)\). Then \(\lfloor N_9(m, n)/p^j \rfloor\) equals the floor of the real number \(9 Q_9 (n/p^j)/m\).

lemma floor_N9 {m n p j : ℕ} (hm : 1 ≤ m) (hd : m ∣ Q9) (hp2 : 2 ≤ p) :
    ((N9m m n / p ^ j : ℕ) : ℤ)
      = Int.ofNat ⌊((9*Q9:ℕ):ℝ)*((n : ℝ) / (((p ^ j : ℕ)) : ℝ))/((m : ℕ) : ℝ)⌋₊

Uses 4 · Used by 1

Statement usesScaled factorial argument N₉ · The modulus \(Q_9 = 210\)

Proof usesExact formula for the scaled factorial argument \(N_9\) · Integer cast of the floor of a quotient of natural numbers

Used byValuation identity for the weighted product

LemmaLegendre terms of \(N_1\) as real floors#✓fully proved

Let \(m \ge 1\) divide \(Q_9 = 210\), and let \(p \ge 2\), \(n\) and \(j\) be natural numbers. Write \(N_1(m, n) = n \cdot (Q_9/m)\). Then \(\lfloor N_1(m, n)/p^j \rfloor\) equals the floor of the real number \(Q_9 (n/p^j)/m\).

lemma floor_N1 {m n p j : ℕ} (hm : 1 ≤ m) (hd : m ∣ Q9) (hp2 : 2 ≤ p) :
    ((N1m m n / p ^ j : ℕ) : ℤ)
      = Int.ofNat ⌊((Q9:ℕ):ℝ)*((n : ℝ) / (((p ^ j : ℕ)) : ℝ))/((m : ℕ) : ℝ)⌋₊

Uses 4 · Used by 1

Statement usesScaled factorial argument \(N_1\) · The modulus \(Q_9 = 210\)

Proof usesExact formula for the scaled factorial argument \(N_1\) · Integer cast of the floor of a quotient of natural numbers

Used byValuation identity for the weighted product

LemmaLegendre's formula with integer summands#✓fully proved

Let \(p\) be a prime and let \(N\) and \(b\) be natural numbers with \(\lfloor \log_p N \rfloor < b\), where \(\lfloor \log_p N \rfloor\) is taken to be \(0\) when \(N = 0\). Then the exponent of \(p\) in \(N!\), as an integer, equals \(\sum_{j=1}^{b-1} \lfloor N / p^j \rfloor\).

lemma legendre_sum9 {N p b : ℕ} (hp : p.Prime) (h : Nat.log p N < b) :
    (((N)!.factorization p : ℤ)) = ∑ j ∈ Finset.Ico 1 b, ((N / p ^ j : ℕ) : ℤ)

Used by 1

Used byValuation identity for the weighted product

LemmaValuation of a factorial ratio as a difference of valuations#✓fully proved

Let \(Q = 210\), let \(m \ge 1\) be a divisor of \(Q\), and let \(n\), \(p\) be natural numbers. Write \(N = n \cdot (Q/m)\) and \(R_m(n) = (10N)! / ((9N)! \, N!)\). Then, as integers, \(v_p(R_m(n)) = v_p((10N)!) - v_p((9N)!) - v_p(N!)\), where \(v_p(k)\) is the exponent of \(p\) in the prime factorization of \(k\) (zero when \(p\) is not prime).

lemma vp_ratio9 {m n p : ℕ} (hm1 : 1 ≤ m) (hd : m ∣ Q9) :
    ((ratio9 m n).factorization p : ℤ)
      = (((N10m m n)!.factorization p : ℤ) - ((N9m m n)!.factorization p : ℤ)
        - ((N1m m n)!.factorization p : ℤ))

Uses 6 · Used by 2

Statement usesScaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_1\) · Scaled factorial argument N₉ · The modulus \(Q_9 = 210\) · Binomial factor ratio₉

Proof usesFactorial divisibility behind ratio₉

Used byValuation term of one binomial factor · Valuation terms vanish off the prime support

DefinitionOne divisor's contribution to the valuation#✓fully proved

For a pair \((m, \varepsilon)\) of a natural number \(m\) and an integer \(\varepsilon\), and natural numbers \(p\) and \(n\), let \(a = \lfloor 210/m \rfloor\) (so \(a = 0\) when \(m = 0\)). The term is the integer \(\varepsilon\bigl(v_p((10na)!) - v_p((9na)!) - v_p((na)!)\bigr)\), where \(v_p(k)\) is the exponent of \(p\) in the prime factorization of \(k\) (zero when \(p\) is not prime).

def nu9term (q : ℕ × ℤ) (p n : ℕ) : ℤ :=
  q.2 * (((N10m q.1 n)!.factorization p : ℤ)
    - ((N9m q.1 n)!.factorization p : ℤ)
    - ((N1m q.1 n)!.factorization p : ℤ))

Uses 3 · Used by 6

Statement usesScaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_1\) · Scaled factorial argument N₉

Used byThe \(p\)-adic valuation of the weighted product · Valuation identity for the weighted product · Prime factorization of \(\log F_9(n)\) · Valuation term of one binomial factor · Valuation terms vanish off the prime support · A weighted log-factor as a sum over primes

DefinitionThe \(p\)-adic valuation of the weighted product#✓fully proved

For natural numbers \(p\) and \(n\), \(\nu_p(n)\) is the integer \(\sum_{d \mid 210} \mu(d)\bigl(v_p((2100n/d)!) - v_p((1890n/d)!) - v_p((210n/d)!)\bigr)\), where \(\mu\) is the Möbius function and \(v_p(m)\) is the exponent of \(p\) in the prime factorization of \(m\) (zero when \(p\) is not prime).

def nu9 (p n : ℕ) : ℤ :=
  w9.toFinset.sum (fun q : ℕ × ℤ => nu9term q p n)

Uses 2 · Used by 7

Statement usesOne divisor's contribution to the valuation · The Möbius divisor table for \(210\)

Used bySingle-term valuation identity for large primes · Valuation identity for the weighted product · Prime factorization of \(\log F_9(n)\) · Upper bound for \(\log F_9(n)\) when \((1890n, 2100n)\) has no prime · Contribution of primes with \(p^2 > 2100n\) · Contribution of the small-square primes · Bound for one small-square prime term

LemmaThe continuous Breusch function vanishes at small ratios#✓fully proved

Let \(p\) be a prime and let \(n \ge 1\) and \(j\) be natural numbers. If \(p^j > 2100n\), then the continuous Breusch function \(G\) satisfies \(G(n/p^j) = 0\).

lemma G9r_vanish_of {n p j : ℕ} (hp : p.Prime) (hn : 1 ≤ n)
    (h : 10 * Q9 * n < p ^ j) : G9r ((n : ℝ) / (((p ^ j : ℕ)) : ℝ)) = 0

Uses 4 · Used by 2

Statement usesContinuous Breusch function · The modulus \(Q_9 = 210\)

Proof usesThe continuous Breusch function vanishes near zero · Q₉ is positive

Used bySingle-term valuation identity for large primes · Bound for one small-square prime term

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.