Summation over squares

Stream: new members

[Yongxi Lin (Aaron)]

What is the best way to prove the following inequality?

import Mathlib

example {S : Finset ℕ} (hs : SetLike.coe S ⊆ {n | IsSquare n}) : ∑ n ∈ S, 1 / (n : ℝ) ≤ ∑' n : ℕ, 1 / (n : ℝ) ^ 2 := by sorry

Summable.sum_le_tsum cannot be directly used here. It seems like that I need to deal with some type conversion... but can this be avoided?

[Aaron Liu]

this is false as stated

[Aaron Liu]

I think you probably meant ∑' (n : ℕ), 1 / (n : ℝ) ^ 2

[Aaron Liu]

the current statement is summing the inverse squares of all real numbers

[Aaron Liu]

which doesn't converge

[Yongxi Lin (Aaron)]

Aaron Liu said:

I think you probably meant ∑' (n : ℕ), 1 / (n : ℝ) ^ 2

Yes this is what I mean, just updated my code.

[Aaron Liu]

alright here's what I came up with

import Mathlib

example {S : Finset ℕ} (hs : SetLike.coe S ⊆ {n | IsSquare n}) :
    ∑ n ∈ S, 1 / (n : ℝ) ≤ ∑' (n : ℕ), 1 / (n : ℝ) ^ 2 := by
  have hS : Set.Finite ((· ^ 2) ⁻¹' (S : Set ℕ)) := by
    refine Set.Finite.preimage (Function.Injective.injOn ?_) S.finite_toSet
    exact Nat.pow_left_injective (by decide)
  let S' := hS.toFinset
  have hS' : S'.map ⟨(· ^ 2), Nat.pow_left_injective (by decide)⟩ = S := by
    apply SetLike.coe_injective
    have h : (S : Set ℕ) ⊆ Set.range (· ^ 2) :=
      hs.trans (by simp [isSquare_iff_exists_sq, Set.subset_def])
    simpa [S', Set.image_preimage_eq_iff] using h
  rw [← hS', Finset.sum_map, Function.Embedding.coeFn_mk]
  simp only [Nat.cast_pow]
  refine Summable.sum_le_tsum S' (fun _ _ => by positivity) ?_
  simp

[Yongxi Lin (Aaron)]

Ahh I see, nice solution.

[Ruben Van de Velde]

Not sure this is better:

import Mathlib
lemma aux {n : Nat} (hn : IsSquare n) : n.sqrt ^ 2 = n := by
  obtain ⟨n, rfl⟩ := hn.exists_sq
  simp

example {S : Finset ℕ} (hs : SetLike.coe S ⊆ {n | IsSquare n}) :
    ∑ n ∈ S, 1 / (n : ℝ) ≤ ∑' (n : ℕ), 1 / (n : ℝ) ^ 2 := by
  have : ∀ n ∈ S, IsSquare n := by
    intro n hn
    exact hs hn
  have : S = (S.image Nat.sqrt).image (· ^ 2) := by
    ext n
    simp only [Finset.mem_image, exists_exists_and_eq_and]
    constructor
    · intro hn
      exact ⟨n, hn, aux <| this n hn⟩
    · rintro ⟨n, hn, rfl⟩
      rwa [aux (this n hn)]
  rw [this, Finset.sum_image (by simp)]
  simp only [Nat.cast_pow]
  refine Summable.sum_le_tsum _ ?_ ?_ <;> simp

[Vlad]

import Mathlib

open Finset in
example {s : Finset ℕ} (hs : SetLike.coe s ⊆ {n | IsSquare n}) :
∑ n ∈ s, 1 / (n : ℝ) ≤ ∑' n : ℕ, 1 / (n : ℝ) ^ 2 := by classical
  have h : {x ∈ s | x ∈ Set.range (· ^ 2)} = s
  · simp [pow_two]; intros; grind [hs ‹_› |>.choose_spec]
  rw [←h, ←image_preimage, sum_image]; simp
  apply Summable.sum_le_tsum; all_goals simp