English
If g is an embedding, then f is strongly measurable iff g∘f is strongly measurable.
Русский
Если g — вложение, то f сильно измерима тогда и только тогда, когда g∘f сильно измерима.
LaTeX
$$$\text{IsEmbedding}(g) \Rightarrow (\mathrm{StronglyMeasurable}(g\circ f) \iff \mathrm{StronglyMeasurable}(f))$$$
Lean4
/-- To prove that a property holds for any strongly measurable function, it is enough to show
that it holds for constant functions and that it is closed under piecewise combination of functions
and pointwise limits.
To use in an induction proof, the syntax is
`induction f, hf using StronglyMeasurable.induction' with`. -/
theorem induction' [MeasurableSpace α] [Nonempty β] [TopologicalSpace β] {P : (f : α → β) → StronglyMeasurable f → Prop}
(const : ∀ (c), P (fun _ ↦ c) stronglyMeasurable_const)
(pcw :
∀ ⦃f g : α → β⦄ {s} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
P f hf → P g hg → P (s.piecewise f g) (hf.piecewise hs hg))
(lim :
∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ n, StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
(∀ n, P (f n) (hf n)) → (∀ x, Tendsto (f · x) atTop (𝓝 (g x))) → P g hg)
(f : α → β) (hf : StronglyMeasurable f) : P f hf :=
by
let s := hf.approx
refine lim (fun n ↦ (s n).stronglyMeasurable) hf (fun n ↦ ?_) hf.tendsto_approx
change P (s n) (s n).stronglyMeasurable
induction s n with
| const c => exact const c
| @pcw f g s hs Pf Pg =>
simp_rw [SimpleFunc.coe_piecewise]
exact pcw f.stronglyMeasurable g.stronglyMeasurable hs Pf Pg
