Friction Work Non-negative

theorem proved Dynamics & Crises

Documentation

Lean 4 Proof

theorem friction_work_nonneg {W_avg DeltaF : ℝ}
    (hbound : DeltaF ≤ W_avg) :
    0 ≤ W_avg - DeltaF := by
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/PolicyCost.lean:88

Module Section

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

In the same file

jarzynski_equality policy_cost_bound friction_work_estimate optimalPolicyTimescale optimalPolicyTimescale_pos aggregation_rhoT aggregation_invariant_classes macroscopic_predictability irrelevance_test policy_cost_scales_with_T