Sphere Packing in R^8

7. Modular Forms🔗

This chapter follows the modular-form pipeline from the original blueprint and uses references such as Diamond and Shurman (2005).

Definition7.1
Group: Congruence groups, slash operators, and modular forms. (2)
Hover another entry in this group to preview it.
Preview
Lemma 7.2
Blueprint label
  • «lemma:slash-negI-even-weight»
Group
  • Congruence groups, slash operators, and modular forms.
XL∃∀Nused by 0

Define the weight-k slash action of \mathrm{SL}_2(\mathbb{Z}) on functions on the upper half-plane.

Proof

Direct formula using the automorphy factor.

Lemma7.2
Group: Congruence groups, slash operators, and modular forms. (2)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • «def:slash-operator»
Group
  • Congruence groups, slash operators, and modular forms.
AL∃∀Nused by 0

For even weight, slash by -I acts trivially.

Code for Lemma7.2●1 definition, incomplete
  • axiom 
    modular_slash_negI_of_even : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    modular_slash_negI_of_even : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Immediate from (-1)^{-k} = 1 for even k.

Definition7.3
Group: Congruence groups, slash operators, and modular forms. (2)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • «def:slash-operator»
Group
  • Congruence groups, slash operators, and modular forms.
AL∃∀Nused by 0

Define modular forms of weight k and level \Gamma.

Code for Definition7.3●1 definition, incomplete
  • axiom 
    ModularForm : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    ModularForm : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Standard slash-invariance, holomorphy, and cusp-growth conditions.

Definition7.4
Group: Eisenstein series, the discriminant form, and positivity/nonvanishing tools. (9)
Hover another entry in this group to preview it.
Preview
Lemma 7.5
Blueprint label
  • «lemma:Ek-is-modular-form»
Group
  • Eisenstein series, the discriminant form, and positivity/nonvanishing tools.
AL∃∀Nused by 0

Define Eisenstein series E_k for even k \ge 4.

Code for Definition7.4●1 definition, incomplete
  • axiom 
    ModularForm.eisensteinSeries_MF : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    ModularForm.eisensteinSeries_MF : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Classical series definition.

Lemma7.5
Group: Eisenstein series, the discriminant form, and positivity/nonvanishing tools. (9)
Hover another entry in this group to preview it.
Preview
Definition 7.4
Blueprint label
  • «def:Ek»
Group
  • Eisenstein series, the discriminant form, and positivity/nonvanishing tools.
AL∃∀Nused by 0

E_k is a modular form and satisfies the expected S-transformation law.

Code for Lemma7.5●1 definition, incomplete
  • axiom 
    EisensteinSeries.eisensteinSeries_SIF : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    EisensteinSeries.eisensteinSeries_SIF :
  PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

By absolute convergence and slash-invariance.

Lemma7.6
Group: Eisenstein series, the discriminant form, and positivity/nonvanishing tools. (9)
Hover another entry in this group to preview it.
Preview
Definition 7.4
Blueprint label
  • «def:Ek»
Group
  • Eisenstein series, the discriminant form, and positivity/nonvanishing tools.
AL∃∀Nused by 0

Fourier expansions of Eisenstein series.

Code for Lemma7.6●1 definition, incomplete
  • axiom 
    E_k_q_expansion : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    E_k_q_expansion : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Classical q-expansion theorem.

Definition7.7
Group: Eisenstein series, the discriminant form, and positivity/nonvanishing tools. (9)
Hover another entry in this group to preview it.
Preview
Definition 7.4
Blueprint label
  • «def:Ek»
Group
  • Eisenstein series, the discriminant form, and positivity/nonvanishing tools.
AL∃∀Nused by 0

Define E_2 by q-expansion.

Code for Definition7.7●1 definition, incomplete
  • axiom 
    E₂_eq : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    E₂_eq : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Direct definition.

Lemma7.8
Group: Eisenstein series, the discriminant form, and positivity/nonvanishing tools. (9)
Hover another entry in this group to preview it.
Preview
Definition 7.4
Blueprint label
  • «def:Ek»
Group
  • Eisenstein series, the discriminant form, and positivity/nonvanishing tools.
AL∃∀Nused by 0

E_2 is quasimodular and satisfies the S-transformation defect term.

Code for Lemma7.8●1 definition, incomplete
  • axiom 
    E₂_transform : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    E₂_transform : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Classical exercise in modular forms.

Definition7.9
Group: Eisenstein series, the discriminant form, and positivity/nonvanishing tools. (9)
Hover another entry in this group to preview it.
Preview
Definition 7.4
Blueprint label
  • «def:Ek»
Group
  • Eisenstein series, the discriminant form, and positivity/nonvanishing tools.
AL∃∀Nused by 0

Define the Dedekind eta function.

Code for Definition7.9●1 definition, incomplete
  • axiom 
    η : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    η : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Direct infinite product definition.

Definition7.10
Group: Eisenstein series, the discriminant form, and positivity/nonvanishing tools. (9)
Hover another entry in this group to preview it.
Preview
Definition 7.4
Blueprint label
  • «def:Ek»
Group
  • Eisenstein series, the discriminant form, and positivity/nonvanishing tools.
AL∃∀Nused by 0

Define the discriminant modular form \Delta.

Code for Definition7.10●1 definition, incomplete
  • axiom 
    Δ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Δ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Direct q-product definition.

Lemma7.11
Group: Eisenstein series, the discriminant form, and positivity/nonvanishing tools. (9)
Hover another entry in this group to preview it.
Preview
Definition 7.4
Blueprint label
  • «def:Ek»
Group
  • Eisenstein series, the discriminant form, and positivity/nonvanishing tools.
AL∃∀Nused by 0

\Delta is a weight-12 cusp form.

Code for Lemma7.11●1 definition, incomplete
  • axiom 
    Delta : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Delta : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Use the eta-transformation law.

Corollary7.12
Group: Eisenstein series, the discriminant form, and positivity/nonvanishing tools. (9)
Hover another entry in this group to preview it.
Preview
Definition 7.4
Blueprint label
  • «def:Ek»
Group
  • Eisenstein series, the discriminant form, and positivity/nonvanishing tools.
AL∃∀Nused by 1

\Delta(it) > 0 on the positive imaginary axis.

Code for Corollary7.12●1 definition, incomplete
  • axiom 
    Delta_imag_axis_pos : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Delta_imag_axis_pos : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

By product positivity.

Corollary7.13
Group: Eisenstein series, the discriminant form, and positivity/nonvanishing tools. (9)
Hover another entry in this group to preview it.
Preview
Definition 7.4
Blueprint label
  • «def:Ek»
Group
  • Eisenstein series, the discriminant form, and positivity/nonvanishing tools.
AL∃∀Nused by 0

\Delta(z) \ne 0 on the upper half-plane.

Code for Corollary7.13●1 definition, incomplete
  • axiom 
    Δ_ne_zero : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Δ_ne_zero : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Follows from cusp-form product structure.

Definition7.14
Group: Theta constants and identities used in the magic-function construction. (6)
Hover another entry in this group to preview it.
Preview
Definition 7.15
Blueprint label
  • «def:H2-H3-H4»
Group
  • Theta constants and identities used in the magic-function construction.
AL∃∀Nused by 0

Define Jacobi theta constants \Theta_2,\Theta_3,\Theta_4.

Code for Definition7.14●3 definitions, 3 incomplete
  • axiom 
    Θ₂ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Θ₂ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    Θ₃ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Θ₃ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    Θ₄ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Θ₄ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Direct theta-series definitions.

Definition7.15
Group: Theta constants and identities used in the magic-function construction. (6)
Hover another entry in this group to preview it.
Preview
Definition 7.14
Blueprint label
  • «def:th00-th01-th10»
Group
  • Theta constants and identities used in the magic-function construction.
AL∃∀Nused by 0

Define H_2 = \Theta_2^4, H_3 = \Theta_3^4, H_4 = \Theta_4^4.

Code for Definition7.15●3 definitions, 3 incomplete
  • axiom 
    H₂ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₂ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    H₃ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₃ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    H₄ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₄ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Direct algebraic definition.

Lemma7.16
Group: Theta constants and identities used in the magic-function construction. (6)
Hover another entry in this group to preview it.
Preview
Definition 7.14
Blueprint label
  • «def:th00-th01-th10»
Group
  • Theta constants and identities used in the magic-function construction.
AL∃∀Nused by 0

Transformation laws of the theta quartics under S and T.

Code for Lemma7.16●6 definitions, 6 incomplete
  • axiom 
    H₂_T_action : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₂_T_action : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    H₃_T_action : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₃_T_action : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    H₄_T_action : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₄_T_action : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    H₂_S_action : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₂_S_action : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    H₃_S_action : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₃_S_action : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    H₄_S_action : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₄_S_action : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Derived from Jacobi theta transformations.

Lemma7.17
Group: Theta constants and identities used in the magic-function construction. (6)
Hover another entry in this group to preview it.
Preview
Definition 7.14
Blueprint label
  • «def:th00-th01-th10»
Group
  • Theta constants and identities used in the magic-function construction.
AL∃∀Nused by 0

H_2,H_3,H_4 are modular forms of level 2.

Code for Lemma7.17●3 definitions, 3 incomplete
  • axiom 
    H₂_MF : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₂_MF : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    H₃_MF : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₃_MF : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    H₄_MF : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₄_MF : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

From slash invariance and boundedness at cusps.

Lemma7.18
Group: Theta constants and identities used in the magic-function construction. (6)
Hover another entry in this group to preview it.
Preview
Definition 7.14
Blueprint label
  • «def:th00-th01-th10»
Group
  • Theta constants and identities used in the magic-function construction.
AL∃∀Nused by 0

Jacobi identity relating the theta quartics.

Code for Lemma7.18●1 definition, incomplete
  • axiom 
    jacobi_identity : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    jacobi_identity : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Dimension and q-expansion comparison.

Lemma7.19
Group: Theta constants and identities used in the magic-function construction. (6)
Hover another entry in this group to preview it.
Preview
Definition 7.14
Blueprint label
  • «def:th00-th01-th10»
Group
  • Theta constants and identities used in the magic-function construction.
XL∃∀Nused by 0

Identities expressing E_4,E_6,\Delta in terms of H_2,H_3,H_4.

Proof

Use uniqueness of low-weight level-1 forms and q-expansions.

Corollary7.20
Group: Theta constants and identities used in the magic-function construction. (6)
Hover another entry in this group to preview it.
Preview
Definition 7.14
Blueprint label
  • «def:th00-th01-th10»
Group
  • Theta constants and identities used in the magic-function construction.
AL∃∀Nused by 1

Positivity statements for theta quartics on the positive imaginary axis.

Code for Corollary7.20●2 definitions, 2 incomplete
  • axiom 
    H₂_imag_axis_pos : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₂_imag_axis_pos : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    H₄_imag_axis_pos : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    H₄_imag_axis_pos : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

From theta-series positivity and transformations.

Definition7.21
Group: Serre derivative identities and differential inequalities. (5)
Hover another entry in this group to preview it.
Preview
Definition 7.22
Blueprint label
  • «def:serre-der»
Group
  • Serre derivative identities and differential inequalities.
AL∃∀Nused by 0

Define the normalized complex derivative operator on modular forms.

Code for Definition7.21●1 definition, incomplete
  • axiom 
    D : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    D : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Temporary placeholders for external `lean := "..."` references from the SpherePacking blueprint port.

XXX Blueprint toolchain workaround: these declarations exist only to keep blueprint links
non-missing while the upstream SpherePacking project is not imported in this workspace toolchain.
    axiom-like (no body)
Proof

Direct operator definition.

Definition7.22
Group: Serre derivative identities and differential inequalities. (5)
Hover another entry in this group to preview it.
Preview
Definition 7.21
Blueprint label
  • «def:derivative»
Group
  • Serre derivative identities and differential inequalities.
AL∃∀Nused by 0

Define the Serre derivative.

Code for Definition7.22●1 definition, incomplete
  • axiom 
    serre_D : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    serre_D : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Direct definition in terms of D and E_2.

Theorem7.23
Group: Serre derivative identities and differential inequalities. (5)
Hover another entry in this group to preview it.
Preview
Definition 7.21
Blueprint label
  • «def:derivative»
Group
  • Serre derivative identities and differential inequalities.
AL∃∀Nused by 1

Serre derivative raises weight by 2 while preserving modularity.

Code for Theorem7.23●1 definition, incomplete
  • axiom 
    serre_D_slash_invariant : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    serre_D_slash_invariant : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

By slash-equivariance and cancellation of quasimodular defects.

Theorem7.24
Group: Serre derivative identities and differential inequalities. (5)
Hover another entry in this group to preview it.
Preview
Definition 7.21
Blueprint label
  • «def:derivative»
Group
  • Serre derivative identities and differential inequalities.
AL∃∀Nused by 1

Ramanujan differential equations for E_2,E_4,E_6.

Code for Theorem7.24●6 definitions, 6 incomplete
  • axiom 
    ramanujan_E₂ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    ramanujan_E₂ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    ramanujan_E₄ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    ramanujan_E₄ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    ramanujan_E₆ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    ramanujan_E₆ : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    ramanujan_E₂' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    ramanujan_E₂' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    ramanujan_E₄' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    ramanujan_E₄' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    ramanujan_E₆' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    ramanujan_E₆' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Apply Theorem 7.23 and low-weight dimension constraints.

Theorem7.25
Group: Serre derivative identities and differential inequalities. (5)
Hover another entry in this group to preview it.
Preview
Definition 7.21
Blueprint label
  • «def:derivative»
Group
  • Serre derivative identities and differential inequalities.
AL∃∀Nused by 1

Product rule for Serre derivatives.

Code for Theorem7.25●1 definition, incomplete
  • axiom 
    serre_D_mul : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    serre_D_mul : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Direct computation from the definition.

Theorem7.26
Group: Serre derivative identities and differential inequalities. (5)
Hover another entry in this group to preview it.
Preview
Definition 7.21
Blueprint label
  • «def:derivative»
Group
  • Serre derivative identities and differential inequalities.
XL∃∀Nused by 1

Monotonicity criterion on the positive imaginary axis for anti-Serre-type differential operators.

Proof

Combine Ramanujan identities with sign information from Corollary 7.12 and Corollary 7.20.