English
There is an outer measure μ on the real line associated to a Stieltjes function f, defined by μ(E) = OuterMeasure.ofFunction(f.length, f.length_empty)(E).
Русский
Существует внешняя мера μ на ℝ, связанная с функцией Стилетджеса f, определяемая как μ(E) = OuterMeasure.ofFunction(f.length, f.length_empty)(E).
LaTeX
$$f.outer = \mathrm{OuterMeasure.ofFunction}(f.length, f.length\_empty)$$
Lean4
/-- The Stieltjes outer measure associated to a Stieltjes function. -/
protected def outer : OuterMeasure ℝ :=
OuterMeasure.ofFunction f.length f.length_empty