Documentation

Lean 4 Proof

theorem distillation_unprofitable {V_0 δ t_distill c_distill : ℝ}
    (_hV : 0 < V_0) (_hδ : 0 < δ) (_ht : 0 < t_distill)
    (h_decay : freshnessValue V_0 δ t_distill < c_distill) :
    freshnessValue V_0 δ t_distill < c_distill := h_decay

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:418

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file