English
Let 1 ≤ p and p ≠ ∞. If a property P holds for characteristic functions scaled by constants, is closed under addition for disjoint supports, and the set of Lp-functions with property P is closed, then P holds for every Lp-function.
Русский
Пусть 1 ≤ p и p ≠ ∞. Если свойство P выполняется для ограничителей вида c·1_s, сохраняется при сложении на непересекающихся участках и множество функций в Lp, удовлетворяющих P, замкнуто, то P выполняется для любой функции из Lp.
LaTeX
$$$$\\forall f\\in L^p(E,p,\\\\mu), P(f)$$ при предпосылках: (i) $P(c\\,\\mathbf{1}_s)$ для измеримых $s$ с конечной measure, (ii) $P$ сохраняется под сложением по непересекающимся поддержкам, (iii) множество таких функций замкнутое.$$
Lean4
/-- To prove something for an arbitrary `Lp` function in a second countable Borel normed group, it
suffices to show that
* the property holds for (multiples of) characteristic functions;
* is closed under addition;
* the set of functions in `Lp` for which the property holds is closed.
-/
@[elab_as_elim]
theorem induction [_i : Fact (1 ≤ p)] (hp_ne_top : p ≠ ∞) (motive : Lp E p μ → Prop)
(indicatorConst :
∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), motive (Lp.simpleFunc.indicatorConst p hs hμs.ne c))
(add :
∀ ⦃f g⦄,
∀ hf : MemLp f p μ,
∀ hg : MemLp g p μ,
Disjoint (support f) (support g) → motive (hf.toLp f) → motive (hg.toLp g) → motive (hf.toLp f + hg.toLp g))
(isClosed : IsClosed {f : Lp E p μ | motive f}) : ∀ f : Lp E p μ, motive f :=
by
refine fun f => (Lp.simpleFunc.denseRange hp_ne_top).induction_on f isClosed ?_
refine Lp.simpleFunc.induction (α := α) (E := E) (lt_of_lt_of_le zero_lt_one _i.elim).ne' hp_ne_top ?_ ?_
· exact fun c s => indicatorConst c
· exact fun f g hf hg => add hf hg
