Documentation

Lean 4 Proof

theorem total_exceeds_within (w K : Fin N -> ℝ) {Ktilde VarRho : ℝ}
    (hK : 0 < Ktilde) (hV : 0 < VarRho) :
    withinCurvature w K < totalCurvature w K Ktilde VarRho := by
  simp only [totalCurvature]
  linarith [between_curvature_pos hK hV]

Dependency Graph

Location

thesis/CESProofs/Dynamics/Closure.lean:82

Module Section

Results 80-85: Rho-Diversity Selection and Closure

In the same file