Fixed conformal changes of coordinates and the complete pointwise kernel classification. No position-dependent frame is differentiated.

def PlanarMidpoint.pullCoeff (s t : ℝ) (c : Coeff) : Coeff

Pullback of a cubic tensor by a fixed conformal change of coordinates.

Equations

• One or more equations did not get rendered due to their size.

def PlanarMidpoint.pullDerivative (s t : ℝ) (z : DerivativeArray) : DerivativeArray

Pullback of all four tensor indices of a cubic derivative.

Equations

• One or more equations did not get rendered due to their size.

theorem PlanarMidpoint.pullCoeff_inverse (s t : ℝ) (c : Coeff) : pullCoeff s (-t) (pullCoeff s t c) = (s ^ 2 + t ^ 2) ^ 3 • c

theorem PlanarMidpoint.pullDerivative_inverse (s t : ℝ) (z : DerivativeArray) : pullDerivative s (-t) (pullDerivative s t z) = (s ^ 2 + t ^ 2) ^ 4 • z

theorem PlanarMidpoint.pullDerivative_ne_zero (s t : ℝ) (z : DerivativeArray) (hr : s ^ 2 + t ^ 2 ≠ 0) (hz : z ≠ 0) : pullDerivative s t z ≠ 0

theorem PlanarMidpoint.kernel_pull (s t : ℝ) (c : Coeff) (z : DerivativeArray) (h : Algebra.Kernel (c 0) (c 1) (c 2) (c 3) z) : Algebra.Kernel (pullCoeff s t c 0) (pullCoeff s t c 1) (pullCoeff s t c 2) (pullCoeff s t c 3) (pullDerivative s t z)

theorem PlanarMidpoint.kernel_smul_coeff (r : ℝ) (c : Coeff) (z : DerivativeArray) (h : Algebra.Kernel (c 0) (c 1) (c 2) (c 3) z) : Algebra.Kernel ((r • c) 0) ((r • c) 1) ((r • c) 2) ((r • c) 3) z

noncomputable def PlanarMidpoint.normalizedCoeff (c : Coeff) : Coeff

Normalize a nonzero trace by a fixed conformal pullback.

Equations

• PlanarMidpoint.normalizedCoeff c = (PlanarMidpoint.radiusSq (PlanarMidpoint.trace c) ^ 2)⁻¹ • PlanarMidpoint.pullCoeff ((PlanarMidpoint.trace c).ofLp 0) ((PlanarMidpoint.trace c).ofLp 1) c

theorem PlanarMidpoint.normalizedCoeff_trace (c : Coeff) (ht : trace c ≠ 0) : normalizedCoeff c 0 + normalizedCoeff c 2 = 1 ∧ normalizedCoeff c 1 + normalizedCoeff c 3 = 0

theorem PlanarMidpoint.pullCoeff_smul (s t r : ℝ) (c : Coeff) : pullCoeff s t (r • c) = r • pullCoeff s t c

theorem PlanarMidpoint.inverse_normalizedCoeff (c : Coeff) (ht : trace c ≠ 0) : pullCoeff ((trace c).ofLp 0) (-(trace c).ofLp 1) (normalizedCoeff c) = radiusSq (trace c) • c

theorem PlanarMidpoint.eq_Q_of_normalizedCoeff (c : Coeff) (ht : trace c ≠ 0) (hn : normalizedCoeff c = ![1, 0, 0, 0]) : c = Q (trace c)

theorem PlanarMidpoint.eq_R_of_normalizedCoeff (c : Coeff) (ht : trace c ≠ 0) (hn : normalizedCoeff c = ![0, 0, 1, 0]) : c = R (trace c)

theorem PlanarMidpoint.exceptional_of_kernel (c : Coeff) (z : DerivativeArray) (hc : c ≠ 0) (hz : z ≠ 0) (h : Algebra.Kernel (c 0) (c 1) (c 2) (c 3) z) : trace c ≠ 0 ∧ (c = Q (trace c) ∨ c = R (trace c))

Complete pointwise classification: a nonzero kernel at a nonzero cubic forces one of the two exceptional graphs.