Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Factorization.lower_score_3_clean

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:822 to 832

Source documentation

The clean case of lower_score_3, combining the three subcases.

Exact Lean statement

lemma Factorization.lower_score_3_clean {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) :
    ∃ 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_clean {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) :    ∃ f' : Factorization n,      f'.total_imbalance < f.total_imbalance ∧ f'.score L ≤ f.score L := by  by_cases h_prod : (deficitMultiset f L).prod ≤ n  · exact lower_score_3_case1 f L h_surplus h_deficit_large hf h_prod  by_cases hL_gt_n : n < L  · exact lower_score_3_case2a f L h_surplus hf hL_gt_n  · exact lower_score_3_case2b f L h_surplus hf      (not_le.mp h_prod) (not_lt.mp hL_gt_n)