CyclicSmoothing.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.CyclicSmoothing.window line 11
Source documentation
Convolution of a normalized nonnegative kernel with an interval (or any finite window).
```
def window {G : Type*} [AddGroup G] (K : G → ℝ) (J : Finset G) (x : G) : ℝ :=
…
```
lemma OAI.Problem337.CyclicSmoothing.window_nonneg line 14
lemma OAI.Problem337.CyclicSmoothing.window_le_one line 18
lemma OAI.Problem337.CyclicSmoothing.sum_window line 26
lemma OAI.Problem337.CyclicSmoothing.window_le_of_kernel_bound line 38

theorem OAI.Problem337.CyclicSmoothing.count_window_lower line 48

Source documentation

The counting conclusion of the smoothing argument. The spectral input is only the sampled mean lower bound; the geometric input is the kernel tail bound outside the outer window. Repeated sample values are allowed.

theorem count_window_lower {G Ω : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
    (K : G → ℝ) (inner outer : Finset G) (samples : Finset Ω) (x : Ω → G)
    (E η : ℝ) (hK : ∀ y, 0 ≤ K y) (hmass : ∑ y, K y = 1) (hη : 0 ≤ η)
    (htail : ∀ z, z ∉ outer → ∀ y ∈ inner, K (z - y) ≤ η)
    (hmean : (samples.card : ℝ) * ((inner.card : ℝ) / Fintype.card G - E) ≤
      ∑ ω ∈ samples, window K inner (x ω)) :
    (samples.card : ℝ) * ((inner.card : ℝ) / Fintype.card G - E -
      (inner.card : ℝ) * η) ≤ ((samples.filter (fun ω => x ω ∈ outer)).card : ℝ) := by
…

Mentions: OAI.Problem337.CyclicSmoothing.window