Documentation

Lean 4 Proof

theorem holder_conjugate_of_substitutes {ρ : ℝ} (hρ : 1 < ρ) :
    ρ.HolderConjugate (dualExponent ρ) := by
  rw [dualExponent_eq_conjExponent]
  exact Real.HolderConjugate.conjExponent hρ

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:599

Module Section

Economics extensions for CES formalization:

In the same file