Lcm.Criterion.σnorm_M_ge_σnorm_L'_mul

@[blueprint "lem:sigmaM-lower-final"  (title := "Lower bound for \\(\\sigma(M)/M\\)")  (statement := /--  With notation as above,  \[    \frac{\sigma(M)}{M}    \ge    \frac{\sigma(L')}{L'}    \Biggl( \prod_{i=1}^3 \Bigl(1 + \frac{1}{p_i(p_i+1)}\Bigr) \Biggr)    \Bigl(1 + \frac{3}{8n}\Bigr).  \]  -/)  (proof := /--    By multiplicativity, we have  $$    \frac{\sigma(M)}{M}    = \frac{\sigma(L')}{L'}    \prod_p \frac{1+p^{-1}+\dots+p^{-\nu_p(M)}}{1+p^{-1}+\dots+p^{-\nu_p(L')}}.  $$  The contribution of $p=p_i$ is  \[    \frac{(1+p_i^{-1}+p_i^{-2})}{1+p^{-1}_i}    = 1 + \frac{1}{p_i(p_i+1)}.  \]  The contribution of $p=2$ is  \[    \frac{1+2^{-1}+\dots+2^{-k-2}}{1+2^{-1}+\dots+2^{-k}},  \]  where \(k\) is the largest integer such that \(2^k \le n\).  A direct calculation yields  \[    \frac{(1+2^{-1}+\dots+2^{-k-2})}{1+2^{-1}+\dots+2^{-k}}    = \frac{2^{k+3}-1}{2^{k+3}-4}    = 1 + \frac{3}{2^{k+3}-4},  \]  Finally, since \(2^k \le n < 2^{k+1}\), we have \(2^{k+3} < 8n\), so  \[    \frac{3}{2^{k+3}-4} \ge \frac{3}{8n},  \]  So the contribution from the prime \(2\) is at least \(1 + 3/(8n)\).   Finally, the contribution of all other primes is at least \(1\).  -/)  (latexEnv := "lemma")  (discussion := 664)]theorem Criterion.σnorm_M_ge_σnorm_L'_mul (c : Criterion) :    σnorm c.M ≥      σnorm c.L' * (∏ i, (1 + 1 / (c.p i * (c.p i + 1 : ℝ)))) * (1 + 3 / (8 * c.n)) := by  have h_sigma_norm_M : (σnorm c.M) = (σnorm (c.L' : ℕ)) * (∏ p ∈ Nat.primeFactors c.M,      ((∑ i ∈ Finset.range (Nat.factorization c.M p + 1), (1 / p : ℝ) ^ i) /      (∑ i ∈ Finset.range (Nat.factorization (c.L' : ℕ) p + 1), (1 / p : ℝ) ^ i))) := by    have h_sigma_norm_prod : ∀ {n : ℕ}, n ≠ 0 → (σnorm n : ℝ) = (∏ p ∈ Nat.primeFactors n,        ((∑ i ∈ Finset.range (Nat.factorization n p + 1), (1 / p : ℝ) ^ i))) := by      intro n hn_ne_zero      have h_sigma_def : ((σ n) : ℝ) = (∏ p ∈ Nat.primeFactors n, (∑ i ∈ Finset.range          (Nat.factorization n p + 1), (p ^ i : ℝ))) := by        unfold σ        have h_sigma_def : ∀ {n : ℕ}, n ≠ 0 → (Nat.divisors n).sum (fun d ↦ d) =            ∏ p ∈ n.primeFactors, (∑ i ∈ Finset.range (Nat.factorization n p + 1), p ^ i) := by          exact fun {n} a ↦ sum_divisors a        convert congr_arg (( ↑ ) : ℕ → ℝ) (h_sigma_def hn_ne_zero) using 1 <;>        norm_num [ArithmeticFunction.sigma]      have h_sigma_def : (n : ℝ) = (∏ p ∈ Nat.primeFactors n, (p ^ (Nat.factorization n p) : ℝ)) :=        mod_cast Eq.symm (Nat.prod_factorization_pow_eq_self hn_ne_zero)      simp_all only [div_eq_mul_inv]      rw [← div_eq_mul_inv, ← Finset.prod_div_distrib]      refine Finset.prod_congr rfl fun p hp ↦ ?_      field_simp      rw [Finset.mul_sum _ _ _, ← Finset.sum_flip]      exact Finset.sum_congr rfl fun i hi ↦ by        rw [show ((1:ℝ) / ↑p) ^ i = 1 / ((↑p) ^ i) by simp]        rw [mul_one_div, eq_div_iff (pow_ne_zero _ <| Nat.cast_ne_zero.mpr <| Nat.ne_of_gt <|          Nat.pos_of_mem_primeFactors hp), ←pow_add, Nat.sub_add_cancel <|          Finset.mem_range_succ_iff.mp hi]    by_cases hM : c.M = 0 <;> by_cases hL' : c.L' = 0    · simp_all    · exact absurd hM (Nat.ne_of_gt (Criterion.M_pos c))    · exact absurd hL' (Nat.ne_of_gt (Criterion.L'_pos c))    · simp_all only [ne_eq, one_div, inv_pow, not_false_eq_true, prod_div_distrib]      rw [mul_div, eq_div_iff]      · rw [mul_comm, ← Finset.prod_subset (show c.L'.primeFactors ⊆ c.M.primeFactors from ?_)]        · intro p hp hpn; rw [Nat.factorization_eq_zero_of_not_dvd] <;> aesop        · intro p hp; simp_all only [mem_primeFactors, ne_eq, not_false_eq_true, and_true, true_and]          exact dvd_trans hp.2 (by exact ⟨(4 * ∏ i, c.p i) * c.m, by rw [Criterion.M]; ring⟩)      · exact Finset.prod_ne_zero_iff.mpr fun p hp ↦ ne_of_gt <| Finset.sum_pos          (fun _ _ ↦ inv_pos.mpr <| pow_pos (Nat.cast_pos.mpr <| Nat.pos_of_mem_primeFactors hp) _)          <| by norm_num  have h_ratio_terms (p : ℕ) (hp : p ∈ Nat.primeFactors c.M) : (∑ i ∈ Finset.range      (Nat.factorization c.M p + 1), (1 / p : ℝ) ^ i) / (∑ i ∈ Finset.range      (Nat.factorization (c.L' : ℕ) p + 1), (1 / p : ℝ) ^ i) ≥ if p ∈ Finset.image c.p Finset.univ      then (1 + 1 / (p * (p + 1) : ℝ)) else if p = 2 then (1 + 3 / (8 * c.n : ℝ)) else 1 := by    split_ifs    · obtain ⟨i, hi⟩ : ∃ i : Fin 3, p = c.p i := by grind      have h_ratio_p_i : (∑ i ∈ Finset.range (Nat.factorization c.M p + 1), (1 / p : ℝ) ^ i) /          (∑ i ∈ Finset.range (Nat.factorization (c.L' : ℕ) p + 1), (1 / p : ℝ) ^ i) ≥          (∑ i ∈ Finset.range 3, (1 / p : ℝ) ^ i) / (∑ i ∈ Finset.range 2, (1 / p : ℝ) ^ i) := by        rw [show Nat.factorization (c.L' : ℕ) p = 1 from hi ▸ c.val_p_L' i]        exact div_le_div_of_nonneg_right (Finset.sum_le_sum_of_subset_of_nonneg (Finset.range_mono          (by grind [c.val_p_M_ge_two i])) fun _ _ _ ↦ by positivity)          (Finset.sum_nonneg fun _ _ ↦ by positivity)      convert h_ratio_p_i using 1; norm_num [Finset.sum_range_succ]; ring_nf; field_simp; grind    · have h_geo_series : (∑ i ∈ Finset.range (Nat.factorization c.M 2 + 1), (1 / 2 : ℝ) ^ i)          / (∑ i ∈ Finset.range (Nat.factorization c.L' 2 + 1), (1 / 2 : ℝ) ^ i) ≥          (1 + 3 / (8 * c.n : ℝ)) := by        have h_geo_series : (∑ i ∈ Finset.range (Nat.factorization c.M 2 + 1), (1 / 2 : ℝ) ^ i)            / (∑ i ∈ Finset.range (Nat.factorization (c.L' : ℕ) 2 + 1), (1 / 2 : ℝ) ^ i) ≥            (∑ i ∈ Finset.range (Nat.factorization (c.L' : ℕ) 2 + 3), (1 / 2 : ℝ) ^ i) /            (∑ i ∈ Finset.range (Nat.factorization (c.L' : ℕ) 2 + 1), (1 / 2 : ℝ) ^ i) := by          exact div_le_div_of_nonneg_right (Finset.sum_le_sum_of_subset_of_nonneg            (Finset.range_mono (by linarith [val_two_M_ge_L' c])) fun _ _ _ ↦ by positivity)            (Finset.sum_nonneg fun _ _ ↦ by positivity)        refine le_trans ?_ h_geo_series        convert σnorm_ratio_ge_aux c.n _ using 1        exact c.val_two_L'.symm ▸ Nat.pow_log_le_self 2 (by linarith [c.hn])      aesop    · rw [ge_iff_le, le_div_iff₀] <;> norm_num      · refine Finset.sum_le_sum_of_subset_of_nonneg (Finset.range_mono (Nat.succ_le_succ ?_))          fun ?_ ?_ ?_ ↦ by positivity        have h_div : c.L' ∣ c.M := by          exact dvd_mul_left _ _        exact (Nat.factorization_le_iff_dvd (by aesop) (by aesop)) |>.2 h_div p      · exact Finset.sum_pos (fun _ _ ↦ inv_pos.mpr (pow_pos (Nat.cast_pos.mpr          (Nat.pos_of_mem_primeFactors hp)) _)) (by norm_num)  have h_prod_ratio_terms : (∏ p ∈ Nat.primeFactors c.M,      ((∑ i ∈ Finset.range (Nat.factorization c.M p + 1), (1 / p : ℝ) ^ i) /      (∑ i ∈ Finset.range (Nat.factorization (c.L' : ℕ) p + 1), (1 / p : ℝ) ^ i))) ≥      (∏ p ∈ Finset.image c.p Finset.univ, (1 + 1/(p * (p + 1) : ℝ)))*(1 + 3 / (8 * c.n : ℝ)) := by    refine le_trans ?_ (Finset.prod_le_prod ?_ h_ratio_terms)    · rw [Finset.prod_ite]      refine mul_le_mul ?_ ?_ (by positivity) (Finset.prod_nonneg fun _ _ ↦ by positivity)      · rw [Finset.prod_subset]        · simp only [mem_image, mem_univ, true_and, subset_iff, mem_filter, mem_primeFactors,            forall_exists_index, forall_apply_eq_imp_iff, exists_apply_eq_apply, and_true]          intro i; exact ⟨c.hp i, by            exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_left (dvd_mul_of_dvd_right              (Finset.dvd_prod_of_mem _ (Finset.mem_univ _)) _) _) _, by              exact Nat.ne_of_gt (Criterion.M_pos c)⟩        · aesop      · rw [Finset.prod_ite]        by_cases h : 2 ∈ c.M.primeFactors <;> simp_all +decide only          [mem_primeFactors, true_and, prod_const]        · simp only [one_pow, mul_one]          refine le_self_pow₀ (M₀ := ℝ) (by norm_num ; positivity) ?_          · norm_num; exact ⟨2, Nat.prime_two, h.1, h.2, fun i ↦ by linarith [c.p_gt_two i], rfl⟩        · contrapose! h          refine ⟨dvd_mul_of_dvd_left ?_ _, Nat.ne_of_gt (Criterion.M_pos c)⟩          · exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_left (by decide) _) _    · intro p hp; split_ifs <;> positivity  simp_all  rw [Finset.prod_image] at h_prod_ratio_terms <;> norm_num [Finset.prod_range_succ] at *  · simpa only [mul_assoc] using mul_le_mul_of_nonneg_left h_prod_ratio_terms <|      show 0 ≤ σnorm c.L' by exact div_nonneg (Nat.cast_nonneg _) <| Nat.cast_nonneg _  · simp [c.hp_mono.injective]