The normal component of the planar projection Jacobian

Deleting one row and the last column of an orthogonal matrix gives an absolute minor equal to the corresponding last-column entry.

The two unit direction vectors of an orthonormal affine frame.

theorem LiebThirring.abs_det_minor_eq_abs_last_column (Q : Matrix (Fin 3) (Fin 3) ℝ) (hQ : Q.transpose * Q = 1) (a : Fin 3) : |(Q.submatrix a.succAbove (Fin.succAbove 2)).det| = |Q a 2|

Deleting one row and the last column of an orthogonal matrix gives an absolute minor equal to the corresponding last-column entry.

noncomputable def LiebThirring.planeFrameVector (n b : Position) (F : PlaneFrame (affinePlane n b)) (i : Fin 2) : Position

The two unit direction vectors of an orthonormal affine frame.

Equations

• LiebThirring.planeFrameVector n b F i = ↑((AffineIsometryEquiv.linearIsometryEquiv F) ((EuclideanSpace.basisFun (Fin 2) ℝ) i))

theorem LiebThirring.inner_planeFrameVector (n b : Position) (F : PlaneFrame (affinePlane n b)) (i j : Fin 2) : inner ℝ (planeFrameVector n b F i) (planeFrameVector n b F j) = if i = j then 1 else 0

The frame direction vectors are orthonormal.

theorem LiebThirring.inner_normal_planeFrameVector (n b : Position) (F : PlaneFrame (affinePlane n b)) (i : Fin 2) : inner ℝ n (planeFrameVector n b F i) = 0

The frame direction vectors are perpendicular to the given normal.

noncomputable def LiebThirring.planeFrameMatrix (n b : Position) (F : PlaneFrame (affinePlane n b)) : Matrix (Fin 3) (Fin 3) ℝ

Columns of the affine frame's linear part, followed by the normal.

Equations

• LiebThirring.planeFrameMatrix n b F i j = (![LiebThirring.planeFrameVector n b F 0, LiebThirring.planeFrameVector n b F 1, n] j).ofLp i

theorem LiebThirring.planeFrameMatrix_inner_columns (n b : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (i j : Fin 3) : inner ℝ (![planeFrameVector n b F 0, planeFrameVector n b F 1, n] i) (![planeFrameVector n b F 0, planeFrameVector n b F 1, n] j) = if i = j then 1 else 0

The completed frame columns are orthonormal when its normal has unit norm.

theorem LiebThirring.planeFrameMatrix_transpose_mul (n b : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) : (planeFrameMatrix n b F).transpose * planeFrameMatrix n b F = 1

The completed frame matrix is orthogonal when its normal has unit norm.

theorem LiebThirring.planeProjectionChart_toMatrix (n b : Position) (a : Fin 3) (ha : n.ofLp a ≠ 0) (F : PlaneFrame (affinePlane n b)) : (LinearMap.toMatrix (PiLp.basisFun 2 ℝ (Fin 2)) (PiLp.basisFun 2 ℝ (Fin 2))) ↑(planeProjectionChart n b a ha F).linear = (planeFrameMatrix n b F).submatrix a.succAbove (Fin.succAbove 2)

The projection chart's matrix is the corresponding minor of the completed frame.

theorem LiebThirring.abs_det_planeProjectionChart (n b : Position) (hn : ‖n‖ = 1) (a : Fin 3) (ha : n.ofLp a ≠ 0) (F : PlaneFrame (affinePlane n b)) : |LinearMap.det ↑(planeProjectionChart n b a ha F).linear| = |n.ofLp a|

The absolute area Jacobian of coordinate deletion is the absolute normal component.