Summation over 'some' subset of natural numbers

Stream: new members

[Anika-Roy]

image.png
Hello!
I'm trying to formalize the theorem statement here but I'm running into issues in defining that there exists some not-predefined subset of the natural number for the summation. I'm attaching my code below, which possibly has many errors. Any guidance or criticims will be great!

import Mathlib.Topology.Algebra.InfiniteSum.Real
open BigOperators

/--
**Proposition**
Let `1 ≤ x < ∑' n, 1 / (n^2 : ℝ)`.
Then there exists a set `A ⊆ ℕ` such that `∑' n in A, 1 / (n^2 : ℝ) = x`.
-/
theorem subseriesDenseInBasel
    (x : ℝ)
    (h1 : 1 ≤ x)
    (h2 : x < ∑' n, (1 : ℝ) / (n : ℝ)^2) :
    ∃ A : Set ℕ, ∑' n in A, (1 : ℝ) / (n : ℝ)^2 = x := by
  sorry

[Ruben Van de Velde]

∑' n : A seems to parse, at least

[Ruben Van de Velde]

$A$ may legitimately be an infinite set here, right?

[Jireh Loreaux]

Indeed, for all but countably many values of x, A must be an infinite set.

[Aaron Liu]

It looks like docs#tsum doesn't support summing over Props, so ∑' n ∈ A, ... fails.

[Edward van de Meent]

you could write ∑' n, ∑ᶠ (_ : n ∈ A), (1 : ℝ) / (n : ℝ)^2 to skip the usual computability assumptions

[Edward van de Meent]

i believe the api is less than awesome tho