## Stream: new members

### Topic: fintype to finset

#### Eloi (Jul 17 2020 at 21:56):

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 (Jul 17 2020 at 22:00):

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

#### Jalex Stark (Jul 17 2020 at 22:01):

I'm not sure what you mean by recover

#### Eloi (Jul 17 2020 at 22:04):

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 (Jul 17 2020 at 22:11):

oh I misunderstood your code

#### Jalex Stark (Jul 17 2020 at 22:12):

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

#### Jalex Stark (Jul 17 2020 at 22:14):

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 (Jul 17 2020 at 22:29):

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

#### Alex J. Best (Jul 17 2020 at 23:20):

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 (Jul 17 2020 at 23:27):

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 (Jul 18 2020 at 05:33):

Nice! Thank you, I'll do so

Last updated: May 13 2021 at 05:21 UTC