Documentation

Lean 4 Proof

theorem holder_ces_duality {ρ : ℝ} (hρ : 1 < ρ)
    {x p : Fin J → ℝ} (hx : ∀ j, 0 ≤ x j) (hp : ∀ j, 0 ≤ p j) :
    ∑ j : Fin J, x j * p j ≤
    lpNorm J ρ x * lpNorm J (dualExponent ρ) p := by
  simp only [lpNorm]
  have hx_abs : ∀ j ∈ Finset.univ, 0 ≤ x j := fun j _ => hx j
  have hp_abs : ∀ j ∈ Finset.univ, 0 ≤ p j := fun j _ => hp j
  rw [show ∑ j : Fin J, |x j| ^ ρ = ∑ j : Fin J, (x j) ^ ρ from
    Finset.sum_congr rfl (fun j _ => by rw [abs_of_nonneg (hx j)])]
  rw [show ∑ j : Fin J, |p j| ^ dualExponent ρ = ∑ j : Fin J, (p j) ^ dualExponent ρ from
    Finset.sum_congr rfl (fun j _ => by rw [abs_of_nonneg (hp j)])]
  exact inner_le_Lp_mul_Lq_of_nonneg Finset.univ (holder_conjugate_of_substitutes hρ) hx_abs hp_abs

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:610

Module Section

Economics extensions for CES formalization:

In the same file