AffineCoefficients.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The affine coefficient array

The identity fiber is diagonal, and all other fibers have size at most two. These facts give the coefficient-square estimate in equation tree-affine-coefficient-norm without a pointwise bound on the function.

theorem OAI.Ostmann.norm_sum_sq_le_card_mul line 19
theorem OAI.Ostmann.affineParameters_eq_identity_iff line 23
def OAI.Ostmann.affineCoefficientSum line 39
Source documentation
The unnormalized coefficients obtained by collecting ordered unit pairs.
```
noncomputable def affineCoefficientSum {p : ℕ} [Fact p.Prime] (G : (ZMod p)ˣ → ℂ)
    (ab : (ZMod p)ˣ × ZMod p) : ℂ :=
…
```
theorem OAI.Ostmann.affineCoefficientSum_identity line 44
theorem OAI.Ostmann.affineCoefficientSum_nonidentity_bound line 52
theorem OAI.Ostmann.affineCoefficientSum_sq_sum line 70

def OAI.Ostmann.affineCoefficient line 112

Source documentation

The coefficient normalization for the operator T* T.

noncomputable def affineCoefficient {p : ℕ} [Fact p.Prime]
    (G : (ZMod p)ˣ → ℂ) (ab : (ZMod p)ˣ × ZMod p) : ℂ :=
…

theorem OAI.Ostmann.affineCoefficient_sq_sum_le line 117

Source documentation

Equation tree-affine-coefficient-norm, with the probability L² hypothesis.

theorem affineCoefficient_sq_sum_le {p : ℕ} [Fact p.Prime]
    (G : (ZMod p)ˣ → ℂ) (hG : (∑ r : (ZMod p)ˣ, ‖G r‖ ^ 2) ≤ (p : ℝ)) :
    (∑ ab : (ZMod p)ˣ × ZMod p, ‖affineCoefficient G ab‖ ^ 2) ≤
      3 / (p : ℝ) ^ 2 := by
…

Mentions: OAI.Ostmann.affineCoefficient