IncidenceSampling.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Incidence retained by the sampled labels

The first sample must preserve incidence as well as its direction counts. The retained point set then consists of points with many incident sampled labels. These assertions concern the original label spaces.

theorem OAI.Falconer.high_value_set_mass line 18

Source documentation

At least a quarter of the incidence remains on the points whose empirical incidence is at least a quarter.

theorem high_value_set_mass {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsProbabilityMeasure μ] (f : X → ℝ)
    (hf : Measurable f) (hfi : Integrable f μ) (hf1 : ∀ x, f x ≤ 1)
    {I : ℝ} (hI : 0 < I) (hmean : I / 2 ≤ ∫ x, f x ∂μ) :
    I / 4 ≤ μ.real {x | I / 4 ≤ f x} := by
…

theorem OAI.Falconer.integral_empirical_kernel line 44

theorem OAI.Falconer.exists_incidence_sample line 54

Source documentation

A direction sample can simultaneously satisfy the prescribed cell counts and leave a point set of mass at least I/4 with empirical incidence at least I/4. No coordinates of the labels are identified.

theorem exists_incidence_sample {X W κ : Type*}
    [MeasurableSpace X] [MeasurableSpace W] [DecidableEq κ]
    (μ : ProbabilityMeasure X) (ν : ProbabilityMeasure W)
    (F : X → W → ℝ) (hF : Measurable (Function.uncurry F))
    (hF0 : ∀ x w, 0 ≤ F x w) (hF1 : ∀ x w, F x w ≤ 1)
    {n : ℕ} (hn : 0 < n) (B : Finset κ) (A : κ → Set W)
    (hA : ∀ j, MeasurableSet (A j)) (p T : κ → ℝ) (L : ℝ)
    (hp : ∀ j ∈ B, 0 ≤ p j)
    (hprob : ∀ j ∈ B, (ν : Measure W).real (A j) ≤ p j)
    (hT : ∀ j ∈ B, (n : ℝ) * (Real.exp 1 - 1) * p j + L ≤ T j)
    {I : ℝ} (hI : 0 < I)
    (hmean : I ≤ ∫ w, ∫ x, F x w ∂(μ : Measure X) ∂(ν : Measure W))
…