Documentation

Lean 4 Proof

theorem powerMean_mono_curvature {ρ₁ ρ₂ : ℝ} (_hρ₁ : 0 < ρ₁) (_hρ₂ : 0 < ρ₂)
    (hle : ρ₁ ≤ ρ₂) (hJ : 2 ≤ J) :
    curvatureK J ρ₂ ≤ curvatureK J ρ₁ := by
  simp only [curvatureK]
  have hJpos : (0 : ℝ) < ↑J := by exact_mod_cast (by omega : 0 < J)
  apply div_le_div_of_nonneg_right _ (le_of_lt hJpos)
  apply mul_le_mul_of_nonneg_right (by linarith)
  have : (1 : ℝ) ≤ ↑J := by exact_mod_cast (by omega : 1 ≤ J)
  linarith

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:487

Module Section

Economics extensions for CES formalization:

In the same file