Exact coordinate semantics of the fourth-order obstruction.

@[reducible, inline]

abbrev PlanarMidpoint.DerivativeArray : Type

The eight entries of a linear map from planar vectors to cubic coefficients.

Equations

• PlanarMidpoint.DerivativeArray = (Fin 8 → ℝ)

def PlanarMidpoint.derivativeArray (J : E →L[ℝ] Coeff) : DerivativeArray

The columns of a cubic derivative in the fixed Euclidean basis.

Equations

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

def PlanarMidpoint.arrayApply (z : DerivativeArray) (h : E) : Coeff

Evaluation of a derivative represented by its eight coordinate entries.

Equations

• PlanarMidpoint.arrayApply z h = ![z 0 * h.ofLp 0 + z 4 * h.ofLp 1, z 1 * h.ofLp 0 + z 5 * h.ofLp 1, z 2 * h.ofLp 0 + z 6 * h.ofLp 1, z 3 * h.ofLp 0 + z 7 * h.ofLp 1]

theorem PlanarMidpoint.vec_decomp (h : E) : h = h.ofLp 0 • vec 1 0 + h.ofLp 1 • vec 0 1

theorem PlanarMidpoint.arrayApply_derivativeArray (J : E →L[ℝ] Coeff) (h : E) : arrayApply (derivativeArray J) h = J h

theorem PlanarMidpoint.derivativeArray_eq_zero_iff (J : E →L[ℝ] Coeff) : derivativeArray J = 0 ↔ J = 0

def PlanarMidpoint.arrayObstruction (c : Coeff) (z : DerivativeArray) (h : E) : E

The midpoint obstruction expressed through coordinate derivative data.

Equations

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

theorem PlanarMidpoint.arrayObstruction_derivativeArray (c : Coeff) (J : E →L[ℝ] Coeff) (h : E) : arrayObstruction c (derivativeArray J) h = obstruction c J h

def PlanarMidpoint.rows (c : Coeff) (z : DerivativeArray) : Fin 10 → ℝ

The ten scalar coefficients of the two homogeneous quartic obstruction components.

Equations

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

theorem PlanarMidpoint.kernel_iff_rows (c : Coeff) (z : DerivativeArray) : Algebra.Kernel (c 0) (c 1) (c 2) (c 3) z ↔ ∀ (i : Fin 10), rows c z i = 0

theorem PlanarMidpoint.arrayObstruction_component_0 (c : Coeff) (z : DerivativeArray) (h : E) : (arrayObstruction c z h).ofLp 0 = rows c z 0 * h.ofLp 0 ^ 4 * h.ofLp 1 ^ 0 + rows c z 1 * h.ofLp 0 ^ 3 * h.ofLp 1 ^ 1 + rows c z 2 * h.ofLp 0 ^ 2 * h.ofLp 1 ^ 2 + rows c z 3 * h.ofLp 0 ^ 1 * h.ofLp 1 ^ 3 + rows c z 4 * h.ofLp 0 ^ 0 * h.ofLp 1 ^ 4

theorem PlanarMidpoint.arrayObstruction_component_1 (c : Coeff) (z : DerivativeArray) (h : E) : (arrayObstruction c z h).ofLp 1 = rows c z 5 * h.ofLp 0 ^ 4 * h.ofLp 1 ^ 0 + rows c z 6 * h.ofLp 0 ^ 3 * h.ofLp 1 ^ 1 + rows c z 7 * h.ofLp 0 ^ 2 * h.ofLp 1 ^ 2 + rows c z 8 * h.ofLp 0 ^ 1 * h.ofLp 1 ^ 3 + rows c z 9 * h.ofLp 0 ^ 0 * h.ofLp 1 ^ 4

theorem PlanarMidpoint.quartic_coefficients_zero (a b c d e : ℝ) (h : ∀ (j : Fin 5), a * ↑↑j ^ 4 + b * ↑↑j ^ 3 + c * ↑↑j ^ 2 + d * ↑↑j + e = 0) : a = 0 ∧ b = 0 ∧ c = 0 ∧ d = 0 ∧ e = 0

theorem PlanarMidpoint.kernel_of_five_arrayObstruction_zero (c : Coeff) (z : DerivativeArray) (htest : ∀ (j : Fin 5), arrayObstruction c z (vec (↑↑j) 1) = 0) : Algebra.Kernel (c 0) (c 1) (c 2) (c 3) z

Five samples determine whether the coordinate obstruction vanishes identically.

theorem PlanarMidpoint.kernel_iff_arrayObstruction_zero (c : Coeff) (z : DerivativeArray) : Algebra.Kernel (c 0) (c 1) (c 2) (c 3) z ↔ ∀ (h : E), arrayObstruction c z h = 0

theorem PlanarMidpoint.kernel_of_obstruction_zero (c : Coeff) (J : E →L[ℝ] Coeff) (h : ∀ (v : E), obstruction c J v = 0) : Algebra.Kernel (c 0) (c 1) (c 2) (c 3) (derivativeArray J)