8. Fourier Eigenfunctions with Double Zeroes
First we define the function a. To this end, we consider the following
functions.
- No associated Lean code or declarations.
Define
\phi_{-4} := \frac{E_4^2}{\Delta}
\phi_{-2} := \frac{E_4(E_2 E_4 - E_6)}{\Delta}
\phi_{0} := \frac{(E_2 E_4 - E_6)^2}{\Delta}.
Uses Definition 7.13 and Definition 7.17.
The function \phi_0(z) is not modular; however, it satisfies the following
transformation rules.
- No associated Lean code or declarations.
We have
\phi_0(z + 1) = \phi_0(z)
\phi_0\left(-\frac{1}{z}\right) = \phi_0(z)-\frac{12i}{\pi}\,\frac{1}{z}\,\phi_{-2}(z)-\frac{36}{\pi^2}\,\frac{1}{z^2}\,\phi_{-4}(z).
Uses Definition 8.1, Lemma 7.14, Lemma 7.18, and Lemma 7.23.
Equation \phi_0(z + 1) = \phi_0(z) follows easily from periodicity of the
Eisenstein series and of \Delta(z). For the second transformation law,
\phi_{0}\left(-\frac{1}{z}\right) = \frac{(E_2(-1/z) E_4(-1/z) - E_6(-1/z))^{2}}{\Delta(-1/z)}
= \frac{((z^2 E_2(z) - 6iz / \pi) \cdot z^4 E_4(z) - z^6 E_6(z))^{2}}{z^{12} \Delta(z)}
= \frac{\left(E_2(z) E_4(z) - E_6(z) - \frac{6i}{\pi z} E_4(z)\right)^2}{\Delta(z)}
= \frac{(E_2(z) E_4(z) - E_6(z))^{2} - \frac{12i}{\pi z}(E_2(z) E_4(z) - E_6(z)) E_4(z) - \frac{36}{\pi^2 z^2} E_4(z)^{2}}{\Delta(z)}
= \phi_0(z) - \frac{12 i}{\pi z} \phi_{-2}(z) - \frac{36}{\pi^2 z^2} \phi_{-4}(z).
For our formalization, we choose rectangular contours for the first and second integrals, and write the definition as follows.
-
MagicFunction.a.RealIntegrals.a'[complete] -
MagicFunction.a.RadialFunctions.a[complete]
Define a_{\rad} : \R \to \C by
a_\rad(r) := I_1(r) + I_2(r) + I_3(r) + I_4(r) + I_5(r) + I_6(r)
where
I_1(r) := \int_{-1}^{-1 + i} \phi_0 \left(\frac{-1}{z+1}\right) (z + 1)^2 e^{\pi i r z} \dd z
I_2(r) := \int_{-1 + i}^{i} \phi_0 \left(\frac{-1}{z+1}\right) (z + 1)^2 e^{\pi i r z} \dd z
I_3(r) := \int_{1}^{1 + i} \phi_0 \left(\frac{-1}{z-1}\right) (z - 1)^2 e^{\pi i r z} \dd z
I_4(r) := \int_{1 + i}^{i} \phi_0 \left(\frac{-1}{z-1}\right) (z - 1)^2 e^{\pi i r z} \dd z
I_5(r) := -2 \int_{0}^{i} \phi_0 \left(\frac{-1}{z}\right) z^2 e^{\pi i r z} \dd z
I_6(r) := 2 \int_{i}^{i\infty} \phi_0(z) e^{\pi i r z} \dd z.
Here all contours are chosen to be straight line segments. Define
a(x) := a_{\rad}(\|x\|^2) for x \in \R^8.
Uses Definition 8.1.
Lean code for Definition8.3●2 definitions
Associated Lean declarations
-
MagicFunction.a.RealIntegrals.a'[complete]
-
MagicFunction.a.RadialFunctions.a[complete]
-
MagicFunction.a.RealIntegrals.a'[complete] -
MagicFunction.a.RadialFunctions.a[complete]
-
def MagicFunction.a.RealIntegrals.a' : ℝ
Real : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.→ ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.def MagicFunction.a.RealIntegrals.a' : ℝ
Real : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.→ ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. -
def MagicFunction.a.RadialFunctions.a : EuclideanSpace
EuclideanSpace.{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.8) → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.def MagicFunction.a.RadialFunctions.a : EuclideanSpace
EuclideanSpace.{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.8) → ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.
In the original paper, the integrals I_1 and I_2 are combined, as are
I_3 and I_4. We write them separately to simplify the formalization.
Now we prove that a satisfies condition eqn:a-fourier.
The following lemma will be used to prove Schwartzness of both a and
b.
Let f(z) be a holomorphic function with Fourier expansion
f(z) = \sum_{n \ge n_0} c_f(n) e^{\pi i n z}
with c_f(n_0) \ne 0. Assume that c_f(n) has polynomial growth, that is,
|c_f(n)| = O(n^k) for some k \in \N. Then there exists a constant
C_f > 0 such that
\left|\frac{f(z)}{\Delta(z)}\right| \le C_f e^{-\pi (n_0 - 2) \Im z}
for all z with \Im z > 1/2.
Lean code for Lemma8.4●1 theorem
Associated Lean declarations
-
theorem MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff (z
UpperHalfPlane: UpperHalfPlaneUpperHalfPlane : TypeThe open upper half plane, denoted as `ℍ` within the `UpperHalfPlane` namespace) (hz1 / 2 < z.im: 1 / 2 <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`.zUpperHalfPlane.imUpperHalfPlane.im (z : UpperHalfPlane) : ℝImaginary part) (cℤ → ℂ: ℤ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).→ ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.) (n₀ℤ: ℤ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).) (hcsumSummable fun i ↦ MagicFunction.PolyFourierCoeffBound.fouterm c (↑z) (↑i + n₀): SummableSummable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) : Prop`Summable f` means that `f` has some (infinite) sum with respect to `L`. Use `tsum` to get the value.fun iℕ↦ MagicFunction.PolyFourierCoeffBound.foutermMagicFunction.PolyFourierCoeffBound.fouterm (coeff : ℤ → ℂ) (x : ℂ) (i : ℤ) : ℂcℤ → ℂ(↑zUpperHalfPlane) (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`.↑iℕ+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`.n₀ℤ)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`.) (kℕ: ℕ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.) (hpolyc =O[Filter.atTop] fun n ↦ ↑n ^ k: cℤ → ℂ=O[Asymptotics.IsBigO.{u_18, u_19, u_20} {α : Type u_18} {E : Type u_19} {F : Type u_20} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : PropThe Landau notation `f =O[l] g` where `f` and `g` are two functions on a type `α` and `l` is a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by a constant multiple of `‖g‖`. In other words, `‖f‖ / ‖g‖` is eventually bounded, modulo division by zero issues that are avoided by this definition.Filter.atTopFilter.atTop.{u_3} {α : Type u_3} [Preorder α] : Filter α`atTop` is the filter representing the limit `→ ∞` on an ordered set. It is generated by the collection of up-sets `{b | a ≤ b}`. (The preorder need not have a top element for this to be well defined, and indeed is trivial when a top element `x` exists, i.e., it coincides with `pure x`.)]Asymptotics.IsBigO.{u_18, u_19, u_20} {α : Type u_18} {E : Type u_19} {F : Type u_20} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : PropThe Landau notation `f =O[l] g` where `f` and `g` are two functions on a type `α` and `l` is a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by a constant multiple of `‖g‖`. In other words, `‖f‖ / ‖g‖` is eventually bounded, modulo division by zero issues that are avoided by this definition.fun nℤ↦ ↑nℤ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `^` in identifiers is `pow`.kℕ) (fUpperHalfPlane → ℂ: UpperHalfPlaneUpperHalfPlane : TypeThe open upper half plane, denoted as `ℍ` within the `UpperHalfPlane` namespace→ ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.) (hf∀ (x : UpperHalfPlane), f x = ∑' (n : ℕ), MagicFunction.PolyFourierCoeffBound.fouterm c (↑x) (↑n + n₀): ∀ (xUpperHalfPlane: UpperHalfPlaneUpperHalfPlane : TypeThe open upper half plane, denoted as `ℍ` within the `UpperHalfPlane` namespace), fUpperHalfPlane → ℂxUpperHalfPlane=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`.∑'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.)(nℕ: ℕ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.),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.)MagicFunction.PolyFourierCoeffBound.foutermMagicFunction.PolyFourierCoeffBound.fouterm (coeff : ℤ → ℂ) (x : ℂ) (i : ℤ) : ℂcℤ → ℂ(↑xUpperHalfPlane) (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`.↑nℕ+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`.n₀ℤ)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`.) : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.fUpperHalfPlane → ℂzUpperHalfPlane/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`.ΔΔ (z : UpperHalfPlane) : ℂzUpperHalfPlane‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` Conventions for notations in identifiers: * The recommended spelling of `≤` in identifiers is `le`. * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).MagicFunction.PolyFourierCoeffBound.DivDiscBoundMagicFunction.PolyFourierCoeffBound.DivDiscBound (c : ℤ → ℂ) (n₀ : ℤ) : ℝcℤ → ℂn₀ℤ*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.expReal.exp (x : ℝ) : ℝThe real exponential function, defined as the real part of the complex exponential(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`.-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator).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`.(HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).↑n₀ℤ-HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).2)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).*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`.zUpperHalfPlane.imUpperHalfPlane.im (z : UpperHalfPlane) : ℝImaginary part)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`.theorem MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff (z
UpperHalfPlane: UpperHalfPlaneUpperHalfPlane : TypeThe open upper half plane, denoted as `ℍ` within the `UpperHalfPlane` namespace) (hz1 / 2 < z.im: 1 / 2 <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`.zUpperHalfPlane.imUpperHalfPlane.im (z : UpperHalfPlane) : ℝImaginary part) (cℤ → ℂ: ℤ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).→ ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.) (n₀ℤ: ℤ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).) (hcsumSummable fun i ↦ MagicFunction.PolyFourierCoeffBound.fouterm c (↑z) (↑i + n₀): SummableSummable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) : Prop`Summable f` means that `f` has some (infinite) sum with respect to `L`. Use `tsum` to get the value.fun iℕ↦ MagicFunction.PolyFourierCoeffBound.foutermMagicFunction.PolyFourierCoeffBound.fouterm (coeff : ℤ → ℂ) (x : ℂ) (i : ℤ) : ℂcℤ → ℂ(↑zUpperHalfPlane) (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`.↑iℕ+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`.n₀ℤ)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`.) (kℕ: ℕ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.) (hpolyc =O[Filter.atTop] fun n ↦ ↑n ^ k: cℤ → ℂ=O[Asymptotics.IsBigO.{u_18, u_19, u_20} {α : Type u_18} {E : Type u_19} {F : Type u_20} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : PropThe Landau notation `f =O[l] g` where `f` and `g` are two functions on a type `α` and `l` is a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by a constant multiple of `‖g‖`. In other words, `‖f‖ / ‖g‖` is eventually bounded, modulo division by zero issues that are avoided by this definition.Filter.atTopFilter.atTop.{u_3} {α : Type u_3} [Preorder α] : Filter α`atTop` is the filter representing the limit `→ ∞` on an ordered set. It is generated by the collection of up-sets `{b | a ≤ b}`. (The preorder need not have a top element for this to be well defined, and indeed is trivial when a top element `x` exists, i.e., it coincides with `pure x`.)]Asymptotics.IsBigO.{u_18, u_19, u_20} {α : Type u_18} {E : Type u_19} {F : Type u_20} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : PropThe Landau notation `f =O[l] g` where `f` and `g` are two functions on a type `α` and `l` is a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by a constant multiple of `‖g‖`. In other words, `‖f‖ / ‖g‖` is eventually bounded, modulo division by zero issues that are avoided by this definition.fun nℤ↦ ↑nℤ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `^` in identifiers is `pow`.kℕ) (fUpperHalfPlane → ℂ: UpperHalfPlaneUpperHalfPlane : TypeThe open upper half plane, denoted as `ℍ` within the `UpperHalfPlane` namespace→ ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.) (hf∀ (x : UpperHalfPlane), f x = ∑' (n : ℕ), MagicFunction.PolyFourierCoeffBound.fouterm c (↑x) (↑n + n₀): ∀ (xUpperHalfPlane: UpperHalfPlaneUpperHalfPlane : TypeThe open upper half plane, denoted as `ℍ` within the `UpperHalfPlane` namespace), fUpperHalfPlane → ℂxUpperHalfPlane=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`.∑'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.)(nℕ: ℕ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.),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.)MagicFunction.PolyFourierCoeffBound.foutermMagicFunction.PolyFourierCoeffBound.fouterm (coeff : ℤ → ℂ) (x : ℂ) (i : ℤ) : ℂcℤ → ℂ(↑xUpperHalfPlane) (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`.↑nℕ+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`.n₀ℤ)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`.) : ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.fUpperHalfPlane → ℂzUpperHalfPlane/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`.ΔΔ (z : UpperHalfPlane) : ℂzUpperHalfPlane‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` Conventions for notations in identifiers: * The recommended spelling of `≤` in identifiers is `le`. * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).MagicFunction.PolyFourierCoeffBound.DivDiscBoundMagicFunction.PolyFourierCoeffBound.DivDiscBound (c : ℤ → ℂ) (n₀ : ℤ) : ℝcℤ → ℂn₀ℤ*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.expReal.exp (x : ℝ) : ℝThe real exponential function, defined as the real part of the complex exponential(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`.-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator).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`.(HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).↑n₀ℤ-HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).2)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`. The meaning of this notation is type-dependent. * For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).*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`.zUpperHalfPlane.imUpperHalfPlane.im (z : UpperHalfPlane) : ℝImaginary part)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`.
When f(z) is a quasi-modular form, we can take k to be the weight of
f.
By the product formula for \Delta,
\left|\frac{f(z)}{\Delta(z)}\right|
= \left|\frac{\sum_{n \ge n_0} c_f(n) e^{\pi i n z}}{e^{2 \pi i z}\prod_{n \ge 1} (1 - e^{2\pi i n z})^{24}}\right|
= |e^{\pi i (n_0 - 2)z}| \cdot \frac{|\sum_{n \ge n_0} c_f(n) e^{\pi i (n - n_0) z}|}{\prod_{n \ge 1} |1 - e^{2\pi i n z}|^{24}}
\le e^{-\pi (n_0 - 2) \Im z} \cdot \frac{\sum_{n \ge n_0} |c_f(n)| e^{-\pi (n - n_0) \Im z}}{\prod_{n \ge 1} (1 - e^{- 2\pi n \Im z})^{24}}
\le e^{-\pi (n_0 - 2) \Im z} \cdot \frac{\sum_{n \ge n_0} |c_f(n)| e^{-\pi (n - n_0) / 2}}{\prod_{n \ge 1} (1 - e^{-\pi n})^{24}}
= C_f \cdot e^{-\pi (n_0 - 2) \Im z}.
Here
C_f = \frac{\sum_{n \ge n_0} |c_f(n)| e^{-\pi (n - n_0) / 2}}{\prod_{n \ge 1} (1 - e^{-\pi n})^{24}}.
The numerator converges absolutely because of polynomial growth, and the
denominator also converges; indeed it is simply e^{\pi}\cdot \Delta(i/2).
Uses Definition 7.22.
As corollaries, we obtain the following bounds for \phi_0,
\phi_{-2}, and \phi_{-4}.
- No associated Lean code or declarations.
There exists a constant C_0 > 0 such that
|\phi_0(z)| \le C_0 e^{-2 \pi \Im z}
for all z with \Im z > 1/2.
Uses Theorem 7.48, Lemma 8.4, Lemma 7.16, and Lemma 7.15.
By Ramanujan's formula,
E_2 E_4 - E_6 = 3E_4' = 720 \sum_{n \ge 1} n \sigma_3(n) e^{2 \pi i n z},
and
(E_2(z) E_4(z) - E_6(z))^{2} = 720^{2} e^{4 \pi i z} + O(e^{5 \pi i z}).
The result then follows from Lemma Lemma 8.4 with
f(z) = (E_2 E_4 - E_6)^2 and n_0 = 4.
- No associated Lean code or declarations.
There exists a constant C_{-2} > 0 such that
|\phi_{-2}(z)| \le C_{-2}
for all z with \Im z > 1/2.
Uses Definition 8.1, Lemma 8.4, and Lemma 7.16.
- No associated Lean code or declarations.
There exists a constant C_{-4} > 0 such that
|\phi_{-4}(z)| \le C_{-4} e^{2 \pi \Im z}
for all z with \Im z > 1/2.
Uses Definition 8.1, Lemma 8.4, and Lemma 7.16.
Note that we can take the constants C_0, C_{-2}, and C_{-4} as
C_0 = 9 \cdot 240^2 \cdot e^{\pi} \cdot \frac{E_4'(i/2)^{2}}{\Delta(i/2)}
C_{-2} = 3 \cdot \frac{E_4(i/2) E_4'(i/2)}{\Delta(i/2)}
C_{-4} = e^{-\pi} \cdot \frac{E_4(i/2)^{2}}{\Delta(i/2)}.
- No associated Lean code or declarations.
For all n \in \N, there exists a constant C' such that for all
r \geq 0,
r^n \cdot \int_{1}^{\infty} e^{-2\pi s} \, e^{-\pi r /s} \, \dd s \leq C'.
Fix n \in \N. There exists a constant C such that for all x \ge 0,
|x|^n \cdot |e^{-\pi x}| \le C.
In particular, for all r \ge 0 and s \ge 1,
r^n \cdot e^{-\pi r/s} \le C s^n.
Hence
r^n \cdot \int_{1}^{\infty} e^{-2\pi s} \, e^{-\pi r /s} \, \dd{s}
= \int_{1}^{\infty} e^{-2\pi s} \, \left(|r|^n \cdot e^{-\pi r /s}\right) \, \dd{s}
\leq C \int_{1}^{\infty} e^{-2\pi s} \, s^n \, \dd{s}.
The Gamma function is given by
\Gamma(x) = \int_{0}^{\infty} e^{-u} \, u^{x-1} \, \dd{u}
for all x > 0. Writing u = 2\pi s and using
\Gamma(n+1) = n!, we obtain
C \int_{1}^{\infty} e^{-2\pi s} \, s^n \, \dd{s}
\leq C \int_{0}^{\infty} e^{-2\pi s} \, s^n \, \dd{s}
= C \int_{0}^{\infty} \frac{1}{(2\pi)^{n+1}} e^{-u} \, u^n \, \dd{u}
= \frac{C \cdot n!}{(2\pi)^n}.
Defining C' := \frac{C \cdot n!}{(2\pi)^n} finishes the proof.
- No associated Lean code or declarations.
There exists a constant C > 0 such that for all r \geq 0,
|I_1(r)|, |I_3(r)|, |I_5(r)| \leq C \int_1^{\infty} e^{-2\pi s} \, e^{-\pi r / s} \, \dd s.
We prove the bound only for I_1(r), as the others are similar.
With the change of variable z = -1 + i t for t \in [0,1], we have
I_1(r) = -i \int_0^1 \phi_0\left(\frac{-1}{i t}\right) t^2 e^{-\pi i r} \cdot e^{-\pi r t} \, \dd t.
With the change of variable s = 1 / t, this becomes
I_1(r) = i \int_1^{\infty} \phi_0(i s) \cdot s^{-4} \cdot e^{-\pi i r} \cdot e^{-\pi r / s} \, \dd s,
so
|I_1(r)| \leq \int_1^{\infty} |\phi_0(i s)| \cdot s^{-4} \cdot |e^{-\pi i r}| \cdot e^{-\pi r / s} \, \dd s
\le \int_1^{\infty} |\phi_0(is)| \cdot e^{-\pi r / s} \, \dd s.
By Corollary Corollary 8.5, we conclude that
|I_1(r)| \leq C_0 \int_1^{\infty} e^{-2\pi s} \, e^{-\pi r / s} \, \dd s.
- No associated Lean code or declarations.
There exist C_1, C_2 > 0 such that for all r \geq 0,
|I_2(r)|, |I_4(r)| \leq C_1 e^{-\pi r}
and
|I_6(r)| \leq C_2 \frac{e^{-\pi(r + 2)}}{r + 2}.
For I_2(r), parametrize z by z = t + i for t \in [-1,0].
Then
I_2(r) = \int_{-1}^0 \phi_0\left(\frac{-1}{t + 1 + i}\right) (t + 1 + i)^2 e^{\pi i r t} e^{-\pi r} \, \dd t.
Since the function
z \mapsto \phi_0\left(\frac{-1}{z+1}\right) (z+1)^2 is holomorphic and
bounded on the contour, there exists C > 0 such that
|\phi_0\left(\frac{-1}{z+1}\right) (z + 1)^2| \leq C,
and therefore
|I_2(r)| \le \int_{-1}^{0} C e^{-\pi r} \, \dd t = C e^{-\pi r}.
The bound for I_4(r) is similar.
/- source paragraph break -/
For I_6(r), parametrize z = i t for t \in [1, \infty), giving
I_6(r) = 2 i \int_1^{\infty} \phi_0(i t) e^{-\pi r t} \, \dd t.
Using Corollary Corollary 8.5, the absolute value is bounded by
|I_6(r)| \leq 2 \int_1^{\infty} |\phi_0(i t)| e^{-\pi r t} \, \dd t \leq \frac{2C_0}{\pi} \int_1^{\infty} e^{-2\pi t} e^{-\pi r t} \, \dd t = \frac{2C_0}{\pi} \frac{e^{-\pi (r + 2)}}{r + 2}.
Combining these bounds, one can show that a is a Schwartz function.
-
MagicFunction.FourierEigenfunctions.a[complete]
a(x) is a Schwartz function.
Uses Definition 8.3 and Corollary 8.5.
Lean code for Lemma8.11●1 definition
Associated Lean declarations
-
MagicFunction.FourierEigenfunctions.a[complete]
-
MagicFunction.FourierEigenfunctions.a[complete]
-
def MagicFunction.FourierEigenfunctions.a : SchwartzMap
SchwartzMap.{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.8)) ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.def MagicFunction.FourierEigenfunctions.a : SchwartzMap
SchwartzMap.{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.8)) ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.The +1-Fourier Eigenfunction of Viazovska's Magic Function.
By Theorem Theorem 5.8, it suffices to show that
the function is smooth and decays faster than any polynomial. Smoothness
follows from differentiation under the integral, already formalized in
mathlib. The decay follows from Lemmas Lemma 8.9 and
Lemma 8.10, together with
Lemma 8.8.
-
MagicFunction.a.Fourier.eig_a[complete]
a(x) satisfies equation eqn:a-fourier.
Uses Lemma 7.16, Definition 7.17, Definition 8.3, Lemma 5.2, and Lemma 8.11.
Lean code for Lemma8.12●1 theorem
Associated Lean declarations
-
MagicFunction.a.Fourier.eig_a[complete]
-
MagicFunction.a.Fourier.eig_a[complete]
-
theorem MagicFunction.a.Fourier.eig_a : (FourierTransform.fourierCLE
FourierTransform.fourierCLE.{u_5, u_6, u_7} (R : Type u_5) (E : Type u_6) {F : Type u_7} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [FourierTransformInv F E] [FourierPair E F] [FourierInvPair F E] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourier E F] [ContinuousFourierInv F E] : E ≃L[R] FThe Fourier transform as a continuous linear equivalence.ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.(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.8)) ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.)) MagicFunction.FourierEigenfunctions.aMagicFunction.FourierEigenfunctions.a : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂThe +1-Fourier Eigenfunction of Viazovska's Magic Function.=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`.MagicFunction.FourierEigenfunctions.aMagicFunction.FourierEigenfunctions.a : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂThe +1-Fourier Eigenfunction of Viazovska's Magic Function.theorem MagicFunction.a.Fourier.eig_a : (FourierTransform.fourierCLE
FourierTransform.fourierCLE.{u_5, u_6, u_7} (R : Type u_5) (E : Type u_6) {F : Type u_7} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [FourierTransformInv F E] [FourierPair E F] [FourierInvPair F E] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourier E F] [ContinuousFourierInv F E] : E ≃L[R] FThe Fourier transform as a continuous linear equivalence.ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.(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.8)) ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.)) MagicFunction.FourierEigenfunctions.aMagicFunction.FourierEigenfunctions.a : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂThe +1-Fourier Eigenfunction of Viazovska's Magic Function.=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`.MagicFunction.FourierEigenfunctions.aMagicFunction.FourierEigenfunctions.a : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂThe +1-Fourier Eigenfunction of Viazovska's Magic Function.
We recall that the Fourier transform of a Gaussian function is
\mathcal{F}(e^{\pi i \|x\|^2 z})(y)=z^{-4}\,e^{\pi i \|y\|^2 \,(\frac{-1}{z}) }.
Next, exchange contour integration in the z variable with Fourier
transform in the x variable in the definition of a. This is justified
because the corresponding double integral converges absolutely. In this way we
obtain
\widehat{a}(y)=\int\limits_{-1}^i\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2\,z^{-4}\,e^{\pi i \|y\|^2 \,(\frac{-1}{z})}\,dz
+\int\limits_{1}^i\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2\,z^{-4}\,e^{\pi i \|y\|^2 \,(\frac{-1}{z})}\,dz
-2\int\limits_{0}^i\phi_0\Big(\frac{-1}{z}\Big)\,z^2\,z^{-4}\,e^{\pi i \|y\|^2 \,(\frac{-1}{z})}\,dz +2\int\limits_{i}^{i\infty}\phi_0(z)\,z^{-4}\,e^{\pi i \|y\|^2 \,(\frac{-1}{z})}\,dz.
Making the change of variables w=\frac{-1}{z}, we arrive at
\widehat{a}(y)=\int\limits_{1}^i\phi_0\Big(1-\frac{1}{w-1}\Big)\,(\frac{-1}{w}+1)^2\,w^{2}\,e^{\pi i \|y\|^2 \,w}\,dw
+\int\limits_{-1}^i\phi_0\Big(1-\frac{1}{w+1}\Big)\,(\frac{-1}{w}-1)^2\,w^2\,e^{\pi i \|y\|^2 \,w}\,dw
-2\int\limits_{i \infty}^i\phi_0(w)\,e^{\pi i \|y\|^2 \,w}\,dw +2\int\limits_{i}^{0}\phi_0\Big(\frac{-1}{w}\Big)\,w^{2}\,e^{\pi i \|y\|^2 \,w}\,dw.
Since \phi_0 is 1-periodic we have
\begin{aligned}
\widehat{a}(y)\,=\,&\int\limits_{1}^i\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2\,e^{\pi i \|y\|^2 \,z}\,dz
+\int\limits_{-1}^i\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2\,e^{\pi i \|y\|^2 \,z}\,dz \\
+&2\int\limits_{i}^{i\infty}\phi_0(z)\,e^{\pi i \|y\|^2 \,z}\,dz
-2\int\limits_{0}^{i}\phi_0\Big(\frac{-1}{z}\Big)\,z^{2}\,e^{\pi i \|y\|^2 \,z}\,dz \\
\,=\,&a(y).
\end{aligned}
This finishes the proof of the proposition.
Next, we check that a has double zeroes at all \Lambda_8-lattice points
of length greater then \sqrt{2}.
Using eqn:phi0-bound, eqn:phi2-bound, and eqn:phi4-bound, we can control
the behavior of \phi_0 near 0 and i\infty.
- No associated Lean code or declarations.
We have
\phi_0\left(\frac{i}{t}\right) = O(e^{-2 \pi / t}) \quad \text{as } t \to 0
\phi_0\left(\frac{i}{t}\right) = O(t^{-2}e^{2 \pi t}) \quad \text{as } t \to \infty.
Uses Corollary 8.5, Corollary 8.6, Corollary 8.7, and Lemma 8.2.
The first estimate follows from eqn:phi0-bound with z = i/t.
For the second estimate, by eqn:phi0-trans-S,
eqn:phi2-bound, and eqn:phi4-bound,
\left|\phi_0\left(\frac{i}{t}\right)\right| \le |\phi_0(it)| + \frac{12}{\pi t} |\phi_{-2}(it)| + \frac{36}{\pi^2 t^2} |\phi_{-4}(it)|
\le C_0 e^{-2 \pi t} + \frac{12}{\pi t} \cdot C_{-2} + \frac{36}{\pi^2 t^2} \cdot C_{-4} e^{2 \pi t} = O(t^{-2}e^{2 \pi t}).
- No associated Lean code or declarations.
For r>\sqrt{2} we can express a(r) in the form
a(r)=-4\sin(\pi r^2/2)^2\,\int\limits_{0}^{i\infty}\phi_0\Big(\frac{-1}{z}\Big)\,z^2\,e^{\pi i r^2 \,z}\,dz.
Uses Corollary 8.13, Definition 8.3, and Corollary 7.26.
Denote the right-hand side by d(r).
Convergence of the integral for r > \sqrt{2} follows from
Corollary Corollary 8.13.
We can write
d(r)=\int\limits_{-1}^{i\infty-1}\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2\,e^{\pi i r^2 \,z}\,dz-
2\int\limits_{0}^{i\infty}\phi_0\Big(\frac{-1}{z}\Big)\,z^2\,e^{\pi i r^2 \,z}\,dz
+\int\limits_{1}^{i\infty+1}\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2\,e^{\pi i r^2 \,z}\,dz.
From eqn:phi0-trans-S we deduce that if r>\sqrt{2}, then
\phi_0\Big(\frac{-1}{z}\Big)\,z^2\,e^{\pi i r^2 \,z}\to 0 as
\Im(z)\to\infty. Therefore we can deform the paths of integration and
rewrite
d(r)=\int\limits_{-1}^{i}\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2\,e^{\pi i r^2 \,z}\,dz
+\int\limits_{i}^{i\infty}\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2\,e^{\pi i r^2 \,z}\,dz
-2\int\limits_{0}^{i}\phi_0\Big(\frac{-1}{z}\Big)\,z^2\,e^{\pi i r^2 \,z}\,dz
-2\int\limits_{i}^{i\infty}\phi_0\Big(\frac{-1}{z}\Big)\,z^2\,e^{\pi i r^2 \,z}\,dz
+\int\limits_{1}^{i}\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2\,e^{\pi i r^2 \,z}\,dz
+\int\limits_{i}^{i\infty}\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2\,e^{\pi i r^2 \,z}\,dz.
Now eqn:phi0-trans-S implies
\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2-2\phi_0\Big(\frac{-1}{z}\Big)\,z^2+
\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2=2\phi_0(z),
and hence
d(r)=\int\limits_{-1}^{i}\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2\,e^{\pi i r^2 \,z}\,dz
-2\int\limits_{0}^{i}\phi_0\Big(\frac{-1}{z}\Big)\,z^2\,e^{\pi i r^2 \,z}\,dz
+\int\limits_{1}^{i}\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2\,e^{\pi i r^2 \,z}\,dz
+2\int\limits_{i}^{i\infty}\phi_0(z)\,e^{\pi i r^2 \,z}\,dz=a(r).
Finally, we find another convenient integral representation for a and
compute values of a(r) at r=0 and r=\sqrt{2}.
- No associated Lean code or declarations.
For r\geq0 we have
a(r)=4i\,\sin(\pi r^2/2)^2\,\Bigg(\frac{36}{\pi^3\,(r^2-2)}-\frac{8640}{\pi^3\,r^4}+\frac{18144}{\pi^3\,r^2}
+\int\limits_0^\infty\,\left(t^2\,\phi_0\Big(\frac{i}{t}\Big)-\frac{36}{\pi^2}\,e^{2\pi t}+\frac{8640}{\pi}\,t-\frac{18144}{\pi^2}\right)\,e^{-\pi r^2 t}\,dt \Bigg).
The integral converges absolutely for all r\in\R_{\geq 0}.
Uses Lemma 8.14, Definition 8.1, Lemma 8.2, and Definition 8.3.
Uses Lemma 8.14.
Suppose that r>\sqrt{2}. Then by Proposition prop:a-double-zeros,
a(r)=4i\,\sin(\pi r^2/2)^2\,\int\limits_{0}^{\infty}\phi_0(i/t)\,t^2\,e^{-\pi r^2 t}\,dt.
From eqn:phi0-trans-S we obtain the asymptotic expansion
\phi_0(i/t)\,t^2=\frac{36}{\pi^2}\,e^{2 \pi t}-\frac{8640}{\pi}\,t+\frac{18144}{\pi^2}+O(t^2\,e^{-2\pi t})
as t\to\infty. For r>\sqrt{2},
\int\limits_0^\infty \left(\frac{36}{\pi^2}\,e^{2 \pi t}+\frac{8640}{\pi}\,t+\frac{18144}{\pi^2}\right)\,e^{-\pi r^2 t}\,dt
=\frac{36}{\pi^3\,(r^2-2)}-\frac{8640}{\pi^3\,r^4}+\frac{18144}{\pi^3\,r^2}.
Therefore the claimed identity holds for r>\sqrt{2}.
/- source paragraph break -/
On the other hand, the definition of a shows that a(r) is analytic in
a neighborhood of [0,\infty), and the asymptotic expansion above implies
that the right-hand side is also analytic there. Hence the identity holds on
the whole interval [0,\infty).
From eqn:a-another-integral we see that the values a(r) lie in
i\R for all r\in\R_{\geq0}.
-
MagicFunction.a.SpecialValues.a_zero[sorry in proof]
We have a(0) = -\frac{i}{8640}.
Uses Lemma 8.15.
Lean code for Lemma8.16●1 theorem, incomplete
Associated Lean declarations
-
MagicFunction.a.SpecialValues.a_zero[sorry in proof]
-
MagicFunction.a.SpecialValues.a_zero[sorry in proof]
-
theorem MagicFunction.a.SpecialValues.a_zero : MagicFunction.FourierEigenfunctions.a
MagicFunction.FourierEigenfunctions.a : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂThe +1-Fourier Eigenfunction of Viazovska's Magic Function.0 =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`.-8640 *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./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`.↑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.theorem MagicFunction.a.SpecialValues.a_zero : MagicFunction.FourierEigenfunctions.a
MagicFunction.FourierEigenfunctions.a : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂThe +1-Fourier Eigenfunction of Viazovska's Magic Function.0 =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`.-8640 *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./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`.↑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.
These identities follow immediately from the previous proposition.
Now we construct function b. To this end we consider the function.
- No associated Lean code or declarations.
Define
h(z) := 128 \frac{H_3(z) + H_4(z)}{H_2(z)^2}.
Uses Definition 7.32.
It is easy to see that h\in M^!_{-2}(\Gamma_0(2)). Indeed, first check
that h|_{-2}\gamma=h for all \gamma\in\Gamma_0(2). Since
\Gamma_0(2) is generated by
\left(\begin{smallmatrix}1&0\\2&1\end{smallmatrix}\right) and
\left(\begin{smallmatrix}1&1\\0&1\end{smallmatrix}\right), it suffices to
check invariance under their action, which follows immediately from the
transformation laws of the theta-null forms and eqn: h define.
Next analyze the poles of h. It is known that \theta_{10} has no zeros
in the upper half-plane, so h has poles only at the cusps. At the cusp
i\infty, this modular form has Fourier expansion
h(z)\,=\,q^{-1} + 16 - 132 q + 640 q^2 - 2550 q^3+O(q^4).
Let
I=\left(\begin{smallmatrix}1&0\\0&1\end{smallmatrix}\right),
T=\left(\begin{smallmatrix}1&1\\0&1\end{smallmatrix}\right), and
S=\left(\begin{smallmatrix}0&-1\\1&0\end{smallmatrix}\right) be elements of
\Gamma_1.
- No associated Lean code or declarations.
Define
\psi_I\,:=\,h-h|_{-2}ST
\psi_T\,:=\,\psi_I|_{-2}T
\psi_S\,:=\,\psi_I|_{-2}S.
Uses Definition 8.17.
- No associated Lean code or declarations.
\psi_I(z), \psi_S(z), and \psi_T(z) can be written as
\psi_I(z) = \frac{H_4^3 (5 H_2^2 + 5 H_2 H_4 + 2 H_4^2)}{2\Delta}
\psi_S(z) = -\frac{H_2^3 (2 H_2^2 + 5 H_2 H_4 + 5 H_4^2)}{2 \Delta}
\psi_T(z) = \frac{H_3^3 (5 H_2^2 - 5 H_2 H_3 + 2 H_3^2)}{2 \Delta}.
Uses Lemma 7.33 and Lemma 7.41.
By the transformation laws of the theta-null functions,
H_2|_{-2}ST = (-H_4)|_{-2}T = -H_3
H_3|_{-2}ST = (-H_3)|_{-2}T = -H_4
H_4|_{-2}ST = (-H_2)|_{-2}T = H_2.
Using these identities and the level-one/level-two identities, we can rewrite
\psi_I(z) as
\psi_I(z) = h(z) - h|_{-2}ST(z)
= 128 \frac{H_3 + H_4}{H_2^2} - 128 \frac{-H_4 + H_2}{H_3^2}
= 128 \frac{H_3^2 (H_3 + H_4) - H_2^2 (H_2 - H_4)}{H_2^2 H_3^2}
= 128 \frac{(H_2 + H_4)^2 (H_2 + 2 H_4) - H_2^2 (H_2 - H_4)}{H_2^2 H_3^2}
= 128 \frac{H_4(5 H_2^2 + 5 H_2 H_4 + 2 H_4^2)}{ H_2^2 H_3^2}
= \frac{H_4^3 (5 H_2^2 + 5 H_2 H_4 + 2 H_4^2)}{2\Delta}.
Applying |_{-2}S and |_{-2}T to the expression for \psi_I proves
the formulas for \psi_S and \psi_T.
- No associated Lean code or declarations.
The Fourier expansions of these functions are
\psi_I(z)\,=\,q^{-1} + 144 + O(q^{1/2})
\psi_T(z)\,=\,q^{-1} + 144 + O(q^{1/2}).
Uses Lemma 8.19.
Now we are ready to define b. Again, the definition here is slightly
different from that in Viazovska (2017), where all contours are chosen to be
straight lines.
- No associated Lean code or declarations.
Define b_\rad : \R \to \C by
b_\rad(r) := J_1(r) + J_2(r) + J_3(r) + J_4(r) + J_5(r) + J_6(r)
where
J_1(r) := \int_{-1}^{-1 + i} \psi_T(z) e^{\pi i r z} \, \dd z
J_2(r) := \int_{-1 + i}^{i} \psi_T(z) e^{\pi i r z} \, \dd z
J_3(r) := \int_{1}^{1 + i} \psi_T(z) e^{\pi i r z} \, \dd z
J_4(r) := \int_{1 + i}^{i} \psi_T(z) e^{\pi i r z} \, \dd z
J_5(r) := -2 \int_{0}^{i} \psi_I(z) e^{\pi i r z} \, \dd z
J_6(r) := -2 \int_{i}^{i \infty} \psi_S(z) e^{\pi i r z} \, \dd z.
Here all contours are straight line segments.
Define b : \R^8 \to \C by b(x) := b_\rad(\|x\|^2).
Uses Definition 8.18.
Now we prove that b is a Schwartz function and satisfies
eqn:b-fourier. As in the case of a(x), we start with an
exponential bound for \psi_S(z) and \psi_I(z).
- No associated Lean code or declarations.
There exist constants C_I, C_S, C_T > 0 such that
|\psi_I(z)| \le C_I e^{2\pi \Im z}
|\psi_T(z)| \le C_T e^{2\pi \Im z}
|\psi_S(z)| \le C_S e^{- \pi \Im z}.
Uses Corollary 8.5 and Lemma 8.4.
The proof is similar to that of Lemma cor:phi0-bound and follows
from Lemma Lemma 8.4 together with the fact that the
vanishing orders of the numerators of \psi_I, \psi_T, and \psi_S
at infinity are respectively 0, 0, and \frac{3}{2}.
- No associated Lean code or declarations.
There exists a constant C > 0 such that
|J_1(r)|, |J_3(r)|, |J_5(r)| \le C \int_1^{\infty} e^{-\pi s} e^{\pi r / s}\, \dd s.
- No associated Lean code or declarations.
There exist C_1, C_2 > 0 such that
|J_2(r)|, |J_4(r)| \le C_1 e^{-\pi r}
|J_6(r)| \le C_2 \frac{e^{\pi (r + 1)}}{r + 1}.
-
MagicFunction.FourierEigenfunctions.b[complete]
b(x) is a Schwartz function.
Uses Lemma 8.22.
Lean code for Lemma8.25●1 definition
Associated Lean declarations
-
MagicFunction.FourierEigenfunctions.b[complete]
-
MagicFunction.FourierEigenfunctions.b[complete]
-
def MagicFunction.FourierEigenfunctions.b : SchwartzMap
SchwartzMap.{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.8)) ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.def MagicFunction.FourierEigenfunctions.b : SchwartzMap
SchwartzMap.{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.8)) ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.The -1-Fourier Eigenfunction of Viazovska's Magic Function.
Uses Lemma 8.23, Lemma 8.24, and Theorem 5.8. Similar to the proof of Lemma 8.11.
-
MagicFunction.b.Fourier.eig_b[complete]
b(x) satisfies equation eqn:b-fourier.
Uses Definition 8.21, Lemma 5.2, Definition 8.18, and Lemma 8.25.
Lean code for Lemma8.26●1 theorem
Associated Lean declarations
-
MagicFunction.b.Fourier.eig_b[complete]
-
MagicFunction.b.Fourier.eig_b[complete]
-
theorem MagicFunction.b.Fourier.eig_b : (FourierTransform.fourierCLE
FourierTransform.fourierCLE.{u_5, u_6, u_7} (R : Type u_5) (E : Type u_6) {F : Type u_7} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [FourierTransformInv F E] [FourierPair E F] [FourierInvPair F E] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourier E F] [ContinuousFourierInv F E] : E ≃L[R] FThe Fourier transform as a continuous linear equivalence.ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.(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.8)) ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.)) MagicFunction.FourierEigenfunctions.bMagicFunction.FourierEigenfunctions.b : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂThe -1-Fourier Eigenfunction of Viazovska's Magic Function.=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`.-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator).MagicFunction.FourierEigenfunctions.bMagicFunction.FourierEigenfunctions.b : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂThe -1-Fourier Eigenfunction of Viazovska's Magic Function.theorem MagicFunction.b.Fourier.eig_b : (FourierTransform.fourierCLE
FourierTransform.fourierCLE.{u_5, u_6, u_7} (R : Type u_5) (E : Type u_6) {F : Type u_7} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] [FourierTransform E F] [FourierAdd E F] [FourierSMul R E F] [FourierTransformInv F E] [FourierPair E F] [FourierInvPair F E] [TopologicalSpace E] [TopologicalSpace F] [ContinuousFourier E F] [ContinuousFourierInv F E] : E ≃L[R] FThe Fourier transform as a continuous linear equivalence.ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.(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.8)) ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.)) MagicFunction.FourierEigenfunctions.bMagicFunction.FourierEigenfunctions.b : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂThe -1-Fourier Eigenfunction of Viazovska's Magic Function.=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`.-Neg.neg.{u} {α : Type u} [self : Neg α] : α → α`-a` computes the negative or opposite of `a`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `-` in identifiers is `neg` (when used as a unary operator).MagicFunction.FourierEigenfunctions.bMagicFunction.FourierEigenfunctions.b : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂThe -1-Fourier Eigenfunction of Viazovska's Magic Function.
Uses Lemma 8.12.
We repeat the argument used in the proof of Proposition
prop:a-fourier. Using the Gaussian Fourier identity and exchanging
the contour integration in z with the Fourier transform in x, we get
\mathcal{F}(b)(x)= \int\limits_{-1}^{i}\psi_T(z)\,z^{-4}\,e^{\pi i \|x\|^2 (\frac{-1}{z})}\,dz
+ \int\limits_{1}^{i}\psi_T(z)\,z^{-4}\,e^{\pi i \|x\|^2 (\frac{-1}{z})}\,dz
- 2\,\int\limits_{0}^{i}\psi_I(z)\,z^{-4}\,e^{\pi i \|x\|^2 (\frac{-1}{z})}\,dz
- 2\,\int\limits_{i}^{i\infty}\psi_S(z)\,z^{-4}\,e^{\pi i \|x\|^2 (\frac{-1}{z})}\,dz.
With the change of variables w=\frac{-1}{z}, we arrive at
\mathcal{F}(b)(x)= \int\limits_{1}^{i}\psi_T\Big(\frac{-1}{w}\Big)\,w^{2}\,e^{\pi i \|x\|^2 w}\,dw
+ \int\limits_{-1}^{i}\psi_T\Big(\frac{-1}{w}\Big)\,w^{2}\,e^{\pi i \|x\|^2 w}\,dw
- 2\,\int\limits_{i\infty}^{i}\psi_I\Big(\frac{-1}{w}\Big)\,w^{2}\,e^{\pi i \|x\|^2 w}\,dw
- 2\,\int\limits_{i}^{0}\psi_S\Big(\frac{-1}{w}\Big)\,w^{2}\,e^{\pi i \|x\|^2 w}\,dw.
Now the definitions imply
\psi_T|_{-2}S=-\psi_T
\psi_I|_{-2}S=\psi_S
\psi_S|_{-2}S=\psi_I,
so this becomes
\mathcal{F}(b)(x)= \int\limits_{1}^{i}-\psi_T(z)\,e^{\pi i \|x\|^2 z}\,dz
+ \int\limits_{-1}^{i}-\psi_T(z)\,e^{\pi i \|x\|^2 z}\,dz
+ 2\,\int\limits_{i}^{i\infty}\psi_S(z)\,e^{\pi i \|x\|^2 z}\,dz
+ 2\,\int\limits_{0}^{i}\psi_I(z)\,e^{\pi i \|x\|^2 z}\,dw.
From the definition of b, we conclude that
\mathcal{F}(b)(x)=-b(x).
Now we regard the radial function b as a function on \R_{\geq0} and
check that it has double roots at the \Lambda_8 points.
- No associated Lean code or declarations.
We have
\psi_I(it) = O(t^2 e^{\pi/t}) \quad \text{as } t \to 0
\psi_I(it) = O(e^{2 \pi t}) \quad \text{as } t \to \infty.
Uses Lemma 8.22 and Definition 8.18.
Uses Lemma 8.22.
By eqn:psiS-define,
\psi_I(it) = (it)^{-2} \psi_S\left(\frac{-1}{it}\right) = -t^{-2} \psi_S\left(\frac{i}{t}\right),
and combined with eqn:psiS-bound this gives eqn:psiI-near-0.
Equation eqn:psiI-near-infty follows from lemma:psi-bound.
- No associated Lean code or declarations.
For r>\sqrt{2}, the function b(r) can be expressed as
b(r)=-4\sin(\pi r^2/2)^2\,\int\limits_{0}^{i\infty}\psi_I(z)\,e^{\pi i r^2 \,z}\,dz.
Uses Lemma 8.20, Definition 8.18, Corollary 8.27, and Corollary 7.26.
Uses Corollary 8.27.
Denote the right-hand side by c(r).
By Corollary cor:psiI-near-0-infty, the integral converges for
r>\sqrt{2}. Rewrite it as
c(r)=\int\limits_{-1}^{i\infty-1}\psi_I(z+1)\,e^{\pi i r^2 \,z}\,dz-2\int\limits_{0}^{i\infty}\psi_I(z)\,e^{\pi i r^2 \,z}\,dz+
\int\limits_{1}^{i\infty+1}\psi_I(z-1)\,e^{\pi i r^2 \,z}\,dz.
From the Fourier expansion of \psi_I, we know that
\psi_I(z)=e^{-2\pi i z}+O(1) as \Im(z)\to\infty.
Because r^2>2, we can deform the paths of integration and write
\int\limits_{-1}^{i\infty-1}\psi_I(z+1)\,e^{\pi i r^2 \,z}\,dz=
\int\limits_{-1}^{i}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz+\int\limits_{i}^{i\infty}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz
\int\limits_{1}^{i\infty+1}\psi_I(z-1)\,e^{\pi i r^2 \,z}\,dz=
\int\limits_{-1}^{i}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz+\int\limits_{i}^{i\infty}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz.
Hence
c(r)=\int\limits_{-1}^{i}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz+\int\limits_{1}^{i}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz
-2\int\limits_{0}^{i}\psi_I(z)\,e^{\pi i r^2 \,z}\,dz
+2\int\limits_{i}^{i\infty}(\psi_T(z)-\psi_I(z))\,e^{\pi i r^2 \,z}\,dz.
Next, the functions \psi_I, \psi_T, and \psi_S satisfy
\psi_T+\psi_S=\psi_I.
Using this identity, we find
c(r)=\int\limits_{-1}^{i}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz+\int\limits_{1}^{i}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz
-2\int\limits_{0}^{i}\psi_I(z)\,e^{\pi i r^2 \,z}\,dz
-2\int\limits_{i}^{i\infty}\psi_S(z)\,e^{\pi i r^2 \,z}\,dz=b(r).
At the end of this section we find another integral representation of b(r)
for r\in\R_{\geq0} and compute special values of b.
- No associated Lean code or declarations.
For r\geq0 we have
b(r)=4i\,\sin(\pi r^2/2)^2\,\left(\frac{144}{\pi\,r^2}+\frac{1}{\pi\,(r^2-2)}+\int\limits_0^\infty\,\left(\psi_I(it)-144-e^{2\pi t}\right)\,e^{-\pi r^2 t}\,dt\right).
The integral converges absolutely for all r\in\R_{\geq 0}.
Uses Lemma 8.28, Lemma 8.20, and Definition 8.21.
Uses Lemma 8.15 and Lemma 8.28.
The proof is analogous to the proof of Proposition
prop:a-another-integral.
First suppose that r>\sqrt{2}. Then by Proposition
prop:b-double-zeros,
b(r)=4i\,\sin(\pi r^2/2)^2\,\int\limits_{0}^{\infty}\psi_I(it)\,e^{-\pi r^2 t}\,dt.
From the Fourier expansion of \psi_I we obtain
\psi_I(it)=e^{2\pi t}+144+O(e^{-\pi t})
as t\to\infty. For r>\sqrt{2},
\int\limits_0^\infty \left(e^{2\pi t}+144\right)\,e^{-\pi r^2 t}\,dt
=\frac{1}{\pi\,(r^2-2)}+\frac{144}{\pi\,r^2}.
Therefore the identity holds for r>\sqrt{2}.
/- source paragraph break -/
On the other hand, the definition of b shows that b(r) is analytic in
a neighborhood of [0,\infty), and the asymptotic expansion above implies
that the right-hand side is also analytic there. Hence the identity holds on
the whole interval [0,\infty).
From eqn:b-another-integral we see that b(r)\in i\R for all
r\in\R_{\geq 0}.
-
MagicFunction.b.SpecialValues.b_zero[sorry in proof]
We have b(0) = 0.
Uses Lemma 8.29.
Lean code for Lemma8.30●1 theorem, incomplete
Associated Lean declarations
-
MagicFunction.b.SpecialValues.b_zero[sorry in proof]
-
MagicFunction.b.SpecialValues.b_zero[sorry in proof]
-
theorem MagicFunction.b.SpecialValues.b_zero : MagicFunction.FourierEigenfunctions.b
MagicFunction.FourierEigenfunctions.b : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂThe -1-Fourier Eigenfunction of Viazovska's Magic Function.0 =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`.0theorem MagicFunction.b.SpecialValues.b_zero : MagicFunction.FourierEigenfunctions.b
MagicFunction.FourierEigenfunctions.b : SchwartzMap (EuclideanSpace ℝ (Fin 8)) ℂThe -1-Fourier Eigenfunction of Viazovska's Magic Function.0 =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`.0
These identities follow immediately from the previous proposition.