Mellin.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Mellin coefficients of a square pullback

Character orthogonality identifies the coefficient after substituting K * z^2. The factor-two estimate then follows from SquarePullback.

theorem OAI.Ostmann.sum_mulChar_units_eq_zero line 19
theorem OAI.Ostmann.sum_mulChar_units_eq_ite line 30
theorem OAI.Ostmann.mellin_orthogonality line 41
def OAI.Ostmann.mellinCoefficient line 54
Source documentation
Probability-normalized Mellin coefficient on the nonzero field elements.
```
noncomputable def mellinCoefficient {p : ℕ} [Fact p.Prime]
    (f : (ZMod p)ˣ → ℂ) (ρ : MulChar (ZMod p) ℂ) : ℂ :=
…
```

theorem OAI.Ostmann.mellinCoefficient_square_pullback line 59

Source documentation

Character orthogonality computes the square-pullback coefficient.

theorem mellinCoefficient_square_pullback {p : ℕ} [Fact p.Prime]
    (s : Finset (MulChar (ZMod p) ℂ)) (c : MulChar (ZMod p) ℂ → ℂ)
    (f : (ZMod p)ˣ → ℂ) (hf : ∀ z, f z = ∑ χ ∈ s, c χ * χ z)
    (K : (ZMod p)ˣ) (ρ : MulChar (ZMod p) ℂ) :
    mellinCoefficient (fun z => f (K * z ^ 2)) ρ =
      ∑ χ ∈ s.filter (fun χ => χ ^ 2 = ρ), c χ * χ K := by
…

Mentions: OAI.Ostmann.mellinCoefficient

theorem OAI.Ostmann.mellinCoefficient_square_pullback_bound line 94

Source documentation

Equation tree-square-pullback for a finite Mellin expansion.

theorem mellinCoefficient_square_pullback_bound {p : ℕ} [Fact p.Prime]
    (s : Finset (MulChar (ZMod p) ℂ)) (c : MulChar (ZMod p) ℂ → ℂ)
    (f : (ZMod p)ˣ → ℂ) (hf : ∀ z, f z = ∑ χ ∈ s, c χ * χ z)
    (K : (ZMod p)ˣ) (ρ : MulChar (ZMod p) ℂ) :
    ‖mellinCoefficient (fun z => f (K * z ^ 2)) ρ‖ ^ 2 ≤
      2 * ∑ χ ∈ s.filter (fun χ => χ ^ 2 = ρ), ‖c χ‖ ^ 2 := by
…

Mentions: OAI.Ostmann.mellinCoefficient