Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Factorization.lower_score_3_case1

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:432 to 475

Source documentation

Case 1 of lower_score_3: if the product of deficit primes is ≤ n, adding the full deficit multiset yields a factorization with zero imbalance and lower score.

Exact Lean statement

lemma Factorization.lower_score_3_case1 {n : ℕ} (f : Factorization n) (L : ℕ)
    (h_surplus : ∀ p, f.balance p ≤ 0) (h_deficit_large : ∀ p, f.balance p < 0 → p ≤ L)
    (hf : ∃ p ∈ (n + 1).primesBelow, p ≤ L ∧ f.balance p < 0)
    (h_prod : (deficitMultiset f L).prod ≤ n) :
    ∃ f' : Factorization n,
      f'.total_imbalance < f.total_imbalance ∧
      f'.score L ≤ f.score L

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Factorization.lower_score_3_case1 {n : ℕ} (f : Factorization n) (L : ℕ)    (h_surplus : ∀ p, f.balance p ≤ 0) (h_deficit_large : ∀ p, f.balance p < 0 → p ≤ L)    (hf : ∃ p ∈ (n + 1).primesBelow, p ≤ L ∧ f.balance p < 0)    (h_prod : (deficitMultiset f L).prod ≤ n) :    ∃ f' : Factorization n,      f'.total_imbalance < f.total_imbalance ∧      f'.score L ≤ f.score L := by  set f' := addFactor f (deficitMultiset f L).prod    h_prod (deficitMultiset_prod_pos f L) with hf'  have h_zero_bal : ∀ p, f'.balance p = 0 :=    addFactor_deficit_balance_eq_zero f L h_surplus h_deficit_large _ h_prod      (deficitMultiset_prod_pos f L) rfl  have hf'_imb : f'.total_imbalance = 0 :=    Finset.sum_eq_zero fun p _ ↦ by simp [h_zero_bal p]  obtain ⟨p₀, hp₀_mem, _, hp₀_bal⟩ := hf  have hn_pos : 0 < n := (prime_of_mem_primesBelow hp₀_mem).pos.trans_le    (Nat.lt_succ_iff.mp (mem_primesBelow.mp hp₀_mem).1)  have hf'_score : f'.score L ≤ f.score L := by    rw [score_eq (Finset.sum_eq_zero fun p _ ↦ by simp [h_zero_bal p])]    unfold score    split_ifs with h    · rw [addFactor_waste]      have h_log_ineq : Real.log (n / (deficitMultiset f L).prod) ≤ Real.log n :=        Real.log_le_log (div_pos (Nat.cast_pos.mpr hn_pos)          (Nat.cast_pos.mpr (deficitMultiset_prod_pos f L)))          (div_le_self (Nat.cast_nonneg _) (by exact_mod_cast deficitMultiset_prod_pos f L))      have h_sum_nonneg : 0 ≤ ∑ p ∈ (n + 1).primesBelow,          if f.balance p > 0 then (f.balance p : ℝ) * Real.log p          else if p ≤ L then (-f.balance p : ℝ) * Real.log L          else (-f.balance p : ℝ) * Real.log (n / p) :=        Finset.sum_nonneg fun p hp ↦ by          split_ifs with h1 h2          · linarith [h_surplus p]          · exact mul_nonneg (by simp; linarith [h_surplus p])              (Real.log_nonneg (by norm_cast; linarith [(prime_of_mem_primesBelow hp).two_le]))          · have h_bal_zero : f.balance p = 0 :=              le_antisymm (h_surplus p) (not_lt.mp fun hlt ↦ h2 (h_deficit_large p hlt))            simp [h_bal_zero]      linarith    · simp_all [total_imbalance]  have h_imb_pos : 0 < f.total_imbalance :=    Finset.single_le_sum (fun _ _ ↦ Nat.zero_le _) hp₀_mem |>.trans_lt'      (Int.natAbs_pos.mpr hp₀_bal.ne)  exact ⟨f', hf'_imb ▸ h_imb_pos, hf'_score⟩