MeasureTheory.distribution_add_le_of_enorm

lemma distribution_add_le_of_enorm {A : ℝ≥0∞}    (h : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ A * (‖g₁ x‖ₑ + ‖g₂ x‖ₑ)) :    distribution f (A * (t + s)) μ ≤ distribution g₁ t μ + distribution g₂ s μ := by  unfold distribution  have h₁ : μ ({x | A * (t + s) < ‖f x‖ₑ} \      ({x | t < ‖g₁ x‖ₑ} ∪ {x | s < ‖g₂ x‖ₑ})) = 0 := by    apply measure_mono_null ?_ h    intro x    simpa using fun h₁ h₂ h₃ ↦ lt_of_le_of_lt (by gcongr) h₁  calc    μ {x | A * (t + s) < ‖f x‖ₑ}      ≤ μ ({x | t < ‖g₁ x‖ₑ} ∪ {x | s < ‖g₂ x‖ₑ}) := measure_mono_ae' h₁    _ ≤ μ {x | t < ‖g₁ x‖ₑ} + μ {x | s < ‖g₂ x‖ₑ} := measure_union_le _ _