9. Proof of the Optimal Function Inequalities
- No associated Lean code or declarations.
Consider the function A:(0,\infty)\to\C defined as
A(t):=-t^2\phi_0(i/t)-\frac{36}{\pi^2}\,\psi_I(it).
Then
A(t) < 0
for all t > 0.
Uses Lemma 9.5, Lemma 9.4, Lemma 9.6, and Corollary 9.7.
- No associated Lean code or declarations.
Consider the function B:(0,\infty)\to\C defined as
B(t) := -t^2\phi_0(i/t)+\frac{36}{\pi^2}\,\psi_I(it).
Then
B(t) > 0
for all t > 0.
Uses Lemma 9.5, Lemma 9.4, and Corollary 9.13.
Here we formalize the proof of the inequalities by Lee (2024). First, we can rewrite the first inequality as follows.
Define two quasi-modular forms by
F(z) = (E_2(z) E_4(z) - E_6(z))^2
G(z) = H_2(z)^{3} (2 H_{2}(z)^{2} + 5 H_{2}(z) H_{4}(z) + 5 H_{4}(z)^{2}).
Uses Definition 7.17, Definition 7.13, and Definition 7.32.
Lean code for Definition9.3●2 definitions
-
def F : UpperHalfPlane
UpperHalfPlane : 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`.def F : UpperHalfPlane
UpperHalfPlane : 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`.Definition of $F$ and $G$ and auxiliary functions for the inequality between them on the imaginary axis.
-
def G (τ
UpperHalfPlane: 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`.def G (τ
UpperHalfPlane: 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`.
- No associated Lean code or declarations.
We have
\phi_0 = \frac{F}{\Delta}
\psi_S = -\frac{1}{2} \frac{G}{\Delta}.
Uses Definition 9.3 and Lemma 8.19.
Equation eqn:phi0-F is clear. Equation eqn:psiS-G is already shown in
Lemma Lemma 8.19.
- No associated Lean code or declarations.
Inequality eqn:ineqA and eqn:ineqB are equivalent to
F(it) + \frac{18}{\pi^2} G(it) > 0
F(it) - \frac{18}{\pi^2} G(it) > 0
respectively.
Uses Lemma 9.4, Definition 8.18, and Corollary 7.25.
By eqn:psiS-define from Definition 8.18,
\psi_I(it) = (\psi_S|_{-2}S)(it) = (it)^{2}\psi_S\left(-\frac{1}{it}\right) = -t^2 \psi_S\left(\frac{i}{t}\right).
Combined with Lemma Lemma 9.4 we can rewrite
eqn:ineqA as
A(t) = -t^2 \phi_0\left(\frac{i}{t}\right) + \frac{36}{\pi^2} \psi_S\left(\frac{i}{t}\right) < 0 \Leftrightarrow \frac{F(it)}{\Delta(it)} + \frac{18}{\pi^2} \frac{G(it)}{\Delta(it)} > 0
for t > 0, which is equivalent to eqn:ineqAnew by Corollary
Corollary 7.25.
Equivalences of eqn:ineqB and eqn:ineqBnew follows similarly; just change
the sign.
Now, the first inequality eqn:ineqAnew follows from the positivity of each
F(it) and G(it).
-
F_imag_axis_pos[complete] -
G_imag_axis_pos[complete]
For all t > 0, we have F(it) > 0 and G(it) > 0.
Uses Theorem 7.48 and Corollary 7.42.
Lean code for Lemma9.6●2 theorems
Associated Lean declarations
-
F_imag_axis_pos[complete]
-
G_imag_axis_pos[complete]
-
F_imag_axis_pos[complete] -
G_imag_axis_pos[complete]
-
theorem F_imag_axis_pos : ResToImagAxis.Pos
ResToImagAxis.Pos (F : UpperHalfPlane → ℂ) : PropFunction $F : \mathbb{H} \to \mathbb{C}$ is real and positive on the imaginary axis.FF : UpperHalfPlane → ℂDefinition of $F$ and $G$ and auxiliary functions for the inequality between them on the imaginary axis.theorem F_imag_axis_pos : ResToImagAxis.Pos
ResToImagAxis.Pos (F : UpperHalfPlane → ℂ) : PropFunction $F : \mathbb{H} \to \mathbb{C}$ is real and positive on the imaginary axis.FF : UpperHalfPlane → ℂDefinition of $F$ and $G$ and auxiliary functions for the inequality between them on the imaginary axis.`F(it) > 0` for all `t > 0`. Blueprint: F = 9*(D E₄)² and D E₄ > 0 on imaginary axis.
-
theorem G_imag_axis_pos : ResToImagAxis.Pos
ResToImagAxis.Pos (F : UpperHalfPlane → ℂ) : PropFunction $F : \mathbb{H} \to \mathbb{C}$ is real and positive on the imaginary axis.GG (τ : UpperHalfPlane) : ℂtheorem G_imag_axis_pos : ResToImagAxis.Pos
ResToImagAxis.Pos (F : UpperHalfPlane → ℂ) : PropFunction $F : \mathbb{H} \to \mathbb{C}$ is real and positive on the imaginary axis.GG (τ : UpperHalfPlane) : ℂ`G(it) > 0` for all `t > 0`. Blueprint: Lemma 8.6 - follows from H₂(it) > 0 and H₄(it) > 0. G = H₂³ (2H₂² + 5H₂H₄ + 5H₄²) is positive since all factors are positive.
By Ramanujan's identity Theorem 7.48, we have
F(z) = 9 E_4'(z)^2, and hence
F(it) = 9E_4'(it)^2 = 9 \left(240\sum_{n \geq 1} n \sigma_3(n) e^{-2 \pi n t} \right)^{2} > 0.
The inequality G(it) > 0 follows from positivity of H_2(it) and
H_4(it) in Corollary 7.42.
Equation eqn:ineqAnew holds.
Uses Lemma 9.6.
Lean code for Corollary9.7●1 theorem, incomplete
Associated Lean declarations
-
FG_inequality_1[sorry in proof]
-
FG_inequality_1[sorry in proof]
-
theorem FG_inequality_1 {t
ℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.} (ht0 < t: 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`.tℝ) : FRealFReal (t : ℝ) : ℝtℝ+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`.18 *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.^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`.(-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`.GRealGReal (t : ℝ) : ℝtℝ>GT.gt.{u} {α : Type u} [LT α] (a b : α) : Prop`a > b` is an abbreviation for `b < a`. Conventions for notations in identifiers: * The recommended spelling of `>` in identifiers is `gt`.0theorem FG_inequality_1 {t
ℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.} (ht0 < t: 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`.tℝ) : FRealFReal (t : ℝ) : ℝtℝ+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`.18 *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.^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`.(-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`.GRealGReal (t : ℝ) : ℝtℝ>GT.gt.{u} {α : Type u} [LT α] (a b : α) : Prop`a > b` is an abbreviation for `b < a`. Conventions for notations in identifiers: * The recommended spelling of `>` in identifiers is `gt`.0Main inequalities between $F$ and $G$ on the imaginary axis.
This directly follows from Lemma Lemma 9.6.
To prove the second inequality, we need some identities satisfied by F and
G.
F and G satisfy the following differential equations:
\partial_{12}\partial_{10} F - \frac{5}{6} E_{4} F = 7200 \Delta (-E_{2}')
\partial_{12}\partial_{10} G - \frac{5}{6} E_{4} G = -640 \Delta H_{2}.
Uses Theorem 7.48, Theorem 7.51, Lemma 7.50, and Lemma 7.41.
Lean code for Lemma9.8●2 theorems
-
theorem MLDE_F : serre_D
serre_D (k : ℂ) : (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂSerre derivative of weight $k$. Note that the definition makes sense for any analytic function $F : \mathbb{H} \to \mathbb{C}$.12 (serre_Dserre_D (k : ℂ) : (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂSerre derivative of weight $k$. Note that the definition makes sense for any analytic function $F : \mathbb{H} \to \mathbb{C}$.10 FF : UpperHalfPlane → ℂDefinition of $F$ and $G$ and auxiliary functions for the inequality between them on the imaginary axis.) =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`.5 *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`.6⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `⁻¹` in identifiers is `inv`.*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`.E₄E₄ : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 4.toFunSlashInvariantForm.toFun {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} (self : SlashInvariantForm Γ k) : UpperHalfPlane → ℂThe underlying function `ℍ → ℂ`. Do NOT use directly. Use the coercion instead.*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`.FF : UpperHalfPlane → ℂDefinition of $F$ and $G$ and auxiliary functions for the inequality between them on the imaginary axis.+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`.7200 *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`.Δ_funΔ_fun : UpperHalfPlane → ℂ*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`.negDE₂negDE₂ : UpperHalfPlane → ℂtheorem MLDE_F : serre_D
serre_D (k : ℂ) : (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂSerre derivative of weight $k$. Note that the definition makes sense for any analytic function $F : \mathbb{H} \to \mathbb{C}$.12 (serre_Dserre_D (k : ℂ) : (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂSerre derivative of weight $k$. Note that the definition makes sense for any analytic function $F : \mathbb{H} \to \mathbb{C}$.10 FF : UpperHalfPlane → ℂDefinition of $F$ and $G$ and auxiliary functions for the inequality between them on the imaginary axis.) =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`.5 *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`.6⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `⁻¹` in identifiers is `inv`.*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`.E₄E₄ : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 4.toFunSlashInvariantForm.toFun {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} (self : SlashInvariantForm Γ k) : UpperHalfPlane → ℂThe underlying function `ℍ → ℂ`. Do NOT use directly. Use the coercion instead.*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`.FF : UpperHalfPlane → ℂDefinition of $F$ and $G$ and auxiliary functions for the inequality between them on the imaginary axis.+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`.7200 *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`.Δ_funΔ_fun : UpperHalfPlane → ℂ*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`.negDE₂negDE₂ : UpperHalfPlane → ℂModular linear differential equation satisfied by $F$.
-
theorem MLDE_G : serre_D
serre_D (k : ℂ) : (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂSerre derivative of weight $k$. Note that the definition makes sense for any analytic function $F : \mathbb{H} \to \mathbb{C}$.12 (serre_Dserre_D (k : ℂ) : (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂSerre derivative of weight $k$. Note that the definition makes sense for any analytic function $F : \mathbb{H} \to \mathbb{C}$.10 GG (τ : UpperHalfPlane) : ℂ) =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`.5 *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`.6⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `⁻¹` in identifiers is `inv`.*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`.E₄E₄ : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 4.toFunSlashInvariantForm.toFun {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} (self : SlashInvariantForm Γ k) : UpperHalfPlane → ℂThe underlying function `ℍ → ℂ`. Do NOT use directly. Use the coercion instead.*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`.GG (τ : UpperHalfPlane) : ℂ-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).640 *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`.Δ_funΔ_fun : UpperHalfPlane → ℂ*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`.H₂H₂ (τ : UpperHalfPlane) : ℂtheorem MLDE_G : serre_D
serre_D (k : ℂ) : (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂSerre derivative of weight $k$. Note that the definition makes sense for any analytic function $F : \mathbb{H} \to \mathbb{C}$.12 (serre_Dserre_D (k : ℂ) : (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂSerre derivative of weight $k$. Note that the definition makes sense for any analytic function $F : \mathbb{H} \to \mathbb{C}$.10 GG (τ : UpperHalfPlane) : ℂ) =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`.5 *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`.6⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `⁻¹` in identifiers is `inv`.*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`.E₄E₄ : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 4.toFunSlashInvariantForm.toFun {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} (self : SlashInvariantForm Γ k) : UpperHalfPlane → ℂThe underlying function `ℍ → ℂ`. Do NOT use directly. Use the coercion instead.*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`.GG (τ : UpperHalfPlane) : ℂ-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).640 *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`.Δ_funΔ_fun : UpperHalfPlane → ℂ*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`.H₂H₂ (τ : UpperHalfPlane) : ℂModular linear differential equation satisfied by $G$.
Both identities can be shown by direct computations.
By Ramanujan's identities (Theorem Theorem 7.48) and the
product rule for Serre derivatives (Theorem
Theorem 7.51), we have
\partial_{5} (E_2 E_4 - E_6)
= (E_2 E_4 - E_6)' - \frac{5}{12} E_2 (E_2 E_4 - E_6)
= \frac{E_2^2 - E_4}{12} \cdot E_4 + E_2 \cdot \frac{E_2 E_4 - E_6}{3} - \frac{E_2 E_6 - E_4^2}{2} - \frac{5}{12}E_2 (E_2 E_4 - E_6)
= -\frac{5}{12} (E_2 E_6 - E_4^2)
and
\partial_{7} (E_2 E_6 - E_4^2)
= (E_2 E_6 - E_4^2)' - \frac{7}{12} E_2 (E_2 E_6 - E_4^2)
= \frac{E_2^2 - E_4}{12} \cdot E_6 + E_2 \cdot \frac{E_2 E_6 - E_4^2}{2} - 2 E_4 \cdot \frac{E_2 E_4 - E_6}{3} - \frac{7}{12} E_2 (E_2 E_6 - E_4^2)
= -\frac{7}{12} E_4 (E_2 E_4 - E_6).
Using these, we compute
\partial_{10} F = \partial_{10} (E_2 E_4 - E_6)^2
= 2 (E_2 E_4 - E_6) \partial_{5} (E_2 E_4 - E_6)
= -\frac{6}{5} (E_2 E_4 - E_6) (E_2 E_6 - E_4^2),
and then
\partial_{12}\partial_{10} F
= -\frac{5}{6} \partial_{12} ((E_2 E_4 - E_6) (E_2 E_6 - E_4))
= -\frac{5}{6} (\partial_{5}(E_2 E_4 - E_6)) (E_2 E_6 - E_4^2) - \frac{5}{6} (E_2 E_4 - E_6) (\partial_{7} (E_2 E_6 - E_4))
= \frac{25}{72} (E_2 E_6 - E_4^2)^2 + \frac{35}{72} E_4 (E_2 E_4 - E_6)^2.
Hence
\partial_{12}\partial_{10}F - \frac{5}{6} E_4 F
= \frac{25}{72} ((E_2 E_6 - E_4^2)^2 - E_4 (E_2 E_4 - E_6)^2)
= \frac{25}{72} (- E_2^2 E_4^3 + E_2^2 E_6^2 + E_4^4 - E_4 E_6^3)
= -\frac{25}{72} (E_4^3 - E_6^2) (E_2^2 - E_4)
= 7200 \Delta (-E_2').
This proves equation eqn:ddf. The second is proved similarly,
using Proposition Lemma 7.50 and
Lemma Lemma 7.41.
- No associated Lean code or declarations.
Equation eqn:ddf is positive and equation eqn:ddg is negative on the
positive imaginary axis.
Uses Lemma 9.8, Corollary 7.25, Corollary 7.42, and Definition 7.17.
From equation eqn:E2 in Definition 7.17 and
Lemma Corollary 7.25,
7200 (-E_2'(it)) \Delta(it) = 7200 \cdot 24 \left(\sum_{n \ge 1} n \sigma_1(n) e^{-2 \pi n t}\right) \cdot \Delta(it) > 0.
Negativity of equation eqn:ddg, namely
-640 \Delta(it) H_2(it) < 0, follows from
Corollary 7.42 and Corollary 7.25.
The second inequality follows from the following two observations.
Since G(it) > 0 for all t > 0, we can define the quotient
Q(t) := \frac{F(it)}{G(it)}
as a function on (0, \infty).
-
FmodG_rightLimitAt_zero[sorry in proof]
We have
\lim_{t \to 0^+} Q(t) = \frac{18}{\pi^2}.
Uses Lemma 7.18, Lemma 7.14, and Lemma 7.33.
Lean code for Lemma9.10●1 theorem, incomplete
Associated Lean declarations
-
FmodG_rightLimitAt_zero[sorry in proof]
-
FmodG_rightLimitAt_zero[sorry in proof]
-
theorem FmodG_rightLimitAt_zero : Filter.Tendsto
Filter.Tendsto.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Prop`Filter.Tendsto` is the generic "limit of a function" predicate. `Tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`, the `f`-preimage of `a` is an `l₁` neighborhood.FmodGRealFmodGReal (t : ℝ) : ℝ(nhdsWithinnhdsWithin.{u_1} {X : Type u_1} [TopologicalSpace X] (x : X) (s : Set X) : Filter XThe "neighborhood within" filter. Elements of `𝓝[s] x` are sets containing the intersection of `s` and a neighborhood of `x`.0 (Set.IoiSet.Ioi.{u_1} {α : Type u_1} [Preorder α] (b : α) : Set α`Ioi a` is the left-open right-infinite interval $(a, ∞)$.0)) (nhdsWithinnhdsWithin.{u_1} {X : Type u_1} [TopologicalSpace X] (x : X) (s : Set X) : Filter XThe "neighborhood within" filter. Elements of `𝓝[s] x` are sets containing the intersection of `s` and a neighborhood of `x`.(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`.18 *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.^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`.(-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`.Set.univSet.univ.{u} {α : Type u} : Set αThe universal set on a type `α` is the set containing all elements of `α`. This is conceptually the "same as" `α` (in set theory, it is actually the same), but type theory makes the distinction that `α` is a type while `Set.univ` is a term of type `Set α`. `Set.univ` can itself be coerced to a type `↥Set.univ` which is in bijection with (but distinct from) `α`.)theorem FmodG_rightLimitAt_zero : Filter.Tendsto
Filter.Tendsto.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Prop`Filter.Tendsto` is the generic "limit of a function" predicate. `Tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`, the `f`-preimage of `a` is an `l₁` neighborhood.FmodGRealFmodGReal (t : ℝ) : ℝ(nhdsWithinnhdsWithin.{u_1} {X : Type u_1} [TopologicalSpace X] (x : X) (s : Set X) : Filter XThe "neighborhood within" filter. Elements of `𝓝[s] x` are sets containing the intersection of `s` and a neighborhood of `x`.0 (Set.IoiSet.Ioi.{u_1} {α : Type u_1} [Preorder α] (b : α) : Set α`Ioi a` is the left-open right-infinite interval $(a, ∞)$.0)) (nhdsWithinnhdsWithin.{u_1} {X : Type u_1} [TopologicalSpace X] (x : X) (s : Set X) : Filter XThe "neighborhood within" filter. Elements of `𝓝[s] x` are sets containing the intersection of `s` and a neighborhood of `x`.(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`.18 *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.^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`.(-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`.Set.univSet.univ.{u} {α : Type u} : Set αThe universal set on a type `α` is the set containing all elements of `α`. This is conceptually the "same as" `α` (in set theory, it is actually the same), but type theory makes the distinction that `α` is a type while `Set.univ` is a term of type `Set α`. `Set.univ` can itself be coerced to a type `↥Set.univ` which is in bijection with (but distinct from) `α`.)$\lim_{t \to 0^+} F(it) / G(it) = 18 / \pi^2$.
We have
\lim_{t \to 0^+} Q(t) = \lim_{t \to 0^+} \frac{F(it)}{G(it)} = \lim_{t \to \infty} \frac{F(i/t)}{G(i/t)}.
By using the transformation laws of Eisenstein series eqn:E2-S-transform,
eqn:Ek-trans-S (for k = 4, 6) and the thetanull functions,
eqn:H2-transform-S, eqn:H4-transform-S, we get
F\left(\frac{i}{t}\right) = t^{12} F(it) - \frac{12t^{11}}{\pi} (E_2(it)E_4(it) - E_6(it))E_4(it) + \frac{36t^{10}}{\pi^2}E_4(it)^2
and
G\left(\frac{i}{t}\right) = t^{10} H_{4}(it)^{3}(2H_{4}(it)^{2} + 5 H_{4}(it)H_{2}(it) + 5 H_{2}(it)^{2}).
Since F, E_2 E_4 - E_6 and H_2 are cusp forms, we have
\lim_{t \to \infty}t^k A(it) = 0 when A(z) is one of these forms and
k \geq 0.
From \lim_{t \to \infty} E_4(it) = 1 = \lim_{t \to \infty}H_{4}(it), we get
\begin{aligned}
\lim_{t \to \infty} \frac{F(i/t)}{G(i/t)}
&= \lim_{t \to \infty} \frac{t^{12} F(it) - \frac{12t^{11}}{\pi} (E_2(it)E_4(it) - E_6(it))E_4(it) + \frac{36t^{10}}{\pi^2}E_4(it)^2}{t^{10} H_{4}(it)^{3}(2H_{4}(it)^{2} + 5 H_{4}(it)H_{2}(it) + 5 H_{2}(it)^{2})} \\
&= \lim_{t \to \infty} \frac{t^{2} F(it) - \frac{12t}{\pi} (E_2(it)E_4(it) - E_6(it))E_4(it) + \frac{36}{\pi^2}E_4(it)^2}{H_{4}(it)^{3}(2H_{4}(it)^{2} + 5 H_{4}(it)H_{2}(it) + 5 H_{2}(it)^{2})} \\
&= \frac{18}{\pi^2}.
\end{aligned}
- No associated Lean code or declarations.
Let F be a quasimodular form whose vanishing order at infinity is
n_0 > 0, that is,
F(z) = \sum_{n \geq n_0} a_n q^{n} with a_{n_0} \ne 0. Then
\lim_{t \to \infty} \frac{F'(it)}{F(it)} = n_0.
Uses Lemma 7.44.
By Lemma Lemma 7.44,
\lim_{t \to \infty} \frac{F'(it)}{F(it)}
= \lim_{t \to \infty} \frac{\sum_{n \ge n_0} n a_n e^{-2 \pi n t}}{\sum_{n \ge n_0} a_n e^{-2 \pi n t}}
= \lim_{t \to \infty} \frac{n_0 a_{n_0} e^{-2 \pi n_0 t} + O(e^{-2 \pi (n_0 + 1) t})}{a_{n_0} e^{-2 \pi n_0 t} + O(e^{-2 \pi (n_0 + 1) t})}
= n_0.
-
FmodG_strictAntiOn[complete]
The function t \mapsto Q(t) is strictly decreasing.
Uses Theorem 7.48, Theorem 7.51, Corollary 9.9, Theorem 7.52, and Lemma 9.11.
Lean code for Lemma9.12●1 theorem
Associated Lean declarations
-
FmodG_strictAntiOn[complete]
-
FmodG_strictAntiOn[complete]
-
theorem FmodG_strictAntiOn : StrictAntiOn
StrictAntiOn.{u, v} {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) (s : Set α) : PropA function `f` is strictly antitone on `s` if, for all `a, b ∈ s`, `a < b` implies `f b < f a`.FmodGRealFmodGReal (t : ℝ) : ℝ(Set.IoiSet.Ioi.{u_1} {α : Type u_1} [Preorder α] (b : α) : Set α`Ioi a` is the left-open right-infinite interval $(a, ∞)$.0)theorem FmodG_strictAntiOn : StrictAntiOn
StrictAntiOn.{u, v} {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) (s : Set α) : PropA function `f` is strictly antitone on `s` if, for all `a, b ∈ s`, `a < b` implies `f b < f a`.FmodGRealFmodGReal (t : ℝ) : ℝ(Set.IoiSet.Ioi.{u_1} {α : Type u_1} [Preorder α] (b : α) : Set α`Ioi a` is the left-open right-infinite interval $(a, ∞)$.0)**Proposition 8.12**: `FmodGReal` is strictly decreasing on `(0, ∞)`.
It is enough to show that
\frac{\dd}{\dd t} \left(\frac{F(it)}{G(it)}\right) < 0
\Leftrightarrow (- 2\pi) \frac{F'(it)G(it) - F(it) G'(it)}{G(it)^{2}} < 0
\Leftrightarrow F'(it) G(it) - F(it) G'(it) > 0
\Leftrightarrow (\partial_{10}F)(it) G(it) - F(it) (\partial_{10}G)(it) > 0.
Let \mathcal{L}_{1, 0} := (\partial_{10}F) G - F (\partial_{10} G) = F'G - FG'.
Then
\frac{\mathcal{L}_{1, 0}}{FG} = \frac{F'G - FG'}{FG} = \frac{F'}{F} - \frac{G'}{G}.
The vanishing orders of F and G at infinity are 2 and
\frac{3}{2} respectively, so by
Lemma 9.11 we have
\lim_{t \to \infty} \frac{\mathcal{L}_{1, 0}(it)}{F(it) G(it)}
= \lim_{t \to \infty} \left(\frac{F'(it)}{F(it)} - \frac{G'(it)}{G(it)}\right)
= 2 - \frac{3}{2} = \frac{1}{2} > 0,
so \mathcal{L}_{1, 0}(it) > 0 for sufficiently large t.
Its Serre derivative is positive by Corollary 9.9:
\partial_{22} \mathcal{L}_{1, 0} = (\partial_{12} \partial_{10} F) G - F (\partial_{12}\partial_{10} G)
= \Delta (7200 (-E_{2}') G + 640 H_2 F) > 0.
Hence \mathcal{L}_{1, 0}(it) > 0 by
Theorem 7.52, and the
monotonicity follows.
-
FG_inequality_2[sorry in proof]
Equation eqn:ineqBnew holds.
Uses Lemma 9.10, Lemma 9.12, and Lemma 9.6.
Lean code for Corollary9.13●1 theorem, incomplete
Associated Lean declarations
-
FG_inequality_2[sorry in proof]
-
FG_inequality_2[sorry in proof]
-
theorem FG_inequality_2 {t
ℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.} (ht0 < t: 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`.tℝ) : FRealFReal (t : ℝ) : ℝtℝ-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).18 *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.^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`.(-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`.GRealGReal (t : ℝ) : ℝtℝ<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`.0theorem FG_inequality_2 {t
ℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.} (ht0 < t: 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`.tℝ) : FRealFReal (t : ℝ) : ℝtℝ-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).18 *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.^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`.(-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`.GRealGReal (t : ℝ) : ℝtℝ<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
We have
\frac{F(it)}{G(it)} = Q(t) < \lim_{u \to 0^+} Q(u) = \frac{18}{\pi^2},
and by Lemma Lemma 9.6 the desired inequality follows.
- No associated Lean code or declarations.
The function
g(x):=\frac{\pi\,i}{8640}a(x)+\frac{i}{240\pi}\,b(x)
satisfies conditions eqn:g1--eqn:g3.
Uses Lemma 8.12, Lemma 8.26, Lemma 8.14, Lemma 8.28, Lemma 9.1, Lemma 9.2, Lemma 8.16, and Lemma 8.30.
First, we prove the first sign condition. By Propositions
Lemma 8.14 and Lemma 8.28 we know
that for r>\sqrt{2},
g(r)=\frac{\pi}{2160}\,\sin(\pi r^2/2)^2\,\int\limits_0^\infty A(t)\,e^{-\pi r^2 t}\,dt
where
A(t)=-t^2\phi_0(i/t)-\frac{36}{\pi^2}\,\psi_I(it).
From Proposition Lemma 9.1 we know that A(t)<0 for
t\in(0,\infty), so this identity implies the first sign condition.
/- source paragraph break -/
Next, we prove the Fourier-side sign condition. By Propositions
Lemma 8.15 and
Lemma 8.29 we
know that for r>0,
\widehat{g}(r)=\frac{\pi}{2160}\,\sin(\pi r^2/2)^2\,\int\limits_0^\infty B(t)\,e^{-\pi r^2 t}\,dt
where
B(t)=-t^2\phi_0(i/t)+\frac{36}{\pi^2}\,\psi_I(it).
/- source paragraph break -/
Finally, the normalization g(0)=\widehat g(0)=1 follows readily from
Propositions Lemma 8.16 and Lemma 8.30.
This finishes the proof.