fintype to finset

Stream: new members

[Eloi]

Is it possible to convert a fintype to a finset and later recover the fintype?

I'm trying to define Theta series of a quadratic form, and I need fin 2... but the ∑ notation requires a finset...

noncomputable def Theta'(z: ℂ)(Q: quadratic_form ℤ (fin 2 → ℤ)) /-[in_upper_half_plane z] [pos_def Q]-/:
  cau_seq ℂ complex.abs :=
    ⟨λ M, ∑ m in finset.pi (fin 2) (λ n, Ico_ℤ (- M) M), exp(2 * pi * I * z * (Q m)), sorry⟩

[Jalex Stark]

you might like to use \sum m in finset.range 2

[Jalex Stark]

I'm not sure what you mean by recover

[Eloi]

Then to define a sum over ℤ² I need a sum inside a sum, right?
I mean that m is indexed by a finset, but a quadratic form has to be applied to a term of type fin 2 → ℤ

To be clear, my dream would be to be able to write something like

 ∑ m in (fin 2  →  Ico_ℤ (- M) M)

[Jalex Stark]

oh I misunderstood your code

[Jalex Stark]

I usually either use a double sum or index over the product type

[Jalex Stark]

can you post code that compiles? I'm not familiar with the parts of the library you're using, so chasing down the imports is not fun

[Eloi]

sure, I updated the first comment to make this thread more readable :)

[Alex J. Best]

import data.complex.basic
import data.real.pi
import linear_algebra.quadratic_form
open real  -- pi
open complex
open finset  -- Ico_ℤ
open cau_seq

open_locale big_operators

variable M : ℕ
noncomputable def Theta'(z: ℂ) (Q: quadratic_form ℤ (fin 2 → ℤ)) /-[in_upper_half_plane z] [pos_def Q]-/:
  cau_seq ℂ complex.abs :=
    ⟨λ M, ∑ m in finset.pi (univ : finset (fin 2)) (λ n, Ico_ℤ (- M) M), exp (2 * (real.pi : ℂ) * I * z * (Q (λ t, m t (mem_univ t)))), sorry⟩

[Alex J. Best]

actually using fintype.pi_finset instead seems nicer

noncomputable def Theta'(z: ℂ) (Q: quadratic_form ℤ (fin 2 → ℤ)) /-[in_upper_half_plane z] [pos_def Q]-/:
  cau_seq ℂ complex.abs :=
    ⟨λ M, ∑ m in fintype.pi_finset (λ a : fin 2, Ico_ℤ (- M) M), exp (2 * (real.pi : ℂ) * I * z * Q m), sorry⟩

and if I were you I think I'd separate the creation of the theta series into making a power series in q with integer coefficients, and then evaluation as a complex function!

[Eloi]

Nice! Thank you, I'll do so