Documentation

Lean 4 Proof

noncomputable def irsFirmProfit
    (K_eff γ T : ℝ) (g h : ℝ) : ℝ :=
  K_eff * g * γ - T * h

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:287

Module Section

## General-Weight and IRS Effective Curvature Definitions

In the same file