Sieve.selbergBoundingSum_ge_sum_div

theorem selbergBoundingSum_ge_sum_div (s : SelbergSieve) (hP : ∀ p:ℕ, p.Prime → (p:ℝ) ≤ s.level → p ∣ s.prodPrimes)  (hnu : CompletelyMultiplicative s.nu) (hnu_nonneg : ∀ n, 0 ≤ s.nu n) (hnu_lt : ∀ p, p.Prime → p ∣ s.prodPrimes → s.nu p < 1):    s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 (Nat.floor <| Real.sqrt s.level), s.nu m := by  unfold selbergBoundingSum  calc ∑ l ∈ s.prodPrimes.divisors, (if l ^ 2 ≤ s.level then selbergTerms _ l else 0)     ≥ ∑ l ∈ s.prodPrimes.divisors.filter (fun (l:ℕ) => l^2 ≤ s.level),        ∑ m ∈ (l^(Nat.floor s.level)).divisors.filter (l ∣ ·), s.nu m         := ?_   _ ≥ ∑ m ∈ Finset.Icc 1 (Nat.floor <| Real.sqrt s.level), s.nu m           := ?_  · rw [←Finset.sum_filter]; apply Finset.sum_le_sum; intro l hl    rw [Finset.mem_filter, Nat.mem_divisors] at hl    have hlsq : Squarefree l := Squarefree.squarefree_of_dvd hl.1.1 s.prodPrimes_squarefree    trans (∏ p ∈ l.primeFactors, ∑ n ∈ Finset.Icc 1 (Nat.floor s.level), s.nu (p^n))    · rw [prod_factors_sum_pow_compMult (Nat.floor s.level) _ s.nu]      · exact hnu      · exact hlsq      · rw [ne_eq, Nat.floor_eq_zero, not_lt]        exact s.one_le_level    rw [selbergTerms_apply _ l]    apply prod_factors_one_div_compMult_ge _ _ hnu _ _ hlsq    · intro p hpp hpl      apply hnu_lt p hpp (Trans.trans hpl hl.1.1)    · exact hnu_nonneg   rw [←Finset.sum_biUnion]  · apply Finset.sum_le_sum_of_subset_of_nonneg ?_ (fun _ _ _ => hnu_nonneg _)    intro m hm    have hprod_pos : 0 < (∏ p ∈ m.primeFactors, p) := by      apply Finset.prod_pos;      intro p hp; exact Nat.pos_of_mem_primeFactorsList <| List.mem_toFinset.mp hp    have hprod_ne_zero :  (∏ p ∈ m.primeFactors, p) ^ ⌊s.level⌋₊ ≠ 0 := by      apply pow_ne_zero; apply ne_of_gt; apply hprod_pos    rw [Finset.mem_biUnion]; simp_rw [Finset.mem_filter, Nat.mem_divisors]    rw [Finset.mem_Icc, Nat.le_floor_iff] at hm    · have hm_ne_zero : m ≠ 0 := by        exact ne_of_gt <| Nat.succ_le_iff.mp hm.1      use ∏ p ∈ m.primeFactors, p      constructor; constructor; constructor      · apply prod_primes_dvd_of_dvd <;> intro p hp        · apply hP p <| Nat.prime_of_mem_primeFactors hp          trans (m:ℝ)          · exact_mod_cast Nat.le_of_mem_primeFactors hp          trans (Real.sqrt s.level)          · exact hm.2          apply sqrt_le_self s.level s.one_le_level        exact Nat.prime_of_mem_primeFactors hp      · exact prodPrimes_ne_zero      · rw [←Real.sqrt_le_sqrt_iff (by linarith only [s.one_le_level]), Real.sqrt_sq]        · trans (m:ℝ)          · norm_cast; apply Nat.le_of_dvd (Nat.succ_le_iff.mp hm.1)            exact Nat.prod_primeFactors_dvd m          exact hm.2        apply le_of_lt; norm_cast      constructor; constructor      · rw [←Nat.factorization_le_iff_dvd _ hprod_ne_zero, Nat.factorization_pow]        · intro p          have hy_mul_prod_nonneg : 0 ≤ ⌊s.level⌋₊ * (Nat.factorization (∏ p ∈ m.primeFactors, p)) p := by            apply mul_nonneg            · apply Nat.le_floor; norm_cast; linarith only [s.one_le_level]            · norm_num          trans (Nat.factorization m) p * 1          · rw [mul_one]          rw [Finsupp.smul_apply, smul_eq_mul]          by_cases hpp : p.Prime          swap          · rw [Nat.factorization_eq_zero_of_not_prime _ hpp, zero_mul]; exact hy_mul_prod_nonneg          by_cases hpdvd : p ∣ m          swap          · rw [Nat.factorization_eq_zero_of_not_dvd hpdvd, zero_mul]; exact hy_mul_prod_nonneg          apply mul_le_mul          · trans m            · apply le_of_lt <| Nat.factorization_lt _ _              apply hm_ne_zero            apply Nat.le_floor            refine le_trans hm.2 ?_            apply sqrt_le_self _ s.one_le_level          · rw [←Nat.Prime.pow_dvd_iff_le_factorization hpp <| ne_of_gt hprod_pos, pow_one]            apply Finset.dvd_prod_of_mem            rw [Nat.mem_primeFactors]            exact ⟨hpp, hpdvd, hm_ne_zero⟩          · norm_num          · norm_num        exact hm_ne_zero      · exact hprod_ne_zero      · exact Nat.prod_primeFactors_dvd m    · apply Real.sqrt_nonneg  · intro i hi j hj hij t hti htj x hx    simp only [Finset.bot_eq_empty, Finset.notMem_empty]    specialize hti hx    specialize htj hx    simp_rw [Finset.mem_coe, Finset.mem_filter, Nat.mem_divisors] at *    have h : ∀ i j {n}, i ∣ s.prodPrimes → i ∣ x → x ∣ j ^ n → i ∣ j := by      intro i j n hiP hix hij      apply Nat.squarefree_dvd_pow i j n (squarefree_of_dvd_prodPrimes hiP)      exact Trans.trans hix hij    have hidvdj : i ∣ j := by      apply h i j hi.1.1 hti.2 htj.1.1    have hjdvdi : j ∣ i := by      apply h j i hj.1.1 htj.2 hti.1.1    exact hij <| Nat.dvd_antisymm hidvdj hjdvdi