funlean.
Step 47 / 64

University

Cusp forms

A modular form with an additional zero-limit condition at every cusp.

Start with a concrete example

Compare a quantity that gets halved at every step with one that stays at 1. After more steps, only the first gets close to 0.

1 / 2^2 = 0.25The lower amount stays at 1

After 2 halvings: 0.25. It approaches 0 without becoming 0 in a finite number of steps.

How this example differs from the definition

The halving sequence is not a cusp form. Actual cusps are specific boundary points, and the required behavior must hold at every one.

A small check: try the idea

Compare the numbers in the question with the diagram you are moving. You can try again.

After eight halvings, has the positive quantity become exactly 0?

Read the answer and reasoning

No; it is 1/256, close to 0 but not 0. Move to step 8 and read 1/256 = 0.00390625. Approaching 0 and being exactly 0 are different. The sequence is a model, not a cusp form.

Build the idea in three steps

  1. A modular form has controlled behavior at cusps: boundary directions of the upper half-plane modulo its symmetries.
  2. A cusp form adds the stronger condition that the appropriate limit is zero at every cusp. Zero at a cusp does not mean zero everywhere.
  3. Later in FLT, a theorem proves that every cusp form in one particular weight-and-level space is identically zero. That is an additional theorem.

A small example

A zero function is a cusp form. The argument later needs a nonzero one in precisely the space that the vanishing theorem rules out.

Lean definition · original excerpt

Mathlib · db584cd · Basic.lean

structure CuspForm extends SlashInvariantForm Γ k where  holo' : MDiff (toSlashInvariantForm : ℍ → ℂ)  zero_at_cusps' {c : OnePoint ℝ} (hc : IsCusp c Γ) : c.IsZeroAt toFun k

How to read this Lean

zero_at_cusps′ stores the zero-limit requirement. The structure still extends the same transformation-law data and includes holo′.

Original source ↗ · L83–85Open the complete saved source

Where this idea is used

8. The secret duet9. Two doors to the concert10. A three-note audition11. Borrow a better passport12. The workshops agree13. Pip’s impossible quilt14. The shrinking reservation15. The concert of absolute silence16. The room with no room
I’m lost · Help

Mika’s help desk

Cusp forms

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

A modular form with an additional zero-limit condition at every cusp.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

A zero function is a cusp form. The argument later needs a nonzero one in precisely the space that the vanishing theorem rules out.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →