UniformSamples.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform ball bounds for the original sampled labels

The finite query estimate is transferred to every ball, without identifying labels that happen to have the same spatial coordinate.

theorem OAI.Falconer.iidCount_mono line 17
theorem OAI.Falconer.iidCount_le_card line 26
theorem OAI.Falconer.iidCount_eq_card_filter line 31
theorem OAI.Falconer.uniform_ball_count_of_queries line 35

theorem OAI.Falconer.exists_uniform_ball_sample line 79

Source documentation

Simultaneous ball control and retained empirical incidence. The explicit failure budget depends only on the polynomial number of grid queries.

theorem exists_uniform_ball_sample {X : Type*} [MeasurableSpace X]
    (ν : ProbabilityMeasure X) (p : X → Space 2) (hp : Measurable p)
    (hpbound : ∀ x i, |p x i| ≤ 1)
    {n L H : ℕ} (hn : 0 < n) {δ s K B I : ℝ}
    (hδ : 0 < δ) (hs : 0 ≤ s) (hK : 0 ≤ K) (hB : 1 ≤ B)
    (hL : δ⁻¹+1 ≤ L) (hH : δ⁻¹ ≤ H)
    (hsize : 1 ≤ (n : ℝ) * δ^s)
    (hprob : ∀ c r, δ ≤ r →
      (ν : Measure X).real {x | dist (p x) c ≤ r} ≤ K * r^s)
    (f : X → ℝ) (hf : Integrable f (ν : Measure X)) (hf1 : ∀ x, f x ≤ 1)
    (hI : 0 < I) (hmean : I ≤ ∫ x, f x ∂(ν : Measure X))
    (hsmall : (((2*L+1)^2 * H : ℕ) : ℝ) * exp (-B) ≤ I/4) :
…

Mentions: OAI.Falconer.Space