Samplinglib mathematical lesson

Angular geometry on the actual unit sphere

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product space with its Borel measurable structure, and let S be its literal unit-norm subtype. The actual angular cost c(u,v)=arccos(inner(u,v)) is jointly continuous and measurable on S×S. For every pair it lies between zero and pi, equals Mathlib's unoriented vector angle, dominates the ambient chord norm, vanishes exactly on the diagonal, and is symmetric. It satisfies the triangle inequality. These are explicit properties of the angular cost; no inherited chord-distance instance is replaced, no path-length geodesic-distance identification or Wasserstein theorem is included, and no sphere nonemptiness or positive dimension is assumed.

\[c(u,v)=\arccos\langle u,v\rangle,\quad 0\le c\le\pi,\quad \|u-v\|\le c(u,v),\quad c(u,w)\le c(u,v)+c(v,w).\]

Lean statement · unit_sphere_angular_cost_properties

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem unit_sphere_angular_cost_properties
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] :
    let S := {w : E // ‖w‖ = 1}
    let c : S × S → ℝ := fun z => Real.arccos ⟪z.1.1,z.2.1⟫_ℝ
    Continuous c ∧ Measurable c ∧
      (∀ u v : S, 0 ≤ c (u,v) ∧ c (u,v) ≤ Real.pi ∧
        c (u,v) = InnerProductGeometry.angle u.1 v.1 ∧
        ‖u.1-v.1‖ ≤ c (u,v) ∧
        (c (u,v) = 0 ↔ u = v) ∧ c (u,v) = c (v,u)) ∧
      ∀ u v w : S, c (u,w) ≤ c (u,v)+c (v,w)

Exact module and namespace context

Read the complete mathematical statement and visible assumptions, then expand the numbered formula proof. Exact Lean remains optional and initially folded.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product normed space with its Borel measurable structure.
S is exactly the unit-norm subtype and c(u,v)=arccos(inner(u,v)). Neither positive dimension nor a point of S is assumed.

Mathematical proof

Open a step to read its argument and formula.

1. Identify the angle

Unit norms cancel the denominator in the vector-angle definition, so the literal arccos cost is the existing unoriented angle. Continuity follows from continuous subtype coercions, the inner product and arccos; finite dimension supplies second countability for the measurable product.

\[c(u,v)=\operatorname{angle}(u,v),\qquad c\in C(S\times S;\mathbb R).\]

Corresponding Lean step

  have heq (u v : {w : E // ‖w‖ = 1}) :
      Real.arccos ⟪u.1,v.1⟫_ℝ = InnerProductGeometry.angle u.1 v.1 := by
    simp [InnerProductGeometry.angle,u.property,v.property]
  have hc : Continuous (fun z : {w : E // ‖w‖ = 1} × {w : E // ‖w‖ = 1} =>
      Real.arccos ⟪z.1.1,z.2.1⟫_ℝ) := by fun_prop

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

2. Compare a chord with its angle

Set θ=c(u,v)=angle(u,v). For unit endpoints, expand the squared chord norm. The half-angle identity and sin squared bounded by its argument squared yield the chord estimate; both norms and the angle are nonnegative.

\[\|u-v\|^2=2-2\cos\theta=4\sin^2(\theta/2)\le\theta^2.\]

Corresponding Lean step

private theorem chord_le_angle
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (u v : E) (hu : ‖u‖ = 1) (hv : ‖v‖ = 1) :
    ‖u-v‖ ≤ InnerProductGeometry.angle u v := by
  let θ := InnerProductGeometry.angle u v
  have hθ : 0 ≤ θ := InnerProductGeometry.angle_nonneg u v
  have hc : Real.cos θ = ⟪u,v⟫_ℝ := by
    simpa [θ,hu,hv] using InnerProductGeometry.cos_angle u v
  have heq : ‖u-v‖^2 = 2-2*Real.cos θ := by
    rw [norm_sub_sq_real,hu,hv,hc]
    ring
  have hh := Real.sin_sq_eq_half_sub (θ/2)
  have htwo : 2*(θ/2) = θ := by ring
  rw [htwo] at hh
  have hs := Real.sin_sq_le_sq (x := θ/2)
  change ‖u-v‖ ≤ θ
  nlinarith [norm_nonneg (u-v)]

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

3. Separate points and record the range

The principal arccos lies in [0,pi]. A zero cost forces zero chord, hence equal subtype points. Conversely every unit vector is nonzero and has zero angle with itself. Inner-product symmetry supplies cost symmetry.

\[0\le c(u,v)\le\pi,\quad c(u,v)=0\iff u=v,\quad c(u,v)=c(v,u).\]

Corresponding Lean step

    refine ⟨Real.arccos_nonneg _,Real.arccos_le_pi _,heq u v,hchord,?_,?_⟩
    · constructor
      · intro hz
        apply Subtype.ext
        apply sub_eq_zero.mp
        apply norm_eq_zero.mp
        exact le_antisymm (by simpa only [hz] using hchord) (norm_nonneg _)
      · rintro rfl
        rw [heq]
        apply InnerProductGeometry.angle_self
        intro hz
        have hh := u.property
        rw [hz,norm_zero] at hh
        norm_num at hh
    · rw [heq,heq,InnerProductGeometry.angle_comm]

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

4. Use the vector-angle triangle inequality

Replace each literal cost by its angle expression and apply the existing vector-angle triangle inequality. This is an angular-cost fact; it does not identify an intrinsic path-length metric, particularly on the disconnected two-point sphere.

\[c(u,w)=\operatorname{angle}(u,w)\le\operatorname{angle}(u,v)+\operatorname{angle}(v,w).\]

Corresponding Lean step

  · intro u v w
    rw [heq,heq,heq]
    exact InnerProductGeometry.angle_le_angle_add_angle u.1 v.1 w.1

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

Lean verification

Lean proof · unit_sphere_angular_cost_properties

The formula steps explain the proof; optional folds contain literal Lean excerpts and the full checked theorem.

Download module (.lean)

theorem unit_sphere_angular_cost_properties
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] :
    let S := {w : E // ‖w‖ = 1}
    let c : S × S → ℝ := fun z => Real.arccos ⟪z.1.1,z.2.1⟫_ℝ
    Continuous c ∧ Measurable c ∧
      (∀ u v : S, 0 ≤ c (u,v) ∧ c (u,v) ≤ Real.pi ∧
        c (u,v) = InnerProductGeometry.angle u.1 v.1 ∧
        ‖u.1-v.1‖ ≤ c (u,v) ∧
        (c (u,v) = 0 ↔ u = v) ∧ c (u,v) = c (v,u)) ∧
      ∀ u v w : S, c (u,w) ≤ c (u,v)+c (v,w) := by
  dsimp only
  letI : SecondCountableTopology E := inferInstance
  have heq (u v : {w : E // ‖w‖ = 1}) :
      Real.arccos ⟪u.1,v.1⟫_ℝ = InnerProductGeometry.angle u.1 v.1 := by
    simp [InnerProductGeometry.angle,u.property,v.property]
  have hc : Continuous (fun z : {w : E // ‖w‖ = 1} × {w : E // ‖w‖ = 1} =>
      Real.arccos ⟪z.1.1,z.2.1⟫_ℝ) := by fun_prop
  refine ⟨hc,hc.measurable,?_,?_⟩
  · intro u v
    have hchord : ‖u.1-v.1‖ ≤ Real.arccos ⟪u.1,v.1⟫_ℝ := by
      rw [heq]
      exact chord_le_angle u.1 v.1 u.property v.property
    refine ⟨Real.arccos_nonneg _,Real.arccos_le_pi _,heq u v,hchord,?_,?_⟩
    · constructor
      · intro hz
        apply Subtype.ext
        apply sub_eq_zero.mp
        apply norm_eq_zero.mp
        exact le_antisymm (by simpa only [hz] using hchord) (norm_nonneg _)
      · rintro rfl
        rw [heq]
        apply InnerProductGeometry.angle_self
        intro hz
        have hh := u.property
        rw [hz,norm_zero] at hh
        norm_num at hh
    · rw [heq,heq,InnerProductGeometry.angle_comm]
  · intro u v w
    rw [heq,heq,heq]
    exact InnerProductGeometry.angle_le_angle_add_angle u.1 v.1 w.1

end AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphereAngularCost

Exact module and namespace context

Scope and omitted-condition boundaries

Explicit cost properties only. The inherited subtype distance is still the ambient chord distance; no metric instance is changed.
No intrinsic path-length identity, installed manifold API, Wasserstein theorem or statistical model is certified. In dimension one the two-point sphere has finite angular cost but no internal path between its two points.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

InnerProductGeometry.angle_le_angle_add_angle
InnerProductGeometry.cos_angle
Real.sin_sq_eq_half_sub
Real.sin_sq_le_sq

Mathematical sources

Samplinglib original sphere geometry and feature-law supplement v1 (2026-10-23) (historical source) — Original generic canonical-library mathematics placed by subject; no primary-textbook theorem, concrete statistical model or whole chapter credit.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.