Documentation

Lean 4 Proof

theorem policy_cost_scales_with_T {DeltaPhi T₁ T₂ DeltaS_q : ℝ}
    (hS : 0 < DeltaS_q) (h12 : T₁ < T₂) :
    DeltaPhi - T₂ * DeltaS_q < DeltaPhi - T₁ * DeltaS_q :=
  barrier_decreases_with_T hS h12

Dependency Graph

Location

thesis/CESProofs/Dynamics/PolicyCost.lean:250

Module Section

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

In the same file