theorem SchwartzMap.PoissonSummation_Lattices
  {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} [FactFact (p : Prop) : PropWrapper for adding elementary propositions to the type class systems.
Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally,
but sometimes it is very convenient to be able to use the type class system
in specific circumstances.

For example, `ZMod p` is a field if and only if `p` is a prime number.
In order to be able to find this field instance automatically by type class search,
we have to turn `p.prime` into an instance implicit assumption.

On the other hand, making `Nat.prime` a class would require a major refactoring of the library,
and it is questionable whether making `Nat.prime` a class is desirable at all.
The compromise is to add the assumption `[Fact p.prime]` to `ZMod.field`.

In particular, this class is not intended for turning the type class system
into an automated theorem prover for first-order logic.  (LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`.0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ)LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`.]
  (ΛSubmodule ℤ (EuclideanSpace ℝ (Fin d)) :
    SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations.
This is a sufficient condition for the subset of vectors in the submodule
to themselves form a module.  ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).

      (EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)))
  [DiscreteTopologyDiscreteTopology.{u_2} (α : Type u_2) [t : TopologicalSpace α] : PropA topological space is discrete if every set is open, that is,
its topology equals the discrete topology `⊥`.  ↥ΛSubmodule ℤ (EuclideanSpace ℝ (Fin d))] [IsZLatticeIsZLattice.{u_1, u_2} (K : Type u_1) [NormedField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E]
  (L : Submodule ℤ E) [DiscreteTopology ↥L] : Prop`L : Submodule ℤ E` where `E` is a vector space over a normed field `K` is a `ℤ`-lattice if
it is discrete and spans `E` over `K`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  ΛSubmodule ℤ (EuclideanSpace ℝ (Fin d))]
  (fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ :
    SchwartzMapSchwartzMap.{u_5, u_6} (E : Type u_5) (F : Type u_6) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F]
  [NormedSpace ℝ F] : Type (max u_5 u_6)A function is a Schwartz function if it is smooth and all derivatives decay faster than
any power of `‖x‖`.  (EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ))
      ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. )
  (vEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)) :
  ∑'tsum.{u_4, u_5} {α : Type u_4} {β : Type u_5} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (L : SummationFilter β := SummationFilter.unconditional β) : α`∑' i, f i` is the unconditional sum of `f` if it exists, or 0 otherwise.

More generally, if `L` is a `SummationFilter`, `∑'[L] i, f i` is the sum of `f` with respect to
`L` if it exists, and `0` otherwise.

(Note that even if the unconditional sum exists, it might not be unique if the topology is not
separated. When the support of `f` is finite, we make the most reasonable choice, to use the sum
over the support. Otherwise, we choose arbitrarily an `a` satisfying `HasSum f a`. Similar remarks
apply to more general summation filters.)
 (ℓ↥Λ : ↥ΛSubmodule ℤ (EuclideanSpace ℝ (Fin d))),tsum.{u_4, u_5} {α : Type u_4} {β : Type u_5} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (L : SummationFilter β := SummationFilter.unconditional β) : α`∑' i, f i` is the unconditional sum of `f` if it exists, or 0 otherwise.

More generally, if `L` is a `SummationFilter`, `∑'[L] i, f i` is the sum of `f` with respect to
`L` if it exists, and `0` otherwise.

(Note that even if the unconditional sum exists, it might not be unique if the topology is not
separated. When the support of `f` is finite, we make the most reasonable choice, to use the sum
over the support. Otherwise, we choose arbitrarily an `a` satisfying `HasSum f a`. Similar remarks
apply to more general summation filters.)
 fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.vEuclideanSpace ℝ (Fin d) +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. ↑ℓ↥Λ)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    1 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.
        ↑(ZLattice.covolumeZLattice.covolume.{u_1} {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] (L : Submodule ℤ E)
  (μ : MeasureTheory.Measure E := by volume_tac) : ℝThe covolume of a `ℤ`-lattice is the volume of some fundamental domain; see
`ZLattice.covolume_eq_volume` for the proof that the volume does not depend on the choice of
the fundamental domain.  ΛSubmodule ℤ (EuclideanSpace ℝ (Fin d))
            MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. ) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      ∑'tsum.{u_4, u_5} {α : Type u_4} {β : Type u_5} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (L : SummationFilter β := SummationFilter.unconditional β) : α`∑' i, f i` is the unconditional sum of `f` if it exists, or 0 otherwise.

More generally, if `L` is a `SummationFilter`, `∑'[L] i, f i` is the sum of `f` with respect to
`L` if it exists, and `0` otherwise.

(Note that even if the unconditional sum exists, it might not be unique if the topology is not
separated. When the support of `f` is finite, we make the most reasonable choice, to use the sum
over the support. Otherwise, we choose arbitrarily an `a` satisfying `HasSum f a`. Similar remarks
apply to more general summation filters.)
 (m↥(LinearMap.BilinForm.dualSubmodule (innerₗ (EuclideanSpace ℝ (Fin d))) Λ) :
        ↥(LinearMap.BilinForm.dualSubmoduleLinearMap.BilinForm.dualSubmodule.{u_1, u_2, u_3} {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommRing R] [Field S]
  [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M)
  (N : Submodule R M) : Submodule R MThe dual submodule of a submodule with respect to a bilinear form. 
            (innerₗinnerₗ.{u_3} (F : Type u_3) [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] : F →ₗ[ℝ] F →ₗ[ℝ] ℝThe inner product as a bilinear map in the real case. 
              (EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)))
            ΛSubmodule ℤ (EuclideanSpace ℝ (Fin d)))),tsum.{u_4, u_5} {α : Type u_4} {β : Type u_5} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (L : SummationFilter β := SummationFilter.unconditional β) : α`∑' i, f i` is the unconditional sum of `f` if it exists, or 0 otherwise.

More generally, if `L` is a `SummationFilter`, `∑'[L] i, f i` is the sum of `f` with respect to
`L` if it exists, and `0` otherwise.

(Note that even if the unconditional sum exists, it might not be unique if the topology is not
separated. When the support of `f` is finite, we make the most reasonable choice, to use the sum
over the support. Otherwise, we choose arbitrarily an `a` satisfying `HasSum f a`. Similar remarks
apply to more general summation filters.)

        FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  ⇑fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ ↑m↥(LinearMap.BilinForm.dualSubmodule (innerₗ (EuclideanSpace ℝ (Fin d))) Λ) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
          Complex.expComplex.exp (z : ℂ) : ℂThe complex exponential function, defined via its Taylor series 
            (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.2 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. ↑Real.piReal.pi : ℝThe number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2],
from which one can derive all its properties. For explicit bounds on π,
see `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened.  *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. Complex.IComplex.I : ℂThe imaginary unit.  *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
              ↑(RCLike.wInnerRCLike.wInner.{u_1, u_3, u_4} {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜]
  [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ) (f g : (i : ι) → E i) : 𝕜Weighted inner product giving rise to the L2 norm, denoted as `⟪g, f⟫_[𝕜, w]`.  1 vEuclideanSpace ℝ (Fin d).ofLpWithLp.ofLp.{u_1} {p : ENNReal} {V : Type u_1} (self : WithLp p V) : VConverts an element of `WithLp p V` to an element of `V`. 
                  (↑m↥(LinearMap.BilinForm.dualSubmodule (innerₗ (EuclideanSpace ℝ (Fin d))) Λ)).ofLpWithLp.ofLp.{u_1} {p : ENNReal} {V : Type u_1} (self : WithLp p V) : VConverts an element of `WithLp p V` to an element of `V`. ))HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.