AffineMean.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Constant and mean-zero parts of the affine average

The self-correlation estimate here is the operator inequality used to prove the uniform Mellin estimate in Section 6.

theorem OAI.Ostmann.fieldMean_eq_sum line 17
def OAI.Ostmann.unitMean line 21
theorem OAI.Ostmann.affineAverage_mean line 24
theorem OAI.Ostmann.affineAverage_centered line 41
theorem OAI.Ostmann.affineAverage_centered_function line 49
theorem OAI.Ostmann.affineAverage_full_energy_bound line 55
theorem OAI.Ostmann.unitMean_conj_of_zero line 68

theorem OAI.Ostmann.affineAverage_self_correlation_bound line 77

Source documentation

The exact affine self-correlation estimate underlying src42.

theorem affineAverage_self_correlation_bound {p : ℕ} [Fact p.Prime]
    (G : ZMod p → ℂ) (hG0 : G 0 = 0)
    (hG : (∑ t : ZMod p, ‖G t‖ ^ 2) ≤ (p : ℝ)) :
    (∑ t : ZMod p, ‖affineAverage (fun r : (ZMod p)ˣ => conj (G r)) G t‖ ^ 2) /
      (p : ℝ) ≤ ‖fieldMean G‖ ^ 4 + Real.sqrt (3 / (p : ℝ)) := by
…

Mentions: OAI.Ostmann.affineAverage, OAI.Ostmann.fieldMean

theorem OAI.Ostmann.affineAverage_self_correlation_unit_bound line 94

Source documentation

Restricting the output to units costs only the factor p/(p-1).

theorem affineAverage_self_correlation_unit_bound {p : ℕ} [Fact p.Prime]
    (G : ZMod p → ℂ) (hG0 : G 0 = 0)
    (hG : (∑ t : ZMod p, ‖G t‖ ^ 2) ≤ (p : ℝ)) :
    (∑ t : (ZMod p)ˣ, ‖affineAverage (fun r : (ZMod p)ˣ => conj (G r)) G t‖ ^ 2) /
      ((p : ℝ) - 1) ≤ ((p : ℝ) / ((p : ℝ) - 1)) *
        (‖fieldMean G‖ ^ 4 + Real.sqrt (3 / (p : ℝ))) := by
…

Mentions: OAI.Ostmann.affineAverage, OAI.Ostmann.fieldMean