Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Factorization.score_sum_change

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:529 to 547

Source documentation

The change in the score sum when one deficit prime p (with p ≤ L) has its balance increased by 1 (still ≤ 0).

Exact Lean statement

lemma Factorization.score_sum_change {n : ℕ} (f f' : Factorization n) (L p : ℕ)
    (hp_mem : p ∈ (n + 1).primesBelow) (hp_le_L : p ≤ L) (h_bal_p : f.balance p < 0)
    (h_bal_p' : f'.balance p = f.balance p + 1)
    (h_bal_eq : ∀ q ∈ (n + 1).primesBelow, q ≠ p → f'.balance q = f.balance q) :
    (∑ q ∈ (n + 1).primesBelow,
      if f'.balance q > 0 then (f'.balance q) * Real.log q
      else if q ≤ L then (-f'.balance q) * Real.log L
      else (-f'.balance q) * Real.log (n / q)) -
    (∑ q ∈ (n + 1).primesBelow,
      if f.balance q > 0 then (f.balance q) * Real.log q
      else if q ≤ L then (-f.balance q) * Real.log L
      else (-f.balance q) * Real.log (n / q)) = -Real.log L

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Factorization.score_sum_change {n : ℕ} (f f' : Factorization n) (L p : ℕ)    (hp_mem : p ∈ (n + 1).primesBelow) (hp_le_L : p ≤ L) (h_bal_p : f.balance p < 0)    (h_bal_p' : f'.balance p = f.balance p + 1)    (h_bal_eq : ∀ q ∈ (n + 1).primesBelow, q ≠ p → f'.balance q = f.balance q) :    (∑ q ∈ (n + 1).primesBelow,      if f'.balance q > 0 then (f'.balance q) * Real.log q      else if q ≤ L then (-f'.balance q) * Real.log L      else (-f'.balance q) * Real.log (n / q)) -    (∑ q ∈ (n + 1).primesBelow,      if f.balance q > 0 then (f.balance q) * Real.log q      else if q ≤ L then (-f.balance q) * Real.log L      else (-f.balance q) * Real.log (n / q)) = -Real.log L := by  rw [← Finset.sum_sub_distrib, Finset.sum_eq_single p]  · simp only [h_bal_p', h_bal_p.not_gt, ↓reduceIte, hp_le_L, Int.cast_add, Int.cast_one]    split_ifs with h    · omega    · ring  · exact fun q hq hqp ↦ by simp only [h_bal_eq q hq hqp, sub_self]  · exact absurd hp_mem