English
Let motive be a property of functions α → ENNReal. If the property holds for every constant multiple of characteristic functions of measurable sets, and is closed under (i) addition of disjoint-supported functions and (ii) supremum of increasing sequences of measurable functions, then the property holds for all measurable functions f : α → ENNReal.
Русский
Пусть motive — свойство функций α → ENNReal. Если это свойство выполняется для всех кратных характеристических функций измеримых множеств и сохраняется под сложением дизъюнктно поддерживаемых функций и верхними пределами возрастающих последовательностей измеримых функций, то свойство верно и для любых измеримых функций f: α → ENNReal.
LaTeX
$$$\forall \text{motive} : (\alpha \to \mathrm{ENNReal}) \to \mathrm{Prop},\; (\text{indicator} \;\ldots) \;\to\; (\forall f,g,\; Disjoint(\mathrm{support}\,f)(\mathrm{support}\,g) \to \text{Measurable} f \to \text{Measurable} g \to \text{motive} f \to \text{motive} g \to \text{motive}(f+g)) \to (\forall f: \alpha \to \mathrm{ENNReal}, \text{Measurable} f \to \text{motive} f)$$$
Lean4
/-- To prove something for an arbitrary measurable function into `ℝ≥0∞`, it suffices to show
that the property holds for (multiples of) characteristic functions and is closed under addition
and supremum of increasing sequences of functions.
It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions
can be added once we need them (for example in `h_add` it is only necessary to consider the sum of
a simple function with a multiple of a characteristic function and that the intersection
of their images is a subset of `{0}`. -/
@[elab_as_elim]
theorem ennreal_induction {motive : (α → ℝ≥0∞) → Prop}
(indicator : ∀ (c : ℝ≥0∞) ⦃s⦄, MeasurableSet s → motive (Set.indicator s fun _ => c))
(add :
∀ ⦃f g : α → ℝ≥0∞⦄,
Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g))
(iSup :
∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ n, Measurable (f n)) → Monotone f → (∀ n, motive (f n)) → motive fun x => ⨆ n, f n x)
⦃f : α → ℝ≥0∞⦄ (hf : Measurable f) : motive f :=
by
convert iSup (fun n => (eapprox f n).measurable) (monotone_eapprox f) _ using 2
· rw [iSup_eapprox_apply hf]
·
exact fun n =>
SimpleFunc.induction (fun c s hs => indicator c hs) (fun f g hfg hf hg => add hfg f.measurable g.measurable hf hg)
(eapprox f n)
