MobiusLemma.mobius_lemma_1_sub

@[blueprint  "mobius-lemma-1-sub"  (title := "Mobius Lemma 1, initial step")  (statement := /--    For any $x>0$, $$Q(x) = \sum_{k\leq x} M\left(\sqrt{\frac{x}{k}}\right)$$.  -/)  (proof := /--    We compute    $$Q(x) = \sum_{n\leq x} \sum_{d: d^2|n} \mu(d) = \sum_{k, d: k d^2\leq x} \mu(d)$$    giving the claim.  -/)  (latexEnv := "sublemma")  (discussion := 526)]theorem mobius_lemma_1_sub (x : ℝ) (hx : x > 0) :    Q x = ∑ k ∈ Ioc 0 ⌊x⌋₊, M (Real.sqrt (x / k)) := by  have h_exercise : ∑ n ∈ Ioc 0 ⌊x⌋₊, (if Squarefree n then 1 else 0) =      ∑ k ∈ Ioc 0 ⌊x⌋₊, ∑ d ∈ filter (fun d ↦ d ^ 2 ∣ k) (Nat.divisors k), (moebius d : ℤ) :=    sum_congr rfl fun n hn ↦ by      rw [← sum_sq_div_moebius_eq_squarefree n (mem_Ioc.mp hn).1]; rfl  have h_rewrite : ∑ k ∈ Ioc 0 ⌊x⌋₊, ∑ d ∈ filter (fun d ↦ d ^ 2 ∣ k) (Nat.divisors k),      (moebius d : ℤ) = ∑ d ∈ Icc 1 ⌊Real.sqrt x⌋₊, ∑ k ∈ Icc 1 ⌊x / (d ^ 2)⌋₊, (moebius d : ℤ) := by    have h_reorder : ∑ k ∈ Ioc 0 ⌊x⌋₊, ∑ d ∈ filter (fun d ↦ d ^ 2 ∣ k) (Nat.divisors k),        (moebius d : ℤ) =          ∑ d ∈ Icc 1 ⌊Real.sqrt x⌋₊, ∑ k ∈ filter (fun k ↦ d ^ 2 ∣ k) (Ioc 0 ⌊x⌋₊),            (moebius d : ℤ) := by      repeat rw [sum_sigma']      apply sum_bij (fun p hp ↦ ⟨p.snd, p.fst⟩)      · simp only [mem_sigma, mem_Ioc, mem_filter, Nat.mem_divisors, mem_Icc, and_imp] at *        exact fun a ha₁ ha₂ ha₃ ha₄ ha₅ ↦ ⟨⟨Nat.pos_of_dvd_of_pos ha₃ ha₁, Nat.le_floor <|          le_sqrt_of_sq_le <| le_trans (mod_cast Nat.le_of_dvd ha₁ ha₅) (Nat.floor_le hx.le |>            le_trans (Nat.cast_le.mpr ha₂))⟩, ⟨ha₁, ha₂⟩, ha₅⟩      · aesop      · simp only [mem_sigma, mem_Icc, mem_filter, mem_Ioc, Nat.mem_divisors, Sigma.exists,          and_imp]        exact fun b hb₁ hb₂ hb₃ hb₄ hb₅ ↦          ⟨b.snd, b.fst, ⟨⟨hb₃, hb₄⟩, ⟨dvd_of_mul_left_dvd hb₅, by grind⟩, hb₅⟩, rfl⟩      · grind    have h_div : ∀ d ∈ Icc 1 ⌊Real.sqrt x⌋₊,        filter (fun k ↦ d ^ 2 ∣ k) (Ioc 0 ⌊x⌋₊) =          image (fun m ↦ d ^ 2 * m) (Icc 1 ⌊x / (d ^ 2)⌋₊) := by      intro d hd      ext k      simp only [mem_filter, mem_Ioc, mem_image, mem_Icc]      refine ⟨fun hk ↦ ?_, ?_⟩      · obtain ⟨a, rfl⟩ := hk.2        refine ⟨a, ⟨by nlinarith [mem_Icc.mp hd], Nat.le_floor ?_⟩, rfl⟩        rw [le_div_iff₀ (by norm_cast; nlinarith [mem_Icc.mp hd])]        exact Nat.floor_le hx.le |> le_trans (mod_cast by nlinarith)      · simp only [mem_Icc, forall_exists_index, and_imp] at *        rintro m hm₁ hm₂ rfl        refine ⟨⟨by nlinarith, ?_⟩, dvd_mul_right _ _⟩        rw [Nat.le_floor_iff (by positivity), le_div_iff₀ (by norm_cast; nlinarith)] at *        norm_cast at *        simpa [mul_comm] using hm₂    simp_all only [sum_const]    exact sum_congr rfl fun i hi ↦ by      rw [card_image_of_injective _ fun a b h ↦        mul_left_cancel₀ (pow_ne_zero 2 <| Nat.ne_of_gt <| (mem_Icc.mp hi).1) h]  have h_interchange : ∑ d ∈ Icc 1 ⌊Real.sqrt x⌋₊, ∑ k ∈ Icc 1 ⌊x / (d ^ 2)⌋₊, (moebius d : ℤ) =      ∑ k ∈ Ioc 0 ⌊x⌋₊, ∑ d ∈ Icc 1 ⌊Real.sqrt (x / k)⌋₊, (moebius d : ℤ) := by    rw [sum_sigma', sum_sigma']    apply sum_bij (fun p hp ↦ ⟨p.snd, p.fst⟩)    · norm_num at *      refine fun a ha₁ ha₂ ha₃ ha₄ ↦ ⟨⟨ha₃, ha₄.trans (Nat.floor_mono <| div_le_self hx.le <|        mod_cast Nat.one_le_pow _ _ ha₁)⟩, ha₁, ?_⟩      rw [Nat.le_floor_iff (by positivity), le_div_iff₀ (by positivity)] at *      exact le_sqrt_of_sq_le (by nlinarith [mul_self_sqrt (Nat.cast_nonneg a.snd)])    · grind    · simp only [Nat.cast_nonneg, sqrt_div', mem_sigma, mem_Ioc, mem_Icc, Sigma.exists,        and_imp] at *      refine fun ⟨a, b⟩ ha hb ha' hb' ↦ ⟨b, a, ?_, rfl⟩      rw [Nat.le_floor_iff (by positivity), le_div_iff₀] at * <;> norm_num at *      · refine ⟨⟨ha', le_trans (le_mul_of_one_le_right (by positivity)          (le_sqrt_of_sq_le (mod_cast ha))) hb'⟩, ha, Nat.le_floor ?_⟩        rw [le_div_iff₀ (by positivity)]        nlinarith [mul_self_sqrt (Nat.cast_nonneg a), mul_self_sqrt (show 0 ≤ x by positivity),          sqrt_nonneg a, sqrt_nonneg x, mul_le_mul_of_nonneg_left hb' (sqrt_nonneg a),            mul_le_mul_of_nonneg_left hb' (sqrt_nonneg a)]      · positivity    · intro a ha; simp_all  simp_all only [Q, M, sum_boole, Nat.cast_id]; rfl