IncidenceSamples.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform sampling with incidence and good point labels

Both sampling stages use original probability laws. In the point stage, the good labels are selected after sampling, so no measurable selection or identification of coincident spatial coordinates is required.

theorem OAI.Falconer.exists_uniform_incidence_sample line 19

theorem OAI.Falconer.exists_good_separated_point_sample line 70

Source documentation

Sample from the original point law, retain the labels in a positive mass set, and extract a separated point set. Repeated coordinates cost only the proved ball-count factor.

theorem exists_good_separated_point_sample {X : Type*} [MeasurableSpace X]
    (μ : ProbabilityMeasure X) (p : X → Space 2) (hp : Measurable p)
    (hpbound : ∀ x i, |p x i| ≤ 1)
    (G : Set X) (hG : MeasurableSet G) {J : ℝ} (hJ : 0 < J)
    (hGmass : J ≤ (μ : Measure X).real G)
    {n L H : ℕ} (hn : 0 < n) {δ s K B : ℝ}
    (hδ : 0 < δ) (hs : 0 ≤ s) (hK : 0 ≤ K) (hB : 1 ≤ B)
    (hL : δ⁻¹+1 ≤ L) (hH : δ⁻¹ ≤ H)
    (hsize : 1 ≤ (n : ℝ) * δ^s) (hsize' : (n : ℝ) * δ^s ≤ 2)
    (hprob : ∀ c r, δ ≤ r →
      (μ : Measure X).real {x | dist (p x) c ≤ r} ≤ K * r^s)
    (hsmall : (((2*L+1)^2 * H : ℕ) : ℝ) * exp (-B) ≤ J/4) :
…

Mentions: OAI.Falconer.Space