Non-negativity of the angle between two lines

Proved

QFS.dangle_nonneg

by dbenbenn · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysismeasure-theoryquadratic-forms-sobolev

Let $E$ be a real inner product space. For vectors $v, h \in E$ let $\angle_{\mathrm{line}}(v, h)$ denote the angle between the lines spanned by $v$ and by $h$ — the quantity written dangle v h, which is the angle between $v$ and $h$ read modulo replacing either vector by its negative, so that it is unchanged when $v$ or $h$ is reflected through the origin. It is the quantity for which membership $h \in V(v, \vartheta)$ in a double cone with axis $v$ and aperture $\vartheta$ says exactly $\angle_{\mathrm{line}}(v, h) < \vartheta$ . Then, for all $v, h \in E$ ,

0 \le \angle_{\mathrm{line}}(v, h).

Non-negativity is one of the two elementary facts making $\angle_{\mathrm{line}}$ behave like a distance on the space of lines; it is used, together with the triangle inequality for this quantity, when a covering of the unit sphere by small angular caps is converted into an inclusion between double cones.

Formalization Note. The statement carries no hypothesis whatsoever: $v$ and $h$ are arbitrary vectors of an arbitrary real inner product space, in particular they need not be unit vectors and either may be zero. In the degenerate cases the value is whatever the underlying angle convention returns, and the lemma asserts only that this value is never negative.

Preamble

-- Generated by skeleton subtraction from QuadraticFormsSobolev/RefCones.lean
-- source: quadratic-forms-sobolev@7a1a680db212
/-
Lemma 2.2, Definition 2.3 and Corollary 2.4 of Bux–Kassmann–Schulze: the
reduction of an arbitrary `ϑ`-bounded configuration to a finite family of
reference cones.
-/
import Definitions.Def_QFS_Translate
import Definitions.Def_QFS_Defs
import Definitions.Def_QFS_RefCones
import Mathlib

set_option autoImplicit true
set_option relaxedAutoImplicit false
set_option maxSynthPendingDepth 3

open Real Set Metric InnerProductGeometry

open QFS

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

/-! ## The angle between two lines

A double cone `V(v, ϑ)` is determined by the *line* spanned by `v`, and
membership `h ∈ V(v, ϑ)` says exactly that the line spanned by `h` makes an
angle less than `ϑ` with the line spanned by `v`. That quantity obeys a triangle
inequality, which is what the proof of Lemma 2.2 uses when it passes from a
covering of the sphere to an inclusion of cones. -/

Formal statement

lemma QFS.dangle_nonneg (v h : E) : 0 ≤ dangle v h := by sorry

Source

https://github.com/dbenbenn/quadratic-forms-sobolev/blob/7a1a680db2124d46ce370c91fd450aa454edf491/QuadraticFormsSobolev/RefCones.lean#L28-L29

View graph