pith. machine review for the scientific record. sign in
def

entropyFromZ

definition
show as:
view math explainer →
module
IndisputableMonolith.Foundation.ArrowOfTime
domain
Foundation
line
91 · github
papers citing
2 papers (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.ArrowOfTime on GitHub at line 91.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  88/-- Thermodynamic entropy as coarse-grained Z:
  89    entropy = log of the number of microstates with Z ≤ current Z.
  90    This is monotone in Z, giving the second law. -/
  91noncomputable def entropyFromZ (z : ℝ) (density : ℝ) : ℝ :=
  92  Real.log (1 + z * density)
  93
  94/-- Entropy is monotone in Z (second law from Berry phase). -/
  95theorem entropy_monotone (z₁ z₂ d : ℝ) (hd : 0 < d) (hz : 0 ≤ z₁) (h : z₁ < z₂) :
  96    entropyFromZ z₁ d < entropyFromZ z₂ d := by
  97  unfold entropyFromZ
  98  apply Real.log_lt_log (by nlinarith)
  99  nlinarith
 100
 101end
 102
 103end IndisputableMonolith.Foundation.ArrowOfTime

papers checked against this theorem (showing 2 of 2)