Documentation

Lean 4 Proof

theorem policy_cost_bound {W_avg DeltaF T : ℝ}
    (hT : 0 < T)
    (hJensen : Real.exp (-W_avg / T) ≤ Real.exp (-DeltaF / T)) :
    DeltaF ≤ W_avg := by
  have h := Real.exp_le_exp.mp hJensen
  -- h : -W_avg / T <= -DeltaF / T, with T > 0
  have h2 : -W_avg ≤ -DeltaF := by
    rwa [div_le_div_iff_of_pos_right hT] at h
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/PolicyCost.lean:64

Module Section

Results 26-35: Minimum Policy Cost and Multi-Scale Aggregation

In the same file