Documentation

Lean 4 Proof

def geodesicDistSq (J : ℕ) (x y : Fin J → ℝ) : ℝ :=
  ∑ j : Fin J, ((x j / ∑ i, x i) - (y j / ∑ i, y i)) ^ 2

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/Superadditivity.lean:25

Module Section

Superadditivity of CES (Paper 1, Section 6):

In the same file