noncomputable def ERealFunction.boltzmannEntropy : ℝ → ↑(Set.Ioi ⊥)

The ]-∞,+∞]-valued extension of x ↦ x \log x - x that equals 0 at 0 and +∞ on the negative half-line.

@[simp]

theorem ERealFunction.boltzmannEntropy_apply_of_pos {x : ℝ} (hx : 0 < x) : ↑(boltzmannEntropy x) = ↑(x * Real.log x - x)

On (0,+∞), boltzmannEntropy is given by the real formula x \log x - x.

@[simp]

theorem ERealFunction.boltzmannEntropy_apply_zero : ↑(boltzmannEntropy 0) = 0

At 0, boltzmannEntropy takes the value 0.

@[simp]

theorem ERealFunction.boltzmannEntropy_apply_of_neg {x : ℝ} (hx : x < 0) : ↑(boltzmannEntropy x) = ⊤

On (-∞,0), boltzmannEntropy takes the value +∞.

theorem ERealFunction.effectiveDomain_boltzmannEntropy : effectiveDomain boltzmannEntropy = Set.Ici 0

The effective domain of boltzmannEntropy is the closed half-line [0,+∞).

theorem ERealFunction.boltzmannEntropy_isProper : IsProper fun (x : ℝ) => ↑(boltzmannEntropy x)

boltzmannEntropy is proper as an extended-real-valued function.

theorem ERealFunction.boltzmannEntropy_lowerSemicontinuous : LowerSemicontinuous fun (x : ℝ) => ↑(boltzmannEntropy x)

The extended-real-valued representative of boltzmannEntropy is lower semicontinuous on ℝ.

theorem ERealFunction.boltzmannEntropy_strictlyConvex : StrictlyConvex boltzmannEntropy

boltzmannEntropy is strictly convex on its effective domain [0,+∞).

theorem ERealFunction.boltzmannEntropy_mem_gammaZero : boltzmannEntropy ∈ Γ₀(ℝ)

Example 9.35: the function equal to x \log x - x on (0,+∞), equal to 0 at 0, and equal to +∞ on (-∞,0) belongs to Γ₀(ℝ); equivalently, it is proper, lower semicontinuous, and strictly convex on its effective domain [0,+∞).