funlean.
Step 49 / 64

University

Coefficients as arithmetic data

An expansion expresses the function through a sequence of numbers.

Start with a concrete example

In 1 + 2x + 3x², the numbers 1, 2 and 3 tell us how much of each part to use. Change x and watch the three contributions.

112×243×2²12

x = 2：1 + 4 + 12 = 17

How this example differs from the definition

A finite polynomial makes the idea visible. The form in the proof has a different expansion and arithmetic conditions.

A small check: try the idea

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

With x = 2, how much does the part 3x² contribute?

Read the answer and reasoning

12. Square first: x² = 4, then multiply by the coefficient 3: 3×4 = 12. Inspect the third bar.

Build the idea in three steps

  1. A polynomial such as 2 + 3x + 5x² has a sequence of coefficients: 2, 3, 5.
  2. Modular forms have an expansion called a q-expansion. Its coefficients carry arithmetic information.
  3. qCoeff f n takes the nth coefficient of the expansion of f. The expansion theory is deeper than the polynomial example.

A small example

The matching colored beads stand for matching coefficients at specified indices, not matching the shapes of two pictures.

Lean definition · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_Modularity.lean

def qCoeff (f : ℍ → ℂ) (n : ℕ) : ℂ :=  (qExpansion 1 f).coeff n

How to read this Lean

qExpansion 1 f builds the expansion; .coeff n selects the coefficient. The parameter 1 here is not the weight of f.

Original source ↗ · L19–20Open 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 reservation
I’m lost · Help

Mika’s help desk

Coefficients as arithmetic data

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

An expansion expresses the function through a sequence of numbers.

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

A small clue

The matching colored beads stand for matching coefficients at specified indices, not matching the shapes of two pictures.

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 →