PointSamples.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Separated point sets from samples with repeated coordinates

A maximal separated subfamily covers the sampled coordinates. The bound on the multiplicity in a small ball then controls the loss in cardinality. This is the point-selection step of ang:planar-measures.

theorem OAI.Falconer.exists_separated_cover line 17

theorem OAI.Falconer.selected_points_ball_count line 50

Source documentation

Distinct selected coordinates in a ball cannot outnumber the original sample labels in that ball.

theorem selected_points_ball_count {ι : Type*} [DecidableEq ι]
    (D : Finset ι) (p : ι → Space 2) (P : Finset (Space 2))
    (hP : P ⊆ D.image p) (z : Space 2) (r : ℝ) :
    (P.filter (fun x => dist x z ≤ r)).card ≤
      (D.filter (fun i => dist (p i) z ≤ r)).card := by
…

Mentions: OAI.Falconer.Space

theorem OAI.Falconer.selected_points_card_lower line 66

Source documentation

Covering the original labels by the selected point balls gives the lower cardinality bound, with all repeated labels counted.

theorem selected_points_card_lower {ι : Type*} [DecidableEq ι]
    (D : Finset ι) (p : ι → Space 2) (P : Finset (Space 2))
    {δ L : ℝ} (hcover : ∀ i ∈ D, ∃ x ∈ P, dist (p i) x ≤ δ)
    (hcount : ∀ x ∈ P, ((D.filter (fun i => dist (p i) x ≤ δ)).card : ℝ) ≤ L) :
    (D.card : ℝ) ≤ (P.card : ℝ) * L := by
…

Mentions: OAI.Falconer.Space

theorem OAI.Falconer.selected_points_normalized_ball_bound line 87

Source documentation

The selected separated point set has the normalized finite ball bound required by the published Furstenberg theorem.

theorem selected_points_normalized_ball_bound {ι : Type*} [DecidableEq ι]
    (D : Finset ι) (p : ι → Space 2) (P : Finset (Space 2))
    {δ K f : ℝ} (hδ : 0 < δ) (hK : 0 < K) (hD : D.Nonempty)
    (hP : P ⊆ D.image p)
    (hcover : ∀ i ∈ D, ∃ x ∈ P, dist (p i) x ≤ δ)
    (hsize : (D.card : ℝ) * δ ^ f ≤ 2)
    (hcount : ∀ z r, δ ≤ r → ((D.filter (fun i => dist (p i) z ≤ r)).card : ℝ) ≤
      K * (D.card : ℝ) * r ^ f) :
    NormalizedFiniteBallBound δ f (2 * K^2) P := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.NormalizedFiniteBallBound

theorem OAI.Falconer.exists_separated_point_sample line 116