ContinuousLinearMap.distribution_le

lemma _root_.ContinuousLinearMap.distribution_le {f : α → E₁} {g : α → E₂} (L : E₁ →L[𝕜] E₂ →L[𝕜] E₃) :    distribution (fun x ↦ L (f x) (g x)) (‖L‖ₑ * t * s) μ ≤    distribution f t μ + distribution g s μ := by  have h₀ : {x | ‖L‖ₑ * t * s < ‖(fun x ↦ (L (f x)) (g x)) x‖ₑ} ⊆      {x | t < ‖f x‖ₑ} ∪ {x | s < ‖g x‖ₑ} := fun z hz ↦ by    simp only [mem_union, mem_setOf_eq] at hz ⊢    contrapose! hz    calc      ‖(L (f z)) (g z)‖ₑ ≤ ‖L‖ₑ * ‖f z‖ₑ * ‖g z‖ₑ := by calc          _ ≤ ‖L (f z)‖ₑ * ‖g z‖ₑ := ContinuousLinearMap.le_opENorm (L (f z)) (g z)          _ ≤ ‖L‖ₑ * ‖f z‖ₑ * ‖g z‖ₑ :=            mul_le_mul' (ContinuousLinearMap.le_opENorm L (f z)) (by rfl)      _ ≤ _ := mul_le_mul' (mul_le_mul_right hz.1 ‖L‖ₑ) hz.2  calc    _ ≤ μ ({x | t < ‖f x‖ₑ} ∪ {x | s < ‖g x‖ₑ}) := measure_mono h₀    _ ≤ _ := measure_union_le _ _