AffineOperator.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The weighted affine averaging operator

This is the operator in equation tree-affine-coefficient, together with its adjoint. Its adjoint square is the affine action whose coefficient energy is bounded in AffineCoefficients.

def OAI.Ostmann.affineGenerator line 17
def OAI.Ostmann.affineGeneratorInv line 20
def OAI.Ostmann.affineGeneratorEquiv line 23
theorem OAI.Ostmann.affineGenerator_comp_inv line 36

def OAI.Ostmann.affineAverage line 47

Source documentation

The paper uses this with weights W r = conj (G r).

noncomputable def affineAverage {p : ℕ} [Fact p.Prime]
    (W : (ZMod p)ˣ → ℂ) (F : ZMod p → ℂ) (t : ZMod p) : ℂ :=
…

def OAI.Ostmann.affineAverageAdjoint line 51
theorem OAI.Ostmann.affineGenerator_inner_reindex line 55
theorem OAI.Ostmann.affineAverage_adjoint_identity line 68
theorem OAI.Ostmann.affineCoefficientSum_action line 91
theorem OAI.Ostmann.affineAverage_adjoint_square line 105
Source documentation
The adjoint square is the affine action with the collected coefficient array.
```
theorem affineAverage_adjoint_square {p : ℕ} [Fact p.Prime]
    (W : (ZMod p)ˣ → ℂ) (F : ZMod p → ℂ) :
    affineAverageAdjoint W (affineAverage W F) = affineAction (affineCoefficient W) F := by
…
```
Mentions: OAI.Ostmann.affineAverageAdjoint, OAI.Ostmann.affineAverage, OAI.Ostmann.affineAction, OAI.Ostmann.affineCoefficient

theorem OAI.Ostmann.affineAverage_energy_sq_bound line 134

Source documentation

Squared form of the mean-zero operator bound from Section 6.

theorem affineAverage_energy_sq_bound {p : ℕ} [Fact p.Prime]
    (W : (ZMod p)ˣ → ℂ) (hW : (∑ r : (ZMod p)ˣ, ‖W r‖ ^ 2) ≤ (p : ℝ))
    (F : ZMod p → ℂ) (hF : additiveFourier F 0 = 0) :
    (∑ t : ZMod p, ‖affineAverage W F t‖ ^ 2) ^ 2 ≤
      (3 / (p : ℝ)) * (∑ t : ZMod p, ‖F t‖ ^ 2) ^ 2 := by
…

Mentions: OAI.Ostmann.additiveFourier, OAI.Ostmann.affineAverage

theorem OAI.Ostmann.affineAverage_energy_bound line 158