Project-declaredLean 4.31.0 · mathlib@fabf563a7c95

F₂ eq zero

f₂_eq_zero

sphere packing Fourier analysis modular forms derivative

Plain-language statement

From g = 0 and h = 0, deduce f₂ = 0. Proof: From g = 0 we get a relation between f₂ and f₄. Combined with h = 0, we show f₄² · (3 · H_sum_sq) = 0. Since H_sum_sq → 1 ≠ 0, we get f₄ = 0, then f₂ = 0 follows from h = f₂² = 0.

Exact Lean statement

lemma f₂_eq_zero : f₂ = 0

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma f₂_eq_zero : f₂ = 0 := by  have hg := theta_g_eq_zero  have hh := theta_h_eq_zero  -- Show f₄ = 0 first, then f₂ = 0 follows from theta_h = f₂² = 0  suffices hf₄ : f₄ = 0 by    funext z    have hz := congrFun hh z    unfold theta_h at hz    simp only [Pi.add_apply, Pi.pow_apply, Pi.mul_apply, Pi.zero_apply, hf₄] at hz    simpa [sq_eq_zero_iff] using hz  -- From f₄_sq_mul_eq and theta_h = 0: f₄² * (3 * H_sum_sq) = 0  have h_f₄_sq_3H : f₄ ^ 2 * (fun z => 3 * H_sum_sq z) = 0 := by    ext z    simp only [Pi.mul_apply, Pi.pow_apply, Pi.zero_apply]    have hh_z : theta_h z = 0 := congrFun hh z    calc f₄ z ^ 2 * (3 * H_sum_sq z)        = (2 * H₂ z + H₄ z) ^ 2 * theta_h z := f₄_sq_mul_eq z (congrFun hg z)      _ = _ := by rw [hh_z, mul_zero]  -- f₄² is MDifferentiable  have f₄_sq_MDiff : MDiff (f₄ ^ 2) := f₄_MDifferentiable.pow 2  -- By mul_eq_zero_iff: f₄² = 0 (since 3 * H_sum_sq ≠ 0)  have h_f₄_sq_zero : f₄ ^ 2 = 0 :=    ((UpperHalfPlane.mul_eq_zero_iff f₄_sq_MDiff three_H_sum_sq_MDifferentiable).mp h_f₄_sq_3H      ).resolve_right three_H_sum_sq_ne_zero  -- From f₄² = f₄ * f₄ = 0: f₄ = 0  exact (UpperHalfPlane.mul_eq_zero_iff f₄_MDifferentiable f₄_MDifferentiable).mp    (pow_two f₄ ▸ h_f₄_sq_zero) |>.elim id id

Project: Sphere Packing in Dimension 8
License: Apache-2.0
Commit: acfc6204e65a
Source: SpherePacking/ModularForms/JacobiTheta/Derivative.lean:671-697

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.31.0

Anti Der Pos

antiDerPos

Plain-language statement

If $F$ is a modular form where $F(it)$ is positive for sufficiently large $t$ (i.e. constant term is positive) and the derivative is positive, then $F$ is also positive.

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Anti Serre Der Pos

antiSerreDerPos

Plain-language statement

Let $F : \mathbb{H} \to \mathbb{C}$ be a holomorphic function where $F(it)$ is real for all $t > 0$ . Assume that Serre derivative $\partial_k F$ is positive on the imaginary axis. If $F(it)$ is positive for sufficiently large $t$ , then $F(it)$ is positive for all $t > 0$ .

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Closed Ball center subset upper Half Plane

closedBall_center_subset_upperHalfPlane

Plain-language statement

Closed ball centered at z with radius z.im/2 is contained in the upper half plane.

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record