Lean 4 Proof

theorem optimalPolicyTimescale_pos {DeltaF T ell netBudget : ℝ}
    (hDF : 0 < DeltaF) (hT : 0 < T) (hell : 0 < ell) (hB : 0 < netBudget) :
    0 < optimalPolicyTimescale DeltaF T ell netBudget := by
  simp only [optimalPolicyTimescale]
  exact div_pos (mul_pos hDF hT) (mul_pos hell hB)

Dependency Graph

Location

thesis/CESProofs/Dynamics/PolicyCost.lean:141

Module Section

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

In the same file