Documentation

Lean 4 Proof

theorem hasDerivAt_perCapitaBenefit {J ρ c : ℝ} (hJ : 0 < J) :
    HasDerivAt (fun x => perCapitaBenefit x ρ c)
      ((1 / ρ - 1) * J ^ (1 / ρ - 2) * c) J := by
  simp only [perCapitaBenefit]
  have hrpow : HasDerivAt (fun x => x ^ (1 / ρ - 1 : ℝ))
      (1 * (1 / ρ - 1) * J ^ ((1 / ρ - 1) - 1)) J :=
    (hasDerivAt_id J).rpow_const (p := 1 / ρ - 1) (Or.inl (ne_of_gt hJ))
  convert hrpow.mul_const c using 1; ring_nf

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Calculus.lean:50

Module Section

Paper 1c: Formal Calculus on K(J) and V(J)

In the same file