naming convention

Stream: mathlib4

[Jon Eugster]

in PR #20682, there are the following helper lemmas which both proof a special case of a (real) integral where the lower bound is 0. What would be good names?

The snippet ..._from_zero_... is completely invented by me, and I'm not confident that it's understandable. The latter uses a ₀-suffix currently, which might also not be standard either

lemma integral_log_from_zero_of_pos
    {b : ℝ} (ht : 0 < b) :
    ∫ (s : ℝ) in (0)..b, log s = b * log b - b := sorry

lemma intervalIntegrable_of_even₀
    (h₁f : ∀ x, f x = f (-x))
    (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) (t : ℝ) :
    IntervalIntegrable f volume 0 t := sorry

[Jon Eugster]

for comparison, the main statements are:

theorem integral_log :
    ∫ (s : ℝ) in a..b, log s = b * log b - a * log a - b + a := sorry

theorem intervalIntegrable_of_even
    (h₁f : ∀ x, f x = f (-x))
    (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) (x y : ℝ) :
    IntervalIntegrable f volume x y := sorry

and integral_log_of_pos is the name of a statement which gets deprecated in this PR as superflous assumptions are removed.