OAI/MeasureTheory/Falconer/Estimates/FinitePopularity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Quantitative popular-parameter selection in the finite incidence argument. No asymptotic notation or hidden logarithmic losses are used.

  1. theorem OAI.Falconer.finite_popular_mass line 12

    Source documentation

    Deleting points below a fixed degree threshold loses at most the threshold times the size of the whole set.

    theorem finite_popular_mass {α : Type*} (S : Finset α) (w : α → ℝ)
    {I θ L : ℝ} (hθ : 0 ≤ θ) (htotal : I ≤ ∑ x ∈ S, w x)
    (hsmall : θ*(S.card : ℝ) ≤ I/2) (hupper : ∀ x ∈ S, w x ≤ L) :
    let G := S.filter fun x => θ ≤ w x
…
  2. def OAI.Falconer.familyDegree line 33
  3. theorem OAI.Falconer.familyDegree_sum line 36
  4. theorem OAI.Falconer.family_popular_selection line 53