English
For product spaces, a continuous function with compact support is strongly measurable in the product sigma-algebra.
Русский
На произведении пространств непрерывная функция с компактной поддержкой — сильно измерима в произведенной сигма-алгебре.
LaTeX
$$$\text{Continuous}(f) \land \text{HasCompactSupport}(f) \Rightarrow \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 indicator functions of measurable sets and that it is closed under
addition and pointwise limit.
To use in an induction proof, the syntax is
`induction f, hf using StronglyMeasurable.induction with`. -/
theorem induction [MeasurableSpace α] [AddZeroClass β] [TopologicalSpace β]
{P : (f : α → β) → StronglyMeasurable f → Prop}
(ind : ∀ c ⦃s : Set α⦄ (hs : MeasurableSet s), P (s.indicator fun _ ↦ c) (stronglyMeasurable_const.indicator hs))
(add :
∀ ⦃f g : α → β⦄ (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hfg : StronglyMeasurable (f + g)),
Disjoint f.support g.support → P f hf → P g hg → P (f + g) hfg)
(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 using SimpleFunc.induction with
| const c hs => exact ind c hs
| @add f g h_supp hf hg => exact add f.stronglyMeasurable g.stronglyMeasurable (f + g).stronglyMeasurable h_supp hf hg
