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{StronglyMeasurable } f \land \text{Measurable } g \Rightarrow \text{Measurable } (x \mapsto f(x) + g(x))$$$
Lean4
/-- In a normed vector space, the addition of a strongly measurable function and a 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.stronglyMeasurable_add {α 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 (f + g) :=
by
rcases hf with ⟨φ, hφ⟩
have : Tendsto (fun n x ↦ φ n x + g x) atTop (𝓝 (f + g)) := tendsto_pi_nhds.2 (fun x ↦ (hφ x).add tendsto_const_nhds)
apply measurable_of_tendsto_metrizable (fun n ↦ ?_) this
exact hg.simpleFunc_add _
