English
An induction principle for simple functions: to prove a property P for all simple functions, it suffices to prove P for constants and show closure under piecewise construction on measurable sets and disjoint supports, and then extend to sums.
Русский
Принцип индукции для простых функций: чтобы доказать свойство P для всех простых функций, достаточно доказать P для констант и показать замкнутость по разбиениям на куски на измеримых множествах и по суммам с непересекающимися опорами.
LaTeX
$$$\text{induction'}\;: \forall P, (\forall c, P(\text{const } c)) \to (\forall f,g, \text{Disjoint}(\operatorname{support} f, \operatorname{support} g) \to P f \to P g
\to P (f+g)) \to \forall f, P(f)$$$
Lean4
/-- To prove something for an arbitrary simple function, it suffices to show
that the property holds for (multiples of) characteristic functions and is closed under
addition (of functions with disjoint support).
It is possible to make the hypotheses in `h_add` a bit stronger, and such conditions can be added
once we need them (for example it is only necessary to consider the case where `g` is a multiple
of a characteristic function, and that this multiple doesn't appear in the image of `f`).
To use in an induction proof, the syntax is `induction f using SimpleFunc.induction with`. -/
@[elab_as_elim]
protected theorem induction {α γ} [MeasurableSpace α] [AddZeroClass γ] {motive : SimpleFunc α γ → Prop}
(const :
∀ (c) {s} (hs : MeasurableSet s),
motive (SimpleFunc.piecewise s hs (SimpleFunc.const _ c) (SimpleFunc.const _ 0)))
(add : ∀ ⦃f g : SimpleFunc α γ⦄, Disjoint (support f) (support g) → motive f → motive g → motive (f + g))
(f : SimpleFunc α γ) : motive f := by
classical
generalize h : f.range \ {0} = s
rw [← Finset.coe_inj, Finset.coe_sdiff, Finset.coe_singleton, SimpleFunc.coe_range] at h
induction s using Finset.induction generalizing f with
| empty =>
rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h
convert const 0 MeasurableSet.univ
ext x
simp [h]
| insert x s hxs ih =>
have mx := f.measurableSet_preimage { x }
let g := SimpleFunc.piecewise (f ⁻¹' { x }) mx 0 f
have Pg : motive g := by
apply ih
simp only [g, SimpleFunc.coe_piecewise, range_piecewise]
rw [image_compl_preimage, union_diff_distrib, diff_diff_comm, h, Finset.coe_insert, insert_diff_self_of_notMem,
diff_eq_empty.mpr, Set.empty_union]
· rw [Set.image_subset_iff]
convert Set.subset_univ _
exact preimage_const_of_mem (mem_singleton _)
· rwa [Finset.mem_coe]
convert add _ Pg (const x mx)
· ext1 y
by_cases hy : y ∈ f ⁻¹' { x }
· simpa [g, hy]
· simp [g, hy]
rw [disjoint_iff_inf_le]
rintro y
by_cases hy : y ∈ f ⁻¹' { x } <;> simp [g, hy]
