QuadraticCorrelationExpansion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Expanding the two finite quadratic sums before the kernel average

theorem OAI.Ostmann.finite_correlation_expansion line 11
theorem OAI.Ostmann.finite_correlation_pair_bound line 21

theorem OAI.Ostmann.normalized_quadratic_pair_bound line 37

Source documentation

The exact normalized pair count is all that remains after bounding each expanded pair by the translated periodic estimate.

theorem normalized_quadratic_pair_bound {ι κ υ : Type*}
    (S : Finset ι) (W : Finset κ) (V : Finset υ) (σ : ι → ℝ)
    (F : κ → ι → ℂ) (G : υ → ι → ℂ) (R d e v B : ℝ)
    (hR : 0 < R) (hd : 0 < d) (he : 0 < e) (hv : 0 < v)
    (hσ : ∀ s ∈ S, 0 < σ s)
    (hB : ∀ w ∈ W, ∀ v ∈ V, ‖∑ s ∈ S, F w s * conj (G v s)‖ ≤ B) :
    ‖∑ s ∈ S,
      (((Real.sqrt (R * d / (σ s * v)) : ℝ) : ℂ)⁻¹ * ∑ w ∈ W, F w s) *
        conj (((Real.sqrt (R * e / (σ s * v)) : ℝ) : ℂ)⁻¹ * ∑ v ∈ V, G v s) / (σ s : ℂ)‖ ≤
      v / (R * Real.sqrt (d * e)) * ((W.card : ℝ) * V.card * B) := by
…

theorem OAI.Ostmann.quadratic_pair_count_cancellation line 51

Source documentation

The support pair count cancels the normalization and the interval length.

theorem quadratic_pair_count_cancellation (R d e v N C A H : ℝ)
    (hR : 0 < R) (hd : 0 < d) (he : 0 < e) (hv : 0 < v) (hN : 0 < N)
    (hC : 0 ≤ C) (hA : 0 ≤ A) (J J' : ℕ)
    (hJ : (J : ℝ) * J' ≤ H * R * Real.sqrt (d * e) / (N * v)) :
    v / (R * Real.sqrt (d * e)) * ((J : ℝ) * J' * (C * A * N)) ≤ H * C * A := by
…