Documentation

Lean 4 Proof

theorem cesInner_nonneg {α ρ K L : ℝ} (hα : 0 < α) (hα1 : α < 1)
    (hK : 0 < K) (hL : 0 < L) :
    0 ≤ cesInner α ρ K L :=
  le_of_lt (cesInner_pos hα hα1 hK hL)

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:86

Module Section

Two-Factor CES Production Function (Layer 1 of Macro Extension)

In the same file