Documentation

Lean 4 Proof

theorem generalKeff_zero_friction
    {J : ℕ} {ρ : ℝ} {a : Fin J → ℝ} {Tstar : ℝ} (_hTs : 0 < Tstar) :
    generalEffectiveCurvatureKeff J ρ a 0 Tstar
    = generalCurvatureK J ρ a := by
  unfold generalEffectiveCurvatureKeff
  simp [zero_div, sub_zero, mul_one]

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:354

Module Section

## General-Weight Effective Curvature Theorems

In the same file