OAI/NumberTheory/Ostmann/Construction/SpectatorNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.uniform_absolute_pair_le line 14

   Source documentation

   The same second-moment bound on both factors controls their absolute correlation. This form avoids introducing a square-root loss.

   theorem uniform_absolute_pair_le {A : Type*} [Fintype A] [Nonempty A]
       (F G : A → ℂ) (B : ℝ)
       (hF : (∑ x, ‖F x‖ ^ 2) / (Fintype.card A : ℝ) ≤ B)
       (hG : (∑ x, ‖G x‖ ^ 2) / (Fintype.card A : ℝ) ≤ B) :
       (∑ x, ‖F x * star (G x)‖) / (Fintype.card A : ℝ) ≤ B := by
   …

2. theorem OAI.Ostmann.rationalTree_absolute_pair_le line 30