English
To prove a property for every Lp.simpleFunc E p μ (with 0 < p < ∞), it suffices to prove it for indicatorConst on finite-measure sets and to show it is preserved under addition of disjoint-support simple functions.
Русский
Чтобы доказать свойство для любой Lp.simpleFunc, достаточно доказать его для indicatorConst на множествах конечной меры и показать сохранение под сложение функций с непересекающимися поддержками.
LaTeX
$$$ \\text{induction}_{lp}(hp\\_pos, hp\\_ne\\_top) = \\text{(indicatorConst)} , \\text{(add)} \\Rightarrow \\forall f, P(f) $$$
Lean4
/-- To prove something for an arbitrary `Lp` simple function, with `0 < p < ∞`, it suffices to show
that the property holds for (multiples of) characteristic functions of finite-measure measurable
sets and is closed under addition (of functions with disjoint support). -/
@[elab_as_elim]
protected theorem induction (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ∞) {P : Lp.simpleFunc E p μ → Prop}
(indicatorConst :
∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (Lp.simpleFunc.indicatorConst p hs hμs.ne c))
(add :
∀ ⦃f g : α →ₛ E⦄,
∀ hf : MemLp f p μ,
∀ hg : MemLp g p μ,
Disjoint (support f) (support g) →
P (Lp.simpleFunc.toLp f hf) →
P (Lp.simpleFunc.toLp g hg) → P (Lp.simpleFunc.toLp f hf + Lp.simpleFunc.toLp g hg))
(f : Lp.simpleFunc E p μ) : P f :=
by
suffices ∀ f : α →ₛ E, ∀ hf : MemLp f p μ, P (toLp f hf)
by
rw [← toLp_toSimpleFunc f]
apply this
clear f
apply SimpleFunc.induction
· intro c s hs hf
by_cases hc : c = 0
· convert indicatorConst 0 MeasurableSet.empty (by simp) using 1
ext1
simp [hc]
exact indicatorConst c hs (SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs hf)
· intro f g hfg hf hg hfg'
obtain ⟨hf', hg'⟩ : MemLp f p μ ∧ MemLp g p μ :=
(memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable).mp hfg'
exact add hf' hg' hfg (hf hf') (hg hg')
