def definition def or abbrev

`evolve`

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

formal statement (Lean)

 145def evolve {peq : ProbabilityDistribution Ω}
 146    (R : JDescentOperator peq) :
 147    ℕ → ProbabilityDistribution Ω → ProbabilityDistribution Ω
 148  | 0,     q => q
 149  | n + 1, q => R.step (R.evolve n q)
 150
 151omit [Nonempty Ω] in

used by (25)

From the project-wide theorem graph. These declarations reference this one in their body.

voxelStep in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
LedgerComputation in IndisputableMonolith.Complexity.ComputationBridge decl_use
main_resolution in IndisputableMonolith.Complexity.ComputationBridge decl_use
Turing_incomplete in IndisputableMonolith.Complexity.ComputationBridge decl_use
VorticityVoxel in IndisputableMonolith.Flight.Medium decl_use
eight_tick_dissipation_limit in IndisputableMonolith.Information.Thermodynamics decl_use
RecognitionOperator in IndisputableMonolith.Information.Thermodynamics decl_use
J_stasis_nonneg in IndisputableMonolith.Modal.Possibility decl_use
zenoAntiZenoCrossover in IndisputableMonolith.Quantum.ZenoEffect decl_use
information_conserved in IndisputableMonolith.Relativity.InformationConservation decl_use
entropy_increase_under_conservation in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
evolve_equilibrium_eq in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
evolve_succ in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
evolve_zero in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
free_energy_antitone in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
free_energy_ge_equilibrium in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
free_energy_le_of_le in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
free_energy_step_le in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
kl_divergence_antitone in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
kl_le_of_le in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
kl_step_le in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
second_law in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
SecondLawCert in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
second_law_entropy_form in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
second_law_one_statement in IndisputableMonolith.Thermodynamics.SecondLaw decl_use

depends on (3)

Lean names referenced from this declaration's body.

step in IndisputableMonolith.Complexity.CellularAutomata decl_use
ProbabilityDistribution in IndisputableMonolith.Thermodynamics.RecognitionThermodynamics decl_use
JDescentOperator in IndisputableMonolith.Thermodynamics.SecondLaw decl_use