OAI/NumberTheory/Ostmann/QuadraticCenter/WeightedCorrelationEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.weighted_sum_energy_gram line 12
2. theorem OAI.Ostmann.weighted_sum_energy_le_correlations line 39
3. theorem OAI.Ostmann.divisor_combination_energy_bound line 53
4. theorem OAI.Ostmann.uniform_divisor_combination_energy_bound line 86

   Source documentation

   A uniform pair bound costs exactly the square of the divisor-weight sum.

   theorem uniform_divisor_combination_energy_bound {ι : Type*}
       (S : Finset ι) (P : Finset ℕ) (μ : ι → ℝ)
       (c : Finset ℕ → ℂ) (G : Finset ℕ → ι → ℂ) (lam C : ℝ)
       (hlam : 0 ≤ lam) (_hC : 0 ≤ C)
       (hc : ∀ U ∈ P.powerset, ‖c U‖ ≤ lam ^ U.card)
       (hpair : ∀ U ∈ P.powerset, ∀ V ∈ P.powerset,
         ‖∑ s ∈ S, (μ s : ℂ) * (G U s * conj (G V s))‖ ≤ C) :
       (∑ s ∈ S, μ s * ‖∑ U ∈ P.powerset, c U * G U s‖ ^ 2) ≤
         C * (1 + lam) ^ (2 * P.card) := by
   …