English
A tautology about ENNReal comparisons used in the induction; 0 < top is true.
Русский
Тавтология: 0 < верхняя граница истинна.
LaTeX
$$$$0 < \\top.$$$$
Lean4
/-- To prove something for an arbitrary integrable function in a normed group,
it suffices to show that
* the property holds for (multiples of) characteristic functions;
* is closed under addition;
* the set of functions in the `L¹` space for which the property holds is closed.
* the property is closed under the almost-everywhere equal relation.
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 induction (P : (α → E) → Prop) (h_ind : ∀ (c : E) ⦃s⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun _ => c))
(h_add :
∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Integrable f μ → Integrable g μ → P f → P g → P (f + g))
(h_closed : IsClosed {f : α →₁[μ] E | P f}) (h_ae : ∀ ⦃f g⦄, f =ᵐ[μ] g → Integrable f μ → P f → P g) :
∀ ⦃f : α → E⦄, Integrable f μ → P f :=
by
simp only [← memLp_one_iff_integrable] at *
exact MemLp.induction one_ne_top (motive := P) h_ind h_add h_closed h_ae
