English
If f and g are Finite Strongly Measurable, then their sum and their infimum are Finite Strongly Measurable.
Русский
Если f и g финитно сильно измеримы, то их сумма и infimum также финитно сильно измеримы.
LaTeX
$$$\text{FinStronglyMeasurable}(f) \land \text{FinStronglyMeasurable}(g) \Rightarrow \text{FinStronglyMeasurable}(f+g) \land \text{FinStronglyMeasurable}(\min\{f,g\})$$$
Lean4
@[aesop safe 20 (rule_sets := [Measurable])]
protected theorem add [AddZeroClass β] [ContinuousAdd β] (hf : FinStronglyMeasurable f μ)
(hg : FinStronglyMeasurable g μ) : FinStronglyMeasurable (f + g) μ :=
⟨fun n => hf.approx n + hg.approx n, fun n =>
(measure_mono (Function.support_add _ _)).trans_lt
((measure_union_le _ _).trans_lt (ENNReal.add_lt_top.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩)),
fun x => (hf.tendsto_approx x).add (hg.tendsto_approx x)⟩
