OAI/NumberTheory/Ostmann/Arithmetic/FiniteRootFibres.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.rootFibreSum line 10
2. theorem OAI.Ostmann.sum_rootFibreSum line 14
3. theorem OAI.Ostmann.rootFibreSum_energy line 24

   Source documentation

   Disjoint root fibres retain the same crude finite-frequency energy cost.

   theorem rootFibreSum_energy {D R : Type*} [Fintype D] [Fintype R]
       (root : D → R) (F : D → ℂ) (E : ℝ) (hE : 0 ≤ E)
       (hF : ∀ d, ‖F d‖ ^ 2 ≤ E) :
       (∑ s, ‖rootFibreSum root s F‖ ^ 2) ≤ (Fintype.card D : ℝ) ^ 2 * E := by
   …

   Mentions: OAI.Ostmann.rootFibreSum

4. theorem OAI.Ostmann.rootFibreSum_pair line 53

   Source documentation

   Expanding before taking norms leaves only equal-root pairs.

   theorem rootFibreSum_pair {D K R : Type*} [Fintype D] [Fintype K] [Fintype R]
       (root : D → R) (root' : K → R) (F : D → ℂ) (G : K → ℂ) :
       (∑ s, rootFibreSum root s F * conj (rootFibreSum root' s G)) =
         ∑ d, ∑ k, if root d = root' k then F d * conj (G k) else 0 := by
   …

   Mentions: OAI.Ostmann.rootFibreSum

5. theorem OAI.Ostmann.rootFibreSum_weighted_pair line 72
6. theorem OAI.Ostmann.rootFibreSum_pair_bound line 90