Poisson Summation Formula

Stream: Sphere packing in 8 dimensions

[Yongxi Lin (Aaron)]

This thread is intended for discussing any issues related to the formalization of the Poisson Summation Formula.

[Yongxi Lin (Aaron)]

An important identity used in the proof of this formula is

$$\int_{\mathbb{T}^d}f(x)dx=\int_{(0,1]^d}f(x)dx,$$

which basically says that integrating over UnitAddTorus d is the same as integrating over the box. In order to show this, we need a measurable equivalence between UnitAddTorus dand univ.pi (fun i => Ioc 0 1). At this point, I am unsure about what I should do. What is the correct way of proving this equivalence? In 1d, we have QuotientAddGroup.equivIocMod, so I suppose we should take advantage of sth like MeasurableEquiv.piCongrRight.

import Mathlib

open Set Algebra Submodule MeasureTheory UnitAddTorus FourierTransform Asymptotics Topology Real
  Filter ContinuousMap ZLattice Submodule WithLp

variable {d : Type*} [Fintype d] {E : Type} [NormedAddCommGroup E] [NormedSpace ℂ E]

def equivPiIoc (a : d → ℝ) : UnitAddTorus d ≃ univ.pi (fun i => Ioc (a i) (a i + 1)) := sorry

noncomputable def measurableEquivPiIoc (a : d → ℝ) :
    UnitAddTorus d ≃ᵐ univ.pi fun i => Ioc (a i) (a i + 1) where
  toEquiv := sorry
  measurable_toFun := sorry
  measurable_invFun := sorry

theorem integral_preimage (f : UnitAddTorus d → E) (n : d → ℤ) (a : d → ℝ) :
    ∫ x : UnitAddTorus d, f x =
    ∫ (x : d → ℝ) in univ.pi fun i => Ioc (a i) (a i + 1), f (fun i => x i) := by
  sorry

theorem mFourierCoeff_eq_Integral (f : UnitAddTorus d → E) (n : d → ℤ) (a : d → ℝ) :
    mFourierCoeff f n =
    ∫ (x : d → ℝ) in univ.pi fun i => Ioc (a i) (a i + 1),
    mFourier (-n) (fun i => x i) • f (fun i => x i) := by
  sorry

[Cameron Freer]

Yongxi Lin (Aaron) said:

At this point, I am unsure about what I should do. What is the correct way of proving this equivalence? In 1d, we have QuotientAddGroup.equivIocMod, so I suppose we should take advantage of sth like MeasurableEquiv.piCongrRight.

I played with this a bit -- my sense is that the target type univ.pi (fun i => Ioc (a i) (a i + 1)) unfolds to {f : d → ℝ // ∀ i ∈ univ, f i ∈ Ioc (a i) (a i + 1)}, while Equiv.subtypePiEquivPi has the shape Equiv.subtypePiEquivPi : {f // ∀ a, p a (f a)} ≃ (∀ a, {b // p a b}).

So Equiv.subtypePiEquivPi.symm produces (∀ i, {x // x ∈ Ioc (a i) (a i + 1)}) ≃ {f // ∀ i, f i ∈ Ioc (a i) (a i + 1)} but univ.pi has the predicate {f // ∀ i ∈ univ, f i ∈ Ioc ...}

Because i ∈ univ is always true, the following are propositionally equivalent but not defeq, and so I couldn't get the composition accepted directly:

- subtypePiEquivPi.symm gives: ∀ i, f i ∈ Ioc ...
- univ.pi requires: ∀ i, i ∈ univ → f i ∈ Ioc ...

Instead, I was able to get Equiv.setCongr to work with a small helper lemma that uses Set.mem_univ_pi:

  private lemma pi_eq (a : d → ℝ) :
      {f : d → ℝ | ∀ i, f i ∈ Ioc (a i) (a i + 1)} = univ.pi (fun i => Ioc (a i) (a i + 1)) := by
    ext; simp

  noncomputable def equivPiIoc (a : d → ℝ) :
      UnitAddTorus d ≃ univ.pi (fun i => Ioc (a i) (a i + 1)) :=
    (Equiv.piCongrRight fun i => AddCircle.equivIoc 1 (a i)).trans <|
      Equiv.subtypePiEquivPi.symm.trans <|
        Equiv.setCongr (pi_eq a)

(Initially I had tried a direct construction like:

  noncomputable def equivPiIoc (a : d → ℝ) :
      UnitAddTorus d ≃ univ.pi (fun i => Ioc (a i) (a i + 1)) where
    toFun x := ⟨fun i => (AddCircle.equivIoc 1 (a i) (x i)).val,
                fun i _ => (AddCircle.equivIoc 1 (a i) (x i)).prop⟩
    invFun y := fun i => (AddCircle.equivIoc 1 (a i)).symm ⟨y.val i, y.prop i trivial⟩
    left_inv x := by ext i; simp
    right_inv y := by ext i; simp

)

[Cameron Freer]

and after that, something like the following worked for the measurable version:

  noncomputable def measurableEquivPiIoc (a : d → ℝ) :
      UnitAddTorus d ≃ᵐ univ.pi fun i => Ioc (a i) (a i + 1) where
    toEquiv := equivPiIoc a
    measurable_toFun := by
      refine Measurable.subtype_mk ?_
      exact measurable_pi_lambda _ fun i =>
        (AddCircle.measurableEquivIoc 1 (a i)).measurable.subtype_val.comp (measurable_pi_apply i)
    measurable_invFun := by
      refine measurable_pi_lambda _ fun i => ?_
      have h1 : Measurable (fun (y : univ.pi fun j => Ioc (a j) (a j + 1)) => y.val) :=
        measurable_subtype_coe
      have h2 : Measurable (fun (f : d → ℝ) => f i) := measurable_pi_apply i
      have h3 : Measurable (fun (y : univ.pi fun j => Ioc (a j) (a j + 1)) => y.val i) :=
        h2.comp h1
      have h4 : Measurable fun (y : univ.pi fun j => Ioc (a j) (a j + 1)) =>
          (⟨y.val i, y.prop i trivial⟩ : Ioc (a i) (a i + 1)) :=
        Measurable.subtype_mk h3
      exact (AddCircle.measurableEquivIoc 1 (a i)).symm.measurable.comp h4

[Cameron Freer]

I also got Equiv.subtypeEquivRight to handle it directly:

  noncomputable def equivPiIoc (a : d → ℝ) :
      UnitAddTorus d ≃ univ.pi (fun i => Ioc (a i) (a i + 1)) :=
    (Equiv.piCongrRight fun i => AddCircle.equivIoc 1 (a i)).trans <|
      Equiv.subtypePiEquivPi.symm.trans <|
        Equiv.subtypeEquivRight (fun _ => by simp)

[Yongxi Lin (Aaron)]

@Cameron Freer Thank you for your reply and your code. Indeed there are many way to represent the box $\prod_{i=1}^n(a_i,a_i+1]$, do you think it will be easier to prove the results I want by using {f : d → ℝ // ∀ i ∈ univ, f i ∈ Ioc (a i) (a i + 1)}?

[Cameron Freer]

Yongxi Lin (Aaron) said:

Indeed there are many way to represent the box $\prod_{i=1}^n(a_i,a_i+1]$, do you think it will be easier to prove the results I want by using {f : d → ℝ // ∀ i ∈ univ, f i ∈ Ioc (a i) (a i + 1)}?

That should be defeq to univ.pi (fun i => Ioc (a i) (a i + 1)) and seems likely fine to me for using lemmas like MeasureTheory.MeasurePreserving.integral_comp' and AddCircle.measurePreserving_equivIoc.

[Yongxi Lin (Aaron)]

#34636: shows that $\int_{\mathbb{T}^d}f(x)dx=\int_{(0,1]^d}f(x)dx$, and in particular we can use this formula to compute the fourier coefficients by integrating over a box: $\hat{f}(n)=\int_{(0,1]^d}e^{2\pi i(n \cdot x)}f(x)dx$.