OAI/NumberTheory/EgyptianFractions/FourierSecondMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem337.re_finset_sum line 9
2. theorem OAI.Problem337.finite_complex_second_moment_identity line 14

   Source documentation

   Expand a finite complex second moment into pairwise correlations.

   theorem finite_complex_second_moment_identity {α β : Type*}
       (U : Finset α) (T : Finset β) (z : α → β → ℂ) :
       (∑ u ∈ U, ‖∑ t ∈ T, z u t‖ ^ 2) =
         ∑ t ∈ T, ∑ s ∈ T, (∑ u ∈ U, z u t * conj (z u s)).re := by
   …

3. theorem OAI.Problem337.finite_complex_second_moment_bound line 35

   Source documentation

   Unit phases have a second moment bounded by their diagonal contribution plus a uniform bound for all off-diagonal correlations.

   theorem finite_complex_second_moment_bound {α β : Type*}
       (U : Finset α) (T : Finset β) (z : α → β → ℂ) (E : ℝ)
       (hunit : ∀ u ∈ U, ∀ t ∈ T, ‖z u t‖ = 1)
       (hcorr : ∀ t ∈ T, ∀ s ∈ T, t ≠ s →
         ‖∑ u ∈ U, z u t * conj (z u s)‖ ≤ E) :
       (∑ u ∈ U, ‖∑ t ∈ T, z u t‖ ^ 2) ≤
         (U.card : ℝ) * T.card + (T.card : ℝ) * (T.card - 1 : ℝ) * E := by
   …

4. theorem OAI.Problem337.finite_complex_second_moment_normalized line 78

   Source documentation

   A normalized form of the off-diagonal second-moment bound.

   theorem finite_complex_second_moment_normalized {α β : Type*}
       (U : Finset α) (T : Finset β) (z : α → β → ℂ) (E : ℝ)
       (hU : U.Nonempty) (hT : T.Nonempty) (hE : 0 ≤ E)
       (hunit : ∀ u ∈ U, ∀ t ∈ T, ‖z u t‖ = 1)
       (hcorr : ∀ t ∈ T, ∀ s ∈ T, t ≠ s →
         ‖∑ u ∈ U, z u t * conj (z u s)‖ ≤ E) :
       (∑ u ∈ U, ‖(∑ t ∈ T, z u t) / (T.card : ℂ)‖ ^ 2) / (U.card : ℝ) ≤
         1 / (T.card : ℝ) + E / (U.card : ℝ) := by
   …