OAI/NumberTheory/Ostmann/Arithmetic/MatchedHistoryEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.permuted_root_energy_le line 11
2. theorem OAI.Ostmann.permuted_history_energy_le line 27

   Source documentation

   Root equality is retained in the diagonal. Uniqueness removes the entire frequency-history multiplicity from its square-energy estimate.

   theorem permuted_history_energy_le {A D R : Type*}
       [Fintype A] [Fintype D] [Fintype R]
       (e : Equiv.Perm A) (μ : A → ℝ) (root : D → R) (F : D → A → ℂ) (A₀ : ℝ)
       (hA₀ : 0 ≤ A₀) (hμ : ∀ a, 0 ≤ μ a) (hbound : ∀ a, μ a ≤ A₀)
       (hunique : ∀ a d d', F d a ≠ 0 → F d' a ≠ 0 → root d = root d' → d = d') :
       ‖∑ d, ∑ d', if root d = root d' then
         ∑ a, ((μ a * μ (e a) : ℝ) : ℂ) * (F d a * conj (F d' (e a))) else 0‖ ≤
         A₀ * ∑ d, ∑ a, μ a * ‖F d a‖ ^ 2 := by
   …