OAI/NumberTheory/Ostmann/Quadratic/QuadraticCorrelationNormalization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.quadratic_normalization_product line 11
2. theorem OAI.Ostmann.quadratic_normalization_cancel line 26
3. theorem OAI.Ostmann.quadratic_normalized_correlation_bound line 54

   Source documentation

   After cancellation the remaining finite sum has a constant positive normalization, independent of the kernel index.

   theorem quadratic_normalized_correlation_bound {ι : Type*}
       (S : Finset ι) (σ : ι → ℝ) (A B : ι → ℂ) (R d e v C : ℝ)
       (hR : 0 < R) (hd : 0 < d) (he : 0 < e) (hv : 0 < v)
       (hσ : ∀ s ∈ S, 0 < σ s)
       (hcor : ‖∑ s ∈ S, A s * conj (B s)‖ ≤ C) :
       ‖∑ s ∈ S,
         (((Real.sqrt (R * d / (σ s * v)) : ℝ) : ℂ)⁻¹ * A s) *
           conj (((Real.sqrt (R * e / (σ s * v)) : ℝ) : ℂ)⁻¹ * B s) / (σ s : ℂ)‖ ≤
         v / (R * Real.sqrt (d * e)) * C := by
   …