OAI/NumberTheory/Ostmann/Arithmetic/SymmetrizedPairBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.finiteFamilyAverage line 12
2. theorem OAI.Ostmann.finiteFamilyAverage_norm_sq line 16
3. theorem OAI.Ostmann.finiteFamilyAverage_energy_le line 28
4. theorem OAI.Ostmann.sum_relative_function line 55
5. theorem OAI.Ostmann.finiteFamilyAverage_good_bad_bound line 61

   Source documentation

   Bad pairs are counted by a single relative permutation. No invariance of individual amplitudes or support conditions is required.

   theorem finiteFamilyAverage_good_bad_bound {J X : Type*} [Group J] [Fintype J]
       [Fintype X] (μ : X → ℝ) (A : J → X → ℂ)
       (bad : J → Prop) (B E : ℝ) (hE : 0 ≤ E)
       (hpair : ∀ i j, ‖∑ x, (μ x : ℂ) * (A i x * star (A j x))‖ ≤
         if bad (i⁻¹ * j) then B else E) :
       (∑ x, μ x * ‖finiteFamilyAverage A x‖ ^ 2) ≤
         (Fintype.card {j : J // bad j} : ℝ) / Fintype.card J * B + E := by
   …

   Mentions: OAI.Ostmann.finiteFamilyAverage