TestFunctions.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Transfer from collision distance to test functions

The tests need only a bounded squared norm, not a pointwise bound. This is the Cauchy--Schwarz estimate immediately following Lemma 2.5 in the paper.

theorem OAI.Ostmann.complex_weighted_sum_sq line 17

theorem OAI.Ostmann.centered_test_bound line 33

Source documentation

The empirical test error is bounded by the squared distance of the mass function from the uniform mass on its support, times the test's energy.

theorem centered_test_bound {α : Type*} (s : Finset α) (μ : α → ℝ)
    (f : α → ℂ) (p : ℝ) (hf : (∑ r ∈ s, ‖f r‖ ^ 2) ≤ p) :
    ‖∑ r ∈ s, ((μ r - 1 / (s.card : ℝ) : ℝ) : ℂ) * f r‖ ^ 2 ≤
      p * ∑ r ∈ s, (μ r - 1 / (s.card : ℝ)) ^ 2 := by
…