MellinParseval.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Mellin inversion and Parseval on the nonzero residues

The coefficients use the probability normalization from Mellin.lean. The only character-theoretic input is the finite duality already in Mathlib.

theorem OAI.Ostmann.card_mulChar_eq_card_units line 25
Source documentation
There are exactly as many complex multiplicative characters as units.
```
theorem card_mulChar_eq_card_units {p : ℕ} [Fact p.Prime] :
    Fintype.card (MulChar (ZMod p) ℂ) = Fintype.card (ZMod p)ˣ := by
…
```

theorem OAI.Ostmann.sum_mulChar_apply_eq_ite line 31

Source documentation

Summing characters detects the identity element.

theorem sum_mulChar_apply_eq_ite {p : ℕ} [Fact p.Prime] (u : (ZMod p)ˣ) :
    (∑ χ : MulChar (ZMod p) ℂ, χ u) =
      if u = 1 then (Fintype.card (ZMod p)ˣ : ℂ) else 0 := by
…

theorem OAI.Ostmann.mellin_dual_orthogonality line 54

Source documentation

The dual orthogonality identity, with the sum over characters.

theorem mellin_dual_orthogonality {p : ℕ} [Fact p.Prime] (x z : (ZMod p)ˣ) :
    (∑ χ : MulChar (ZMod p) ℂ, χ x * conj (χ z)) =
      if x = z then (Fintype.card (ZMod p)ˣ : ℂ) else 0 := by
…

theorem OAI.Ostmann.mellin_inversion line 68

Source documentation

Full finite Mellin inversion for arbitrary complex functions on the units.

theorem mellin_inversion {p : ℕ} [Fact p.Prime]
    (f : (ZMod p)ˣ → ℂ) (x : (ZMod p)ˣ) :
    (∑ χ : MulChar (ZMod p) ℂ, mellinCoefficient f χ * χ x) = f x := by
…

Mentions: OAI.Ostmann.mellinCoefficient

theorem OAI.Ostmann.mellin_parseval line 93

Source documentation

The exact probability-normalized Parseval identity.

theorem mellin_parseval {p : ℕ} [Fact p.Prime] (f : (ZMod p)ˣ → ℂ) :
    (∑ χ : MulChar (ZMod p) ℂ, ‖mellinCoefficient f χ‖ ^ 2) =
      (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * ∑ z : (ZMod p)ˣ, ‖f z‖ ^ 2 := by
…

Mentions: OAI.Ostmann.mellinCoefficient