Lcm.Criterion.σnorm_ln_eq

@[blueprint  "lem:sigmaLn"  (title := "Normalised divisor sum for \\(L_n\\)")  (statement := /--  Let \(L'\) be as in Lemma~\ref{lem:Lprime-def}. Then  \begin{equation}\label{eq:sigmaLn}    \frac{\sigma(L_n)}{L_n}    \;=\;    \frac{\sigma(L')}{L'} \prod_{i=1}^3 \Bigl(1 + \frac{1}{q_i}\Bigr).  \end{equation}  -/)  (proof := /--  Use the multiplicativity of \(\sigma(\cdot)\) and the fact that each \(q_i\) occurs to the first  power in \(L_n\).  Then  \[    \sigma(L_n)    = \sigma(L') \prod_{i=1}^3 \sigma(q_i)    = \sigma(L') \prod_{i=1}^3 (1+q_i).  \]  Dividing by \(L_n = L' \prod_{i=1}^3 q_i\) gives  \[    \frac{\sigma(L_n)}{L_n}    = \frac{\sigma(L')}{L'} \prod_{i=1}^3 \frac{1+q_i}{q_i}    = \frac{\sigma(L')}{L'} \prod_{i=1}^3 \Bigl(1 + \frac{1}{q_i}\Bigr).  \]  -/)  (proofUses := ["lem:Lprime-def"])  (latexEnv := "lemma")]theorem Criterion.σnorm_ln_eq (c : Criterion) :    σnorm (L c.n) = σnorm c.L' * ∏ i, (1 + (1 : ℝ) / c.q i) := by  have hcop : ∀ i j, i ≠ j → (c.q i).Coprime (c.q j) := fun i j h ↦    (coprime_primes (c.hq i) (c.hq j)).mpr (c.hq_mono.injective.ne h)  have hcopL' : ∀ i, (c.q i).Coprime c.L' := fun i ↦    (c.hq i).coprime_iff_not_dvd.mpr (c.q_not_dvd_L' i)  have hσ_prime : ∀ i, sigma 1 (c.q i) = 1 + c.q i := fun i ↦ by    rw [← pow_one (c.q i), sigma_one_apply_prime_pow (c.hq i)]    simp [reduceAdd, geom_sum_two, pow_one, add_comm]  simp only [σnorm, σ, c.L_eq_prod_q_mul_L', Fin.prod_univ_three]  rw [show c.q 0 * c.q 1 * c.q 2 * c.L' = (c.q 0 * c.q 1 * c.q 2) * c.L' by ring,      isMultiplicative_sigma.map_mul_of_coprime (coprime_mul_iff_left.mpr        ⟨coprime_mul_iff_left.mpr ⟨hcopL' 0, hcopL' 1⟩, hcopL' 2⟩),      show c.q 0 * c.q 1 * c.q 2 = c.q 0 * (c.q 1 * c.q 2) by ring,      isMultiplicative_sigma.map_mul_of_coprime (coprime_mul_iff_right.mpr        ⟨hcop 0 1 Fin.zero_ne_one, hcop 0 2 <| not_eq_of_beq_eq_false rfl⟩),      isMultiplicative_sigma.map_mul_of_coprime (hcop 1 2 <| not_eq_of_beq_eq_false rfl),      hσ_prime, hσ_prime, hσ_prime]  have hq_ne : ∀ i, (c.q i : ℝ) ≠ 0 := fun i ↦ (cast_pos.mpr (c.hq i).pos).ne'  field_simp [hq_ne, (cast_pos.mpr c.L'_pos).ne']  grind