α : Type u_1
β : Type ?u.252909
E : Type u_2
F : Type ?u.252915
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑(Measure.restrict μ s) univ < ⊤
hC : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
⊢ ‖∫ (x : α) in s, f x ∂μ‖ ≤ C * ENNReal.toReal (↑↑(Measure.restrict μ s) univ)
α : Type u_1
β : Type ?u.252909
E : Type u_2
F : Type ?u.252915
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑μ s < ⊤
hC : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
⊢ ‖∫ (x : α) in s, f x ∂μ‖ ≤ C * ENNReal.toReal (↑↑μ s)
rw [← Measure.restrict_apply_univ] at *
α : Type u_1
β : Type ?u.252909
E : Type u_2
F : Type ?u.252915
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑(Measure.restrict μ s) univ < ⊤
hC : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
this : IsFiniteMeasure (Measure.restrict μ s)
⊢ ‖∫ (x : α) in s, f x ∂μ‖ ≤ C * ENNReal.toReal (↑↑(Measure.restrict μ s) univ)
α : Type u_1
β : Type ?u.252909
E : Type u_2
F : Type ?u.252915
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑(Measure.restrict μ s) univ < ⊤
hC : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
⊢ ‖∫ (x : α) in s, f x ∂μ‖ ≤ C * ENNReal.toReal (↑↑(Measure.restrict μ s) univ)
haveI : IsFiniteMeasure (μ.restrict s) := ⟨‹_›⟩
no goals
α : Type u_1
β : Type ?u.252909
E : Type u_2
F : Type ?u.252915
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
C : ℝ
hs : ↑↑(Measure.restrict μ s) univ < ⊤
hC : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ C
this : IsFiniteMeasure (Measure.restrict μ s)
⊢ ‖∫ (x : α) in s, f x ∂μ‖ ≤ C * ENNReal.toReal (↑↑(Measure.restrict μ s) univ)
exact norm_integral_le_of_norm_le_const hC