Coordinate lines and finite crossing times

Each tie on a nonexceptional coordinate line has an explicit transverse crossing time.

def LiebThirring.coordinateLine (a : Fin 3) (q : Planar) (t : ℝ) : Position

Insert the coordinate along which the line is sliced.

Equations

• LiebThirring.coordinateLine a q t = WithLp.toLp 2 (a.insertNth t fun (i : Fin 2) => q.ofLp i)

@[simp]

theorem LiebThirring.coordinateLine_apply_same (a : Fin 3) (q : Planar) (t : ℝ) : (coordinateLine a q t).ofLp a = t

@[simp]

theorem LiebThirring.coordinateLine_apply_succAbove (a : Fin 3) (q : Planar) (t : ℝ) (i : Fin 2) : (coordinateLine a q t).ofLp (a.succAbove i) = q.ofLp i

@[simp]

theorem LiebThirring.planeProjection_coordinateLine (a : Fin 3) (q : Planar) (t : ℝ) : planeProjection a (coordinateLine a q t) = q

theorem LiebThirring.coordinateLine_eq_affine (a : Fin 3) (q : Planar) (t : ℝ) : coordinateLine a q t = coordinateLine a q 0 + t • coordinateLine a 0 1

theorem LiebThirring.contDiff_coordinateLine (a : Fin 3) (q : Planar) (n : WithTop ℕ∞) : ContDiff ℝ n (coordinateLine a q)