Convexity #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Uniform convexity of the doubled energy on the admissible class #
The doubled mu problem minimizes a quadratic functional over an affine class
that does not depend on the coefficient. Consequently the exact
parallelogram identity
E(X) + E(Y) - 2 E((X+Y)/2) = ½ E(X - Y)
together with admissibility of the midpoint turns minimality of X into the
quantitative energy gap ½ E(X - Y) ≤ E(Y) - E(X). This is the only place
where the algebraic structure of the admissible class is used, so the two
Chapter 1 field classes are shown here to be closed under sums and scalar
multiples.
Algebra of the Chapter 1 field classes #
Zero-trace potential fields are closed under sums.
Zero-trace potential fields are closed under scalar multiples.
Zero-normal-trace solenoidal fields are closed under sums.
Zero-normal-trace solenoidal fields are closed under scalar multiples.
Midpoint admissibility #
The admissible class of the doubled mu problem is convex: the midpoint of
two admissible fields is admissible.
The exact parallelogram identity #
Parallelogram identity for the doubled quadratic form. The form is the diagonal of a symmetric bilinear pairing, so the midpoint defect is exactly a quarter of the form of the difference.
Parallelogram identity for the doubled energy density.
The averaged parallelogram identity and the energy gap #
Parallelogram identity for the doubled energy value.
Uniform convexity of the doubled energy. A minimizer beats the midpoint against any admissible competitor, so the energy gap dominates the energy of the difference.