English
Induction principle for simple functions: to prove P(f) for all simple functions f, it suffices to prove P for constants and to show closure under piecewise composition on measurable sets.
Русский
Индукционный принцип для простых функций: чтобы доказать P(f) для всех простых функций, достаточно доказать P(константы) и замкнутость при кусочно-определении на измеримых множествах.
LaTeX
$$$\\text{induction'} \\; {\\alpha, \\gamma} \\; [MeasurableSpace \\alpha] [Nonempty \\gamma] \\ {P: SimpleFunc\\alpha \\gamma \\to Prop} \\; (\\forall (c), P(\\text{const }\\alpha c)) \\; \\land \\\\ (\\forall f,g : SimpleFunc \\alpha\\gamma) (s: Set\\alpha) (hs: MeasurableSet s), P f \\to P g \\to P (f.piecewise s hs g) \\Rightarrow \\forall f, P f.$$$
Lean4
/-- To prove something for an arbitrary simple function, it suffices to show
that the property holds for constant functions and that it is closed under piecewise combinations
of functions.
To use in an induction proof, the syntax is `induction f with`. -/
@[induction_eliminator]
protected theorem induction' {α γ} [MeasurableSpace α] [Nonempty γ] {P : SimpleFunc α γ → Prop}
(const : ∀ (c), P (SimpleFunc.const _ c))
(pcw : ∀ ⦃f g : SimpleFunc α γ⦄ {s} (hs : MeasurableSet s), P f → P g → P (f.piecewise s hs g))
(f : SimpleFunc α γ) : P f := by
let c : γ := Classical.ofNonempty
classical
generalize h : f.range \ { c } = 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 c
ext x
simp [h]
| insert x s hxs ih =>
have mx := f.measurableSet_preimage { x }
let g := SimpleFunc.piecewise (f ⁻¹' { x }) mx (SimpleFunc.const α c) f
have Pg : P 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 pcw mx.compl Pg (const x)
· ext1 y
by_cases hy : y ∈ f ⁻¹' { x }
· simpa [g, hy]
· simp [g, hy]
