Documentation

Lean 4 Proof

theorem curvature_conservation_as_holder_complement {ρ : ℝ} (hρ : ρ < 1) (hρne : ρ ≠ 0)
    (hJ : 2 ≤ J) {c w : ℝ} (hc : 0 < c) (hw : 0 < w) :
    |cesEigenvaluePerp J ρ c| * |dualEigenvaluePerp J ρ w| = 1 / (↑J * c * w) :=
  curvature_conservation hJ hρ hρne hc hw

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:633

Module Section

Economics extensions for CES formalization:

In the same file