Documentation

Lean 4 Proof

theorem factorShare_slope_is_rho {α ρ K₁ K₂ L : ℝ}
    (hα : 0 < α) (hα1 : α < 1) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hL : 0 < L)
    (_hK : K₁ ≠ K₂) :
    -- The difference in log share ratios equals ρ times the difference
    -- in log factor ratios (exact, not approximate):
    Real.log (laborShare α ρ K₂ L / capitalShare α ρ K₂ L) -
    Real.log (laborShare α ρ K₁ L / capitalShare α ρ K₁ L) =
    ρ * (Real.log (L / K₂) - Real.log (L / K₁)) := by
  rw [factorShare_identity hα hα1 hK₂ hL,
      factorShare_identity hα hα1 hK₁ hL]
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:353

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file