α : Type u_2
β : Type u_1
γ : Type ?u.839059
δ : Type ?u.839062
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : Memℒp f 1
hν : Memℒp f 1
⊢ Memℒp f 1
α : Type u_2
β : Type u_1
γ : Type ?u.839059
δ : Type ?u.839062
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : Integrable f
hν : Integrable f
⊢ Integrable f
simp_rw [← memℒp_one_iff_integrable] at hμ hν⊢
α : Type u_2
β : Type u_1
γ : Type ?u.839059
δ : Type ?u.839062
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : Memℒp f 1
hν : Memℒp f 1
⊢ snorm f 1 (μ + ν) < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.839059
δ : Type ?u.839062
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : Memℒp f 1
hν : Memℒp f 1
⊢ Memℒp f 1
refine' ⟨hμ.aestronglyMeasurable.add_measure hν.aestronglyMeasurable, _⟩
α : Type u_2
β : Type u_1
γ : Type ?u.839059
δ : Type ?u.839062
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : Memℒp f 1
hν : Memℒp f 1
⊢ snorm f 1 μ < ⊤ ∧ snorm f 1 ν < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.839059
δ : Type ?u.839062
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : Memℒp f 1
hν : Memℒp f 1
⊢ snorm f 1 (μ + ν) < ⊤
rw [snorm_one_add_measure, ENNReal.add_lt_top]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.839059
δ : Type ?u.839062
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
hμ : Memℒp f 1
hν : Memℒp f 1
⊢ snorm f 1 μ < ⊤ ∧ snorm f 1 ν < ⊤
exact ⟨hμ.snorm_lt_top, hν.snorm_lt_top⟩