Planar symmetric cubic tensors

The four entries are the coefficients C₁₁₁, C₁₁₂, C₁₂₂, C₂₂₂ of a totally symmetric cubic tensor. The Euclidean pairing identifies it with the bilinear Christoffel tensor K. The derivative index in obstruction is unrestricted.

@[reducible, inline]

abbrev PlanarMidpoint.E : Type

The Euclidean plane with its standard inner product and norm.

Equations

• PlanarMidpoint.E = EuclideanSpace ℝ (Fin 2)

@[reducible, inline]

abbrev PlanarMidpoint.Coeff : Type

The four independent coefficients of a totally symmetric planar cubic tensor.

Equations

• PlanarMidpoint.Coeff = (Fin 4 → ℝ)

@[reducible, inline]

noncomputable abbrev PlanarMidpoint.midpointTime : ℝ

The affine midpoint parameter, explicitly named to keep independent statements identical.

Equations

• PlanarMidpoint.midpointTime = 1 / 2

def PlanarMidpoint.vec (x y : ℝ) : E

A planar vector specified by its two standard coordinates.

Equations

• PlanarMidpoint.vec x y = !₂[x, y]

@[simp]

theorem PlanarMidpoint.vec_zero (x y : ℝ) : (vec x y).ofLp 0 = x

@[simp]

theorem PlanarMidpoint.vec_one (x y : ℝ) : (vec x y).ofLp 1 = y

theorem PlanarMidpoint.vec_ext {u v : E} (h₀ : u.ofLp 0 = v.ofLp 0) (h₁ : u.ofLp 1 = v.ofLp 1) : u = v

def PlanarMidpoint.K (c : Coeff) (u v : E) : E

The symmetric bilinear Christoffel tensor obtained by raising a cubic index.

Equations

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

def PlanarMidpoint.cubic (c : Coeff) (u v w : E) : ℝ

The symmetric trilinear form represented by the four cubic coefficients.

Equations

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

def PlanarMidpoint.trace (c : Coeff) : E

The contraction of a planar cubic tensor against the Euclidean metric.

Equations

• PlanarMidpoint.trace c = PlanarMidpoint.vec (c 0 + c 2) (c 1 + c 3)

def PlanarMidpoint.obstruction (c : Coeff) (J : E →L[ℝ] Coeff) (h : E) : E

The quartic midpoint obstruction with an unrestricted derivative slot.

Equations

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

theorem PlanarMidpoint.K_symm (c : Coeff) (u v : E) : K c u v = K c v u

theorem PlanarMidpoint.cubic_swap_left (c : Coeff) (u v w : E) : cubic c u v w = cubic c v u w

theorem PlanarMidpoint.cubic_swap_right (c : Coeff) (u v w : E) : cubic c u v w = cubic c u w v

theorem PlanarMidpoint.cubic_diagonal (c : Coeff) (u : E) : cubic c u u u = c 0 * u.ofLp 0 ^ 3 + 3 * c 1 * u.ofLp 0 ^ 2 * u.ofLp 1 + 3 * c 2 * u.ofLp 0 * u.ofLp 1 ^ 2 + c 3 * u.ofLp 1 ^ 3

theorem PlanarMidpoint.K_pairing (c : Coeff) (u v w : E) : inner ℝ (K c u v) w = cubic c u v w