def definition def or abbrev

`remainingEntropy`

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

formal statement (Lean)

  57noncomputable def remainingEntropy (bh : EvolvingBlackHole) : ℝ :=

Definition body.

  58  bh.S_initial * (1 - bh.evaporation_fraction)
  59
  60/-- The entropy carried away by radiation (naive, before Page time). -/

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

Lean names referenced from this declaration's body.

entropy in IndisputableMonolith.Foundation.InitialCondition decl_use
before in IndisputableMonolith.Foundation.TimeEmergence decl_use
EvolvingBlackHole in IndisputableMonolith.Quantum.PageCurve decl_use
entropy in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
entropy in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use