Zulip Chat Archive

Stream: new members

Topic: fintype to finset


view this post on Zulip 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

view this post on Zulip Jalex Stark (Jul 17 2020 at 22:00):

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

view this post on Zulip Jalex Stark (Jul 17 2020 at 22:01):

I'm not sure what you mean by recover

view this post on Zulip 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)

view this post on Zulip Jalex Stark (Jul 17 2020 at 22:11):

oh I misunderstood your code

view this post on Zulip Jalex Stark (Jul 17 2020 at 22:12):

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

view this post on Zulip 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

view this post on Zulip Eloi (Jul 17 2020 at 22:29):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Eloi (Jul 18 2020 at 05:33):

Nice! Thank you, I'll do so


Last updated: May 13 2021 at 05:21 UTC