lambda_pnt

@[blueprint  "lambda-pnt"  (statement := /-- We have $\sum_{n \leq x} \lambda(n) = o(x)$. -/)  (proof := /--  From the identity    $$ \lambda(n) = \sum_{d^2|n} \mu(n/d^2)$$  and summing, we have  $$ \sum_{n \leq x} \lambda(n) = \sum_{d \leq \sqrt{x}} \sum_{n \leq x/d^2} \mu(n).$$  For any $\eps>0$, we have from Proposition \ref{mu-pnt} that  $$ \sum_{n \leq x/d^2} \mu(n) = O(\eps x/d^2) + O_\eps(1)$$  and hence on summing in $d$  $$ \sum_{n \leq x} \lambda(n) = O(\eps x) + O_\eps(x^{1/2}).$$  Sending $\eps \to 0$ we obtain the claim.  -/)  (proofUses := ["mu-pnt"])  (latexEnv := "proposition")]theorem lambda_pnt : (fun x : ℝ ↦ ∑ n ∈ range ⌊x⌋₊, (-1)^(Ω n)) =o[atTop] fun x ↦ x := by  have h_lambda_pnt : (fun N : ℕ => ∑ n ∈ Finset.range N, (-1 : ℝ) ^ (Nat.factorization n).sum (fun p k => k)) =o[Filter.atTop] (fun N : ℕ => (N : ℝ)) := by    have h_lambda_pnt : (fun N : ℕ => ∑ n ∈ Finset.Icc 1 N, (-1 : ℝ) ^ (Nat.factorization n).sum (fun p k => k)) =o[Filter.atTop] (fun N : ℕ => (N : ℝ)) := by      have h_lambda_pnt : (fun N : ℕ => ∑ d ∈ Finset.Icc 1 (Nat.sqrt N), ∑ k ∈ Finset.Icc 1 (N / d^2), (μ k : ℝ)) =o[Filter.atTop] (fun N : ℕ => (N : ℝ)) := by        exact sum_mu_div_sq_isLittleO      convert h_lambda_pnt using 2;      convert sum_lambda_eq_sum_mu_div_sq _;      exact Eq.symm cardFactors_eq_sum_factorization    have h_lambda_pnt : (fun N : ℕ => ∑ n ∈ Finset.range (N + 1), (-1 : ℝ) ^ (Nat.factorization n).sum (fun p k => k)) =o[Filter.atTop] (fun N : ℕ => (N : ℝ)) := by      rw [ Asymptotics.isLittleO_iff_tendsto' ] at * <;> norm_num at *;      · convert h_lambda_pnt.add ( show Filter.Tendsto ( fun x : ℕ => ( 1 : ℝ ) / x ) Filter.atTop ( nhds 0 ) from tendsto_const_nhds.div_atTop tendsto_natCast_atTop_atTop ) using 2 <;> norm_num [ Finset.sum_Ico_eq_sum_range ];        erw [ Finset.sum_Ico_eq_sub _ _ ] <;> norm_num [ Finset.sum_range_succ' ] ; ring_nf;      · exact ⟨ 1, by aesop ⟩;      · exact ⟨ 1, by aesop ⟩;    simp_all +decide only [Finset.sum_range_succ]    have := h_lambda_pnt.sub ( show ( fun N : ℕ => ( -1 : ℝ ) ^ N.factorization.sum fun p k => k ) =o[Filter.atTop] fun N : ℕ => ( N : ℝ ) from ?_ );    · aesop;    · rw [ Asymptotics.isLittleO_iff_tendsto' ] <;> norm_num;      · exact tendsto_zero_iff_norm_tendsto_zero.mpr ( by simpa using tendsto_inv_atTop_nhds_zero_nat );      · exact ⟨ 1, fun n hn => by positivity ⟩;  have h_floor : (fun x : ℝ => ∑ n ∈ Finset.range ⌊x⌋₊, (-1 : ℝ) ^ (Nat.factorization n).sum (fun p k => k)) =o[Filter.atTop] (fun x : ℝ => (⌊x⌋₊ : ℝ)) := by    rw [ Asymptotics.isLittleO_iff_tendsto' ] at * <;> norm_num at *;    · exact h_lambda_pnt.comp <| tendsto_nat_floor_atTop;    · exact ⟨ 1, by aesop ⟩;    · exact ⟨ 1, by intros; linarith ⟩;  rw [ Asymptotics.isLittleO_iff ] at *;  intro c hc  filter_upwards [h_floor (half_pos hc), Filter.eventually_gt_atTop 1] with x hx₁ hx₂  refine le_trans ?_ (le_trans hx₁ ?_)  · norm_num [ Norm.norm ];    convert le_rfl using 2;    congr! 2;    exact Eq.symm cardFactors_eq_sum_factorization  · norm_num [ abs_of_nonneg, Nat.floor_le, hx₂.le ];    rw [ abs_of_nonneg ( by positivity ) ] ; nlinarith [ Nat.floor_le ( by positivity : 0 ≤ x ) ]