Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Factorization.addFactor_deficit_balance_eq_zero

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:408 to 428

Source documentation

Adding the full deficit multiset product to a factorization with no surplus primes and all deficit primes at most L results in zero balance for all primes.

Exact Lean statement

lemma Factorization.addFactor_deficit_balance_eq_zero {n : ℕ} (f : Factorization n) (L : ℕ)
    (h_surplus : ∀ p, f.balance p ≤ 0) (h_deficit_large : ∀ p, f.balance p < 0 → p ≤ L)
    (m : ℕ) (hm : m ≤ n) (hm_pos : 0 < m) (h_m_def : m = (deficitMultiset f L).prod) :
    ∀ p, (addFactor f m hm hm_pos).balance p = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Factorization.addFactor_deficit_balance_eq_zero {n : ℕ} (f : Factorization n) (L : ℕ)    (h_surplus : ∀ p, f.balance p ≤ 0) (h_deficit_large : ∀ p, f.balance p < 0 → p ≤ L)    (m : ℕ) (hm : m ≤ n) (hm_pos : 0 < m) (h_m_def : m = (deficitMultiset f L).prod) :    ∀ p, (addFactor f m hm hm_pos).balance p = 0 := fun p ↦ by  by_cases hp : p.Prime <;> by_cases hp_le_L : p ≤ L <;> simp_all only [addFactor_balance]  · simp_all only [CanonicallyOrderedAdd.multiset_prod_pos]    simp only [factorization_prod_eq_count (fun q hq ↦ (mem_deficitMultiset f L q hq).1)]    by_cases hp_def : f.balance p < 0 <;> simp_all only [cast_ite, cast_natAbs, Int.cast_eq,      CharP.cast_eq_zero, count_deficitMultiset, abs_of_nonneg (le_of_not_gt hp_def)]    · split_ifs <;> simp_all only [abs_of_neg hp_def, add_neg_cancel, primesBelow,        Finset.mem_filter, Finset.mem_range, and_true]      · linarith [h_deficit_large p hp_def, deficit_implies_le_n f p hp_def]    · split_ifs <;> grind  · simp_all only [CanonicallyOrderedAdd.multiset_prod_pos, not_le]    have h_bal_zero : f.balance p = 0 :=      le_antisymm (h_surplus p) (not_lt.mp fun h ↦ hp_le_L.not_ge (h_deficit_large p h))    simp only [factorization_prod_eq_count (fun q hq ↦ (mem_deficitMultiset f L q hq).1),      count_deficitMultiset]    grind  · simp_all [balance, sum]  · simp_all [balance, sum]