Essential supremum and infimum #
We define the essential supremum and infimum of a function
f : α → β with respect to a measure
α. The essential supremum is the infimum of the constants
c : β such that
f x ≤ c
TODO: The essential supremum of functions
α → ℝ≥0∞ is used in particular to define the norm in
L∞ space (see measure_theory/lp_space.lean).
There is a different quantity which is sometimes also called essential supremum: the least
upper-bound among measurable functions of a family of measurable functions (in an almost-everywhere
sense). We do not define that quantity here, which is simply the supremum of a map with values in
α →ₘ[μ] β (see measure_theory/ae_eq_fun.lean).