ProjectedDirections.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Lifting auxiliary radial directions

The integer-cap argument in prep:integer-caps uses the map w ↦ P w / ‖P w‖ only where projected separation bounds ‖P w‖ away from zero. These elementary facts keep the auxiliary direction map separate from the original Euclidean distance map.

theorem OAI.Falconer.normalize_dist_le line 26

Source documentation

Normalization is Lipschitz on vectors whose norms are bounded below.

theorem normalize_dist_le {v w : E} {c : ℝ} (hc : 0 < c)
    (hv : c ≤ ‖v‖) (hw : c ≤ ‖w‖) :
    dist (normalize v) (normalize w) ≤ (2 / c) * dist v w := by
…

theorem OAI.Falconer.normalize_map_radial line 55

Source documentation

A linear map commutes with radial directions after re-normalization.

theorem normalize_map_radial (P : E →L[ℝ] F) {x y : E} (hxy : y ≠ x) :
    normalize (P (normalize (y - x))) = normalize (P y - P x) := by
…

theorem OAI.Falconer.normalized_projection_dist_le line 63

Source documentation

The auxiliary normalized projection has a uniform Lipschitz bound on the part of the sphere on which projected separation is available.

theorem normalized_projection_dist_le (P : E →L[ℝ] F) {c : ℝ} (hc : 0 < c)
    (hP : ‖P‖ ≤ 1) {v w : E} (hv : c ≤ ‖P v‖) (hw : c ≤ ‖P w‖) :
    dist (normalize (P v)) (normalize (P w)) ≤ (2 / c) * dist v w := by
…