Documentation

Lean 4 Proof

theorem compact_support_q_lt_one {q T : ℝ} (hq : q < 1) (hT : 0 < T)
    {ε : ℝ} (hε : ε < -T / (1 - q)) :
    qExp q (ε / T) = 0 := by
  rw [qExp_eq_of_ne (by linarith : q ≠ 1)]
  have h1q : (0 : ℝ) < 1 - q := by linarith
  -- Show the base 1 + (1-q)·(ε/T) is negative, so max clips to 0
  have hbase : 1 + (1 - q) * (ε / T) ≤ 0 := by
    -- Key: ε < -T/(1-q) implies (1-q)*ε + T < 0 implies 1 + (1-q)*(ε/T) < 0
    suffices h : T + (1 - q) * ε < 0 by
      have : T * (1 + (1 - q) * (ε / T)) = T + (1 - q) * ε := by
        field_simp
      nlinarith [mul_pos hT (show 0 < -( 1 + (1 - q) * (ε / T)) from by nlinarith)]
    -- From ε < -T/(1-q): multiply by (1-q) > 0
    have : ε * (1 - q) < -T := by
      calc ε * (1 - q) < (-T / (1 - q)) * (1 - q) :=
            mul_lt_mul_of_pos_right hε h1q
        _ = -T := by field_simp
    linarith
  rw [max_eq_left hbase]
  exact zero_rpow (by positivity)

Dependency Graph

Location

thesis/CESProofs/Potential/QEquilibrium.lean:72

Module Section

Propositions 3-4: q-Exponential Equilibrium and Tail Behavior

In the same file