AllDimensionalGraphGeometry.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Geometry of the retained graph in arbitrary dimension

The graph tests use orthogonal distance to a line and one scalar longitudinal constraint. Each longitudinal constraint is in the unknown endpoint's own cap direction. In particular these bounds do not divide by the angle between the two endpoint directions.

def OAI.Falconer.perpendicularPart line 22
Source documentation
Perpendicular displacement from the line in a unit direction.
```
def perpendicularPart (w v : E) : E := v - inner ℝ w v • w
```
theorem OAI.Falconer.perpendicularPart_sub line 24
theorem OAI.Falconer.norm_perpendicularPart_le line 30
Source documentation
Orthogonal projection is a contraction.
```
theorem norm_perpendicularPart_le {w : E} (hw : ‖w‖ = 1) (v : E) :
    ‖perpendicularPart w v‖ ≤ ‖v‖ := by
…
```
Mentions: OAI.Falconer.perpendicularPart
theorem OAI.Falconer.perpendicularPart_direction_error line 41
Source documentation
Moving a unit direction changes the perpendicular test by at most twice its angular displacement times the size of the tested vector.
```
theorem perpendicularPart_direction_error {w z : E} (hw : ‖w‖ = 1) (hz : ‖z‖ = 1)
    (v : E) :
    ‖perpendicularPart w v - perpendicularPart z v‖ ≤ 2 * ‖w-z‖ * ‖v‖ := by
…
```
Mentions: OAI.Falconer.perpendicularPart
theorem OAI.Falconer.perpendicularPart_test_error line 60
Source documentation
The error in a graph perpendicular test from both point and cap replacement is controlled uniformly in the dimension.
```
theorem perpendicularPart_test_error {w z : E} (hw : ‖w‖ = 1) (hz : ‖z‖ = 1)
    (u v : E) :
    ‖perpendicularPart w u - perpendicularPart z v‖ ≤
      ‖u-v‖ + 2 * ‖w-z‖ * ‖v‖ := by
…
```
Mentions: OAI.Falconer.perpendicularPart

theorem OAI.Falconer.longitudinal_test_error line 72

Source documentation

Scalar phase error under point and cap replacement.

theorem longitudinal_test_error {w z : E} (hw : ‖w‖ = 1) (u v : E) :
    |inner ℝ w u - inner ℝ z v| ≤ ‖u-v‖ + ‖w-z‖ * ‖v‖ := by
…

theorem OAI.Falconer.norm_le_longitudinal_add_perpendicular line 87
Source documentation
A perpendicular tube and a longitudinal interval together confine the unknown point to a ball, regardless of any other direction in the graph.
```
theorem norm_le_longitudinal_add_perpendicular {w : E} (hw : ‖w‖ = 1) (v : E) :
    ‖v‖ ≤ |inner ℝ w v| + ‖perpendicularPart w v‖ := by
…
```
Mentions: OAI.Falconer.perpendicularPart
theorem OAI.Falconer.two_test_diameter line 99
Source documentation
Difference of two points satisfying the same scalar interval and the same perpendicular tube belongs to a ball of the expected radius.
```
theorem two_test_diameter {w : E} (hw : ‖w‖ = 1) {u v : E} {a b : ℝ}
    (hlong : |inner ℝ w u - inner ℝ w v| ≤ a)
    (hperp : ‖perpendicularPart w u - perpendicularPart w v‖ ≤ b) :
    ‖u-v‖ ≤ a+b := by
…
```
Mentions: OAI.Falconer.perpendicularPart

theorem OAI.Falconer.retained_candidates_diameter line 113

Source documentation

When each point lies in a tube of radius τ and its scalar coordinate in an interval of half-width τ, the full candidate diameter is at most 4τ.

theorem retained_candidates_diameter {w : E} (hw : ‖w‖ = 1) {u v : E} {c τ : ℝ}
    (hu : |inner ℝ w u - c| ≤ τ) (hv : |inner ℝ w v - c| ≤ τ)
    (hpu : ‖perpendicularPart w u‖ ≤ τ) (hpv : ‖perpendicularPart w v‖ ≤ τ) :
    ‖u-v‖ ≤ 4*τ := by
…

Mentions: OAI.Falconer.perpendicularPart

theorem OAI.Falconer.witness_tube_bound line 128

Source documentation

Two centers retained in one cap lie in a slightly wider tube in any nearby witness direction. This is the geometric input to the parallel test.

theorem witness_tube_bound {w w₀ : E} (hw : ‖w‖ = 1) (hw₀ : ‖w₀‖ = 1)
    {u v z : E} {τ δ L : ℝ} (hδ : 0 ≤ δ)
    (hu : ‖perpendicularPart w₀ (u-z)‖ ≤ τ)
    (hv : ‖perpendicularPart w₀ (v-z)‖ ≤ τ)
    (hclose : ‖w-w₀‖ ≤ δ) (hsize : ‖u-v‖ ≤ L) :
    ‖perpendicularPart w (u-v)‖ ≤ 2*τ + 2*δ*L := by
…

Mentions: OAI.Falconer.perpendicularPart