Explicit operator bounds for the planar cubic tensor.

theorem PlanarMidpoint.norm_le_abs_coordinates (u : E) : ‖u‖ ≤ |u.ofLp 0| + |u.ofLp 1|

The Euclidean norm is bounded by the sum of absolute coordinates.

theorem PlanarMidpoint.norm_K_le (c : Coeff) (u v : E) : ‖K c u v‖ ≤ 8 * ‖c‖ * ‖u‖ * ‖v‖

A uniform trilinear bound; the constant is deliberately coarse.

theorem PlanarMidpoint.K_diagonal_sub (c d : Coeff) (v w : E) : K c v v - K d w w = K (c - d) v v + K d (v - w) v + K d w (v - w)

Difference decomposition retaining the quadratic velocity structure.

theorem PlanarMidpoint.norm_K_diagonal_sub_le (c d : Coeff) (v w : E) : ‖K c v v - K d w w‖ ≤ 8 * ‖c - d‖ * ‖v‖ ^ 2 + 8 * ‖d‖ * (‖v‖ + ‖w‖) * ‖v - w‖

The Christoffel force is locally Lipschitz in coefficients and velocity.