Documentation

Lean 4 Proof

theorem welfareDistanceFn_eq_zero_iff {z : ℝ} (hz : 0 < z) :
    welfareDistanceFn z = 0 ↔ z = 1 := by
  constructor
  · intro h
    simp only [welfareDistanceFn] at h
    -- h : z - 1 - log z = 0, so log z = z - 1
    have hlog : Real.log z = z - 1 := by linarith
    -- From 1 + x ≤ exp x with x = log z:
    -- 1 + log z ≤ exp(log z) = z
    -- So 1 + (z - 1) ≤ z, i.e. z ≤ z (trivially true)
    -- But we also need the reverse. Use exp(x) ≥ 1 + x with x = z - 1:
    -- exp(z - 1) ≥ 1 + (z - 1) = z
    -- And exp(log z) = z, so exp(z - 1) ≥ exp(log z)
    -- Since exp is strictly monotone: z - 1 ≥ log z
    -- Combined with log z = z - 1: equality in 1+x ≤ exp x at x = log z
    -- Equality in exp x ≥ 1 + x holds iff x = 0
    -- Use the strict version: exp x > 1 + x for x ≠ 0
    by_contra hne
    have hne1 : z - 1 ≠ 0 := sub_ne_zero.mpr hne
    have hstrict := Real.add_one_lt_exp hne1
    -- 1 + (z - 1) < exp(z - 1), i.e., z < exp(z - 1)
    -- But hlog says log z = z - 1, so exp(z - 1) = exp(log z) = z
    rw [← hlog, Real.exp_log hz] at hstrict
    linarith
  · intro h
    rw [h]
    exact welfareDistanceFn_at_one

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/Defs.lean:144

Module Section

Core definitions for the Lean formalization of Paper 4:

In the same file