PairMoment.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The bottom-pair second moment

The valid difference/ratio coordinates identify the bottom-pair moment with the contribution of ordered distinct nonzero pairs. In particular, an L² bound suffices; no pointwise bound on the test is used.

theorem OAI.Ostmann.pairCoordinate_sum_eq line 33
theorem OAI.Ostmann.pairCoordinate_sum_le_square line 40

theorem OAI.Ostmann.bottomPair_sum_norm_sq_le line 64

Source documentation

The unnormalized bottom-pair L² estimate.

theorem bottomPair_sum_norm_sq_le {K : Type*} [Field K] [Fintype K] (g : K → ℂ) :
    (∑ dt : ValidPairCoordinates K,
      ‖g (dt.1.1 * dt.1.2 / (dt.1.2 - 1)) * conj (g (dt.1.1 / (dt.1.2 - 1)))‖ ^ 2) ≤
      (∑ x : K, ‖g x‖ ^ 2) ^ 2 := by
…

Mentions: OAI.Ostmann.ValidPairCoordinates

theorem OAI.Ostmann.bottomPair_mean_norm_sq_le line 73

Source documentation

Equation tree-R-mean: the valid bottom-pair moment is bounded by (p/(p-1))² when the field-probability squared norm is at most one.

theorem bottomPair_mean_norm_sq_le {p : ℕ} [Fact p.Prime] (g : ZMod p → ℂ)
    (hg : (∑ x : ZMod p, ‖g x‖ ^ 2) ≤ (p : ℝ)) :
    (∑ dt : ValidPairCoordinates (ZMod p),
      ‖g (dt.1.1 * dt.1.2 / (dt.1.2 - 1)) * conj (g (dt.1.1 / (dt.1.2 - 1)))‖ ^ 2) /
      ((p : ℝ) - 1) ^ 2 ≤ ((p : ℝ) / ((p : ℝ) - 1)) ^ 2 := by
…

Mentions: OAI.Ostmann.ValidPairCoordinates