Documentation

Lean 4 Proof

theorem freshness_decay_positive {V_0 δ t : ℝ}
    (hV : 0 < V_0) : 0 < freshnessValue V_0 δ t :=
  mul_pos hV (exp_pos _)

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:409

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file