Documentation

Lean 4 Proof

theorem two_level_ces_curvature (w K : Fin N -> ℝ) (Ktilde VarRho : ℝ) :
    totalCurvature w K Ktilde VarRho =
    withinCurvature w K + betweenCurvature Ktilde VarRho := by
  rfl

Dependency Graph

Location

thesis/CESProofs/Dynamics/Closure.lean:68

Module Section

Results 80-85: Rho-Diversity Selection and Closure

In the same file