A double cone depends only on the line spanned by its axis

Proved

QFS.doubleCone_neg

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

analysismeasure-theoryquadratic-forms-sobolev

Let $E$ be a real inner product space, let $v \in E$ and let $\vartheta \in \mathbb{R}$ . Writing $V(v, \vartheta)$ for the double cone with axis $v$ and aperture $\vartheta$ , one has

V(-v, \vartheta) \;=\; V(v, \vartheta).

Reversing the axis does not change the double cone: membership in $V(v,\vartheta)$ is a condition on the angle between the line spanned by the point and the line spanned by $v$ , and that line is unchanged when $v$ is replaced by $-v$ . This is the formal reason a double cone is an invariant of a line rather than of a direction, which in turn is why the reduction to finitely many reference cones works with a covering of projective space — antipodal pairs of directions — rather than of the sphere.

Formalization Note. The statement is completely unconditional: no positivity or upper bound is imposed on $\vartheta$ , $v$ need not be a unit vector, and the ambient space is an arbitrary real inner product space. In particular it also holds in the degenerate cases $v = 0$ and $\vartheta \notin [0, \pi]$ .

Preamble

-- Generated by skeleton subtraction from QuadraticFormsSobolev/ConeGap.lean
-- source: quadratic-forms-sobolev@7a1a680db212
/-
The signed distance to the boundary of a cone.

For a unit axis `v` and apex angle `ϑ`, write `a = ⟪v,p⟫` and `b = ‖p − a·v‖` for
the components of `p` along and across the axis. Then

  `coneGap v ϑ p = a sin ϑ − b cos ϑ`

is positive exactly on the cone `Ṽ(v, ϑ)`, is `1`-Lipschitz in `p`, and is
positively homogeneous. Consequently a ball of radius `ρ < coneGap v ϑ p` about
`p` lies inside the cone — the quantitative fact used throughout Sections 4 and
5, of which `mem_cone_of_norm_sub_lt` is the special case `p = t·v`.
-/
import Definitions.Def_QFS_Translate
import Definitions.Def_QFS_Defs
import Definitions.Def_QFS_ConeGap
import Mathlib

set_option autoImplicit true
set_option relaxedAutoImplicit false
set_option maxSynthPendingDepth 3

open Real Set Metric
open RealInnerProductSpace

open QFS

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

/-! ## The gap as a distance

`coneGap v ϑ h = ‖h‖ sin(ϑ − ∠(v,h))`, which is the exact distance from `h` to the
boundary of the cone. This makes the constants in Section 5.2 computable. -/

Formal statement

lemma QFS.doubleCone_neg (v : E) (ϑ : ℝ) : doubleCone (-v) ϑ = doubleCone v ϑ := by sorry

Source

https://github.com/dbenbenn/quadratic-forms-sobolev/blob/7a1a680db2124d46ce370c91fd450aa454edf491/QuadraticFormsSobolev/ConeGap.lean#L263-L267

View graph