English
Suppose μ is a sigma-finite measure on α. For motive: (α → ENNReal) → Prop, if the property holds on indicator functions of measurable sets with finite μ-measure, is stable under addition of disjoint-supported functions and under suprema of increasing sequences, then it holds for all measurable ENNReal-valued functions.
Русский
Пусть μ — сигма-ограниченная мера на α. Пусть motive : (α → ENNReal) → Prop. Если свойство верно для индикаторных функций измеримых множеств с конечной мерой μ, сохранено при суммировании функций с попарно непересекающимися поддержками и при взятии верхних пределов возрастающих последовательностей, то верность свойства распространяется на все измеримые функции α → ENNReal.
LaTeX
$$$\forall \text{motive} : (\alpha \to \mathrm{ENNReal}) \to \mathrm{Prop},\; (\text{indicator} \;\ldots) \Rightarrow (\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 with finite mass according to
some sigma-finite measure 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_sigmaFinite_induction [SigmaFinite μ] {motive : (α → ℝ≥0∞) → Prop}
(indicator : ∀ (c : ℝ≥0∞) ⦃s⦄, MeasurableSet s → μ 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
refine Measurable.ennreal_induction (fun c s hs ↦ ?_) add iSup hf
convert
iSup (f := fun n ↦ (s ∩ spanningSets μ n).indicator fun _ ↦ c)
(fun n ↦ measurable_const.indicator (hs.inter (measurableSet_spanningSets ..)))
(fun m n hmn a ↦ Set.indicator_le_indicator_of_subset (by gcongr) (by simp) _)
(fun n ↦
indicator _ (hs.inter (measurableSet_spanningSets ..))
(measure_inter_lt_top_of_right_ne_top (measure_spanningSets_lt_top ..).ne)) with
a
simp [← Set.indicator_iUnion_apply (M := ℝ≥0∞) rfl, ← Set.inter_iUnion]
