Documentation

Lean 4 Proof

noncomputable def irsEffectiveCurvaturePerp
    (J : ℕ) (ρ γ c : ℝ) (T Tstar_base : ℝ) : ℝ :=
  irsEigenvaluePerp J ρ γ c * max 0 (1 - T / (Tstar_base * γ))

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:260

Module Section

## General-Weight and IRS Effective Curvature Definitions

In the same file