Continuity of quadratic forms in finite dimension

The polar form of an arbitrary quadratic form on a finite-dimensional real normed space is jointly continuous, hence so is the quadratic form itself. These statements have no wall, lattice, or stability hypotheses.

theorem QuadraticMap.continuous_polar {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) : Continuous fun (p : M × M) => polar (⇑Q) p.1 p.2

The polar form is jointly continuous on a finite-dimensional real normed space.

theorem QuadraticMap.continuous_of_finiteDimensional {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) : Continuous ⇑Q

A quadratic form on a finite-dimensional real normed space is continuous: it is half the diagonal of its polar form.