Documentation

Lean 4 Proof

theorem integration_boundary {K_eff T c₀ : ℝ} (_hK : 0 < K_eff) (_hc : 0 < c₀)
    (hT : 0 < T) :
    -- Integration profitable iff K_eff > c₀ · T
    K_eff > c₀ * T ↔ K_eff / T > c₀ := by
  rw [gt_iff_lt, gt_iff_lt, lt_div_iff₀ hT]

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:75

Module Section

Propositions 12-17 and Corollary 5:

In the same file