English
The sum of a strongly measurable function and a measurable function is measurable.
Русский
Сумма сильно измеримой и измеримой функций является измеримой.
LaTeX
$$$\forall g:\alpha \to E, \forall f:\alpha \to E, \text{Measurable } g \land \text{StronglyMeasurable } f \Rightarrow \text{Measurable } (x \mapsto g(x) + f(x))$$$
Lean4
/-- In a normed vector space, the addition of a measurable function and a strongly measurable
function is measurable. Note that this is not true without further second-countability assumptions
for the addition of two measurable functions. -/
theorem _root_.Measurable.add_stronglyMeasurable {α E : Type*} {_ : MeasurableSpace α} [AddCancelMonoid E]
[TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] [ContinuousAdd E] [PseudoMetrizableSpace E] {g f : α → E}
(hg : Measurable g) (hf : StronglyMeasurable f) : Measurable (g + f) :=
by
rcases hf with ⟨φ, hφ⟩
have : Tendsto (fun n x ↦ g x + φ n x) atTop (𝓝 (g + f)) := tendsto_pi_nhds.2 (fun x ↦ tendsto_const_nhds.add (hφ x))
apply measurable_of_tendsto_metrizable (fun n ↦ ?_) this
exact hg.add_simpleFunc _
