Optimal Policy Speed

def proved Dynamics & Crises

Documentation

Lean 4 Proof

def optimalPolicyTimescale (DeltaF T ell netBudget : ℝ) : ℝ :=
  DeltaF * T / (ell * netBudget)

Dependency Graph

Used by

optimalPolicyTimescale_pos

Location

thesis/CESProofs/Dynamics/PolicyCost.lean:138

Module Section

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

In the same file

jarzynski_equality policy_cost_bound friction_work_nonneg friction_work_estimate optimalPolicyTimescale_pos aggregation_rhoT aggregation_invariant_classes macroscopic_predictability irrelevance_test policy_cost_scales_with_T