IncidenceForest.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Incidence forests for independent affine directions

An edge is cut by the coordinate of its line direction. All other lines preserve this coordinate. On the selected line the coordinate determines the point, so the deleted edge is the only crossing of the cut.

theorem OAI.TwoPointCorrelations.independent_coordinate_functionals line 22

Source documentation

Linear coordinates on an independent family, extended to the ambient space.

theorem independent_coordinate_functionals [DecidableEq ι] (d : ι → V) (hd : LinearIndependent K d) :
    ∃ φ : ι → V →ₗ[K] K, ∀ i j, φ i (d j) = if i = j then 1 else 0 := by
…

def OAI.TwoPointCorrelations.affineIncidenceGraph line 37
Source documentation
Line vertices and point vertices are distinct, even when their types coincide.
```
def affineIncidenceGraph (anchor d : ι → V) : SimpleGraph (ι ⊕ V) where
…
```
theorem OAI.TwoPointCorrelations.coordinate_injective_on_line line 47
def OAI.TwoPointCorrelations.edgeSide line 57
theorem OAI.TwoPointCorrelations.edgeSide_incidence line 62

theorem OAI.TwoPointCorrelations.affineIncidenceGraph_edge_isBridge line 81

Source documentation

Every incidence edge is a bridge when line directions are independent.

theorem affineIncidenceGraph_edge_isBridge (anchor d : ι → V)
    (hd : LinearIndependent K d) (i : ι) (x : V)
    (hx : ∃ t : K, x = anchor i + t • d i) :
    (affineIncidenceGraph (K := K) anchor d).IsBridge s(Sum.inl i, Sum.inr x) := by
…

Mentions: OAI.TwoPointCorrelations.affineIncidenceGraph

theorem OAI.TwoPointCorrelations.affineIncidenceGraph_isAcyclic line 122
Source documentation
One affine line per independent direction has an acyclic incidence graph.
```
theorem affineIncidenceGraph_isAcyclic (anchor d : ι → V)
    (hd : LinearIndependent K d) : (affineIncidenceGraph (K := K) anchor d).IsAcyclic := by
…
```
Mentions: OAI.TwoPointCorrelations.affineIncidenceGraph
theorem OAI.TwoPointCorrelations.incidence_walk_unique line 138
Source documentation
A run sequence without immediate reversal is recovered from its two endpoints.
```
theorem incidence_walk_unique (anchor d : ι → V) (hd : LinearIndependent K d)
    {u v : ι ⊕ V} (p q : (affineIncidenceGraph (K := K) anchor d).Walk u v)
…
```
Mentions: OAI.TwoPointCorrelations.affineIncidenceGraph