OAI/NumberTheory/Ostmann/Construction/DistinctProductError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A concrete error bound for deleting repeated indices

  1. theorem OAI.Ostmann.distinct_product_error line 13
  2. theorem OAI.Ostmann.normalized_distinct_product_error line 47

    Source documentation

    For a nonempty finite population, the normalized deletion error is at most k²/J. This suffices for kernels whose bias is bounded below.

    theorem normalized_distinct_product_error {A : Type*} [Fintype A] [DecidableEq A]
    (k : ℕ) (hk : 1 ≤ k) (y : A → ℂ) (hy : ∀ a, ‖y a‖ ≤ 1)
    (hA : 0 < Fintype.card A) :
    ‖((∑ a, y a) / (Fintype.card A : ℂ)) ^ k -
      (∑ e : Fin k ↪ A, ∏ i, y (e i)) / (Fintype.card A : ℂ) ^ k‖ ≤
        (k : ℝ) ^ 2 / Fintype.card A := by
…