Anisotropic quadratic maps over normed fields are coercive

Let Q be a continuous anisotropic quadratic map on a proper normed space V over a nontrivially normed field. Then Q is bounded below by a multiple of the squared norm: there is c > 0 with c * ‖x‖ ^ 2 ≤ ‖Q x‖ for every x. The constant is the minimum of ‖Q‖ on a compact shell ‖k‖⁻¹ ≤ ‖x‖ ≤ 1, where ‖k‖ > 1, into which every nonzero vector rescales. A shell is used rather than the unit sphere because over a general nontrivially normed field (for instance a nonarchimedean one) a nonzero vector need not have a scalar multiple of norm exactly 1, whereas rescale_to_shell always rescales it into the shell.

Consequently the sublevel sets {x | ‖Q x‖ ≤ r} of Q are compact. In particular, for an anisotropic quadratic form on a finite-dimensional space over a locally compact nontrivially normed field such as ℝ or ℚ_p, every sublevel set is compact for the module topology. This is the input that makes the orthogonal group of an anisotropic form compact: an isometry carries each vector into a level set of Q.

Main results

• QuadraticMap.Anisotropic.exists_pos_mul_norm_sq_le: an anisotropic quadratic map on a proper normed space is bounded below by a positive multiple of the squared norm.
• QuadraticMap.Anisotropic.isCompact_setOf_norm_apply_le_of_continuous: the sublevel sets of the norm of a continuous anisotropic quadratic map on a proper normed space are compact.
• QuadraticMap.Anisotropic.isCompact_setOf_norm_apply_le: the sublevel sets of the norm of an anisotropic quadratic form on a finite-dimensional space over a locally compact field are compact.

theorem QuadraticMap.Anisotropic.exists_pos_mul_norm_sq_le {K : Type u_1} {V : Type u_2} {N : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup V] [NormedSpace K V] [ProperSpace V] [NormedAddCommGroup N] [NormedSpace K N] {Q : QuadraticMap K V N} (hQ : Q.Anisotropic) (hcont : Continuous ⇑Q) : ∃ c > 0, ∀ (x : V), c * ‖x‖ ^ 2 ≤ ‖Q x‖

Anisotropic quadratic maps are coercive. A continuous anisotropic quadratic map on a proper normed space over a nontrivially normed field is bounded below by a positive multiple of the squared norm.

theorem QuadraticMap.Anisotropic.isCompact_setOf_norm_apply_le_of_continuous {K : Type u_1} {V : Type u_2} {N : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup V] [NormedSpace K V] [ProperSpace V] [NormedAddCommGroup N] [NormedSpace K N] {Q : QuadraticMap K V N} (hQ : Q.Anisotropic) (hcont : Continuous ⇑Q) (r : ℝ) : IsCompact {x : V | ‖Q x‖ ≤ r}

The sublevel sets {x | ‖Q x‖ ≤ r} of a continuous anisotropic quadratic map on a proper normed space over a nontrivially normed field are compact.

theorem QuadraticMap.Anisotropic.isCompact_setOf_norm_apply_le {K : Type u_1} {V : Type u_2} [NontriviallyNormedField K] [WeaklyLocallyCompactSpace K] [Invertible 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [TopologicalSpace V] [IsModuleTopology K V] {Q : QuadraticForm K V} (hQ : Anisotropic Q) (r : ℝ) : IsCompact {x : V | ‖Q x‖ ≤ r}

The sublevel sets {x | ‖Q x‖ ≤ r} of an anisotropic quadratic form on a finite-dimensional space over a locally compact nontrivially normed field, such as ℝ or ℚ_p, are compact for the module topology.