AffineAction.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Identifying the Fourier matrix of the affine action

The finite matrix from AffineFourier is the action of F(t) ↦ ∑ c(a,b) F(at+b) on nonzero additive frequencies.

theorem OAI.Ostmann.additiveFourier_sum line 17
theorem OAI.Ostmann.additiveFourier_const_mul line 24
theorem OAI.Ostmann.additiveFourier_add_right line 31
theorem OAI.Ostmann.additiveFourier_unit_mul line 41
theorem OAI.Ostmann.additiveFourier_affine_shift line 47
def OAI.Ostmann.affineAction line 54
theorem OAI.Ostmann.additiveFourier_affineAction line 58
theorem OAI.Ostmann.additiveFourier_affineAction_zero line 89
theorem OAI.Ostmann.sum_units_eq_sum_of_zero line 98

theorem OAI.Ostmann.affineAction_energy_bound line 118

Source documentation

The affine action on mean-zero functions, in counting-measure squared norm.

theorem affineAction_energy_bound {p : ℕ} [Fact p.Prime]
    (c : (ZMod p)ˣ × ZMod p → ℂ) (f : ZMod p → ℂ)
    (hf : additiveFourier f 0 = 0) :
    (∑ t : ZMod p, ‖affineAction c f t‖ ^ 2) ≤
      ((p : ℝ) * ∑ ab : (ZMod p)ˣ × ZMod p, ‖c ab‖ ^ 2) *
        ∑ t : ZMod p, ‖f t‖ ^ 2 := by
…

Mentions: OAI.Ostmann.additiveFourier, OAI.Ostmann.affineAction

theorem OAI.Ostmann.affineAction_collected_energy_bound line 142

Source documentation

The coefficient array arising from T* T has squared action norm at most 3/p.

theorem affineAction_collected_energy_bound {p : ℕ} [Fact p.Prime]
    (G : (ZMod p)ˣ → ℂ) (hG : (∑ r : (ZMod p)ˣ, ‖G r‖ ^ 2) ≤ (p : ℝ))
    (f : ZMod p → ℂ) (hf : additiveFourier f 0 = 0) :
    (∑ t : ZMod p, ‖affineAction (affineCoefficient G) f t‖ ^ 2) ≤
      (3 / (p : ℝ)) * ∑ t : ZMod p, ‖f t‖ ^ 2 := by
…

Mentions: OAI.Ostmann.additiveFourier, OAI.Ostmann.affineAction, OAI.Ostmann.affineCoefficient