module module

`IndisputableMonolith.Thermodynamics.SecondLaw`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Thermodynamics.MaxEntFromCost module_import
IndisputableMonolith.Thermodynamics.RecognitionThermodynamics module_import

declarations in this module (22)

def gibbsPD L110
lemma gibbsPD_p L116
structure JDescentOperator L132
def evolve L145
lemma evolve_zero L152
lemma evolve_succ L157
theorem evolve_equilibrium_eq L163
theorem kl_step_le L177
theorem kl_le_of_le L186
theorem kl_divergence_antitone L199
lemma fe_kl_id L207
theorem free_energy_step_le L216
theorem free_energy_le_of_le L231
theorem free_energy_antitone L245
theorem free_energy_ge_equilibrium L253
theorem second_law L273
theorem second_law_one_statement L300
theorem second_law_entropy_form L334
theorem entropy_increase_under_conservation L355
structure SecondLawCert L374
def secondLawCert L406
theorem secondLawCert_inhabited L422