AngularSamples.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite sampled direction families

Ball counts for the sampled direction labels control both multiplicities and normalized ball counts of the rounded incident line families. The estimates below retain the original labels, including repeated directions.

def OAI.Falconer.roundedLineFamily line 17
theorem OAI.Falconer.roundedLineFamily_nonempty line 21
theorem OAI.Falconer.slope_close_of_roundedLine_close line 26
Source documentation
The coordinate error from rounding is at most half the grid width.
```
theorem slope_close_of_roundedLine_close {δ r m : ℝ} (hδ : 0 < δ) (hδr : δ ≤ r)
    (x l : Space 2) (hclose : dist (roundedIncidentLine δ x m) l ≤ r) :
    |m - l 0| ≤ 2 * r := by
…
```
Mentions: OAI.Falconer.Space, OAI.Falconer.roundedIncidentLine

theorem OAI.Falconer.roundedLineFamily_ball_count line 38

Source documentation

Raw ball counts for the rounded line family follow from the original direction-label counts.

theorem roundedLineFamily_ball_count {ι : Type*} [DecidableEq ι]
    {δ K b : ℝ} (hδ : 0 < δ) (x : Space 2) (m : ι → ℝ)
    (D S : Finset ι) (hSD : S ⊆ D)
    (hcount : ∀ a r : ℝ, δ ≤ r →
      ((D.filter (fun i => |m i - a| ≤ r)).card : ℝ) ≤ K * r ^ b)
    (l : Space 2) (r : ℝ) (hδr : δ ≤ r) :
    (((roundedLineFamily δ x m S).filter (fun z => dist z l ≤ r)).card : ℝ) ≤
      K * 2 ^ b * r ^ b := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.roundedLineFamily

theorem OAI.Falconer.card_le_image_card_mul_fiber_bound line 67

Source documentation

A finite map can lose only the maximum multiplicity of its fibers.

theorem card_le_image_card_mul_fiber_bound {ι α : Type*}
    [DecidableEq ι] [DecidableEq α] (S : Finset ι) (F : ι → α) {L : ℝ}
    (hF : ∀ a ∈ S.image F, ((S.filter (fun i => F i = a)).card : ℝ) ≤ L) :
    (S.card : ℝ) ≤ ((S.image F).card : ℝ) * L := by
…

theorem OAI.Falconer.roundedLineFamily_card_lower line 76

Source documentation

Even repeated original direction labels give enough distinct rounded lines: their multiplicity is controlled by one δ-ball count.

theorem roundedLineFamily_card_lower {ι : Type*} [DecidableEq ι]
    {δ K b : ℝ} (hδ : 0 < δ) (x : Space 2) (m : ι → ℝ)
    (D S : Finset ι) (hSD : S ⊆ D)
    (hcount : ∀ a : ℝ,
      ((D.filter (fun i => |m i - a| ≤ δ)).card : ℝ) ≤ K * δ ^ b) :
    (S.card : ℝ) ≤ ((roundedLineFamily δ x m S).card : ℝ) * (K * δ ^ b) := by
…

Mentions: OAI.Falconer.Space, OAI.Falconer.roundedLineFamily

theorem OAI.Falconer.roundedLineFamily_normalized_ball_bound line 99

Source documentation

The raw sampled-family bound yields exactly the normalized finite ball bound required by the published theorem.

theorem roundedLineFamily_normalized_ball_bound {ι : Type*} [DecidableEq ι]
    {δ K b L : ℝ} (hδ : 0 < δ) (x : Space 2) (m : ι → ℝ)
    (D S : Finset ι) (hSD : S ⊆ D)
    (hcount : ∀ a r : ℝ, δ ≤ r →
      ((D.filter (fun i => |m i - a| ≤ r)).card : ℝ) ≤ K * r ^ b)
    (hL : K * 2 ^ b ≤ L * ((roundedLineFamily δ x m S).card : ℝ)) :
    NormalizedFiniteBallBound δ b L (roundedLineFamily δ x m S) := by
…

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

theorem OAI.Falconer.roundedLineFamily_normalized_of_large_sample line 117

Source documentation

If a point retains an I fraction of the sampled labels, the line family has normalized loss at most 2 * 2^b * K^2 / I. The sample-size assumption is the one supplied by n = ceil (δ^(-b)).

theorem roundedLineFamily_normalized_of_large_sample {ι : Type*} [DecidableEq ι]
    {δ K I b : ℝ} (hδ : 0 < δ) (hK : 0 < K) (hI : 0 < I)
    (x : Space 2) (m : ι → ℝ) (D S : Finset ι) (hD : D.Nonempty) (hSD : S ⊆ D)
    (hsize : (D.card : ℝ) * δ ^ b ≤ 2)
    (hretained : I * (D.card : ℝ) ≤ (S.card : ℝ))
    (hcount : ∀ a r : ℝ, δ ≤ r →
      ((D.filter (fun i => |m i - a| ≤ r)).card : ℝ) ≤
        (K * (D.card : ℝ)) * r ^ b) :
    NormalizedFiniteBallBound δ b (2 * 2 ^ b * K ^ 2 / I)
      (roundedLineFamily δ x m S) := by
…

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