α : Type u_2
β : Type ?u.1127420
γ : Type ?u.1127423
δ : Type ?u.1127426
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝ : NormedRing 𝕜
f✝ f g : α → 𝕜
c : ℝ
hg : Integrable g
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ ∀ᵐ (a : α) ∂μ, ‖f a * g a‖ ≤ (c • fun a => ‖g a‖) a
α : Type u_2
β : Type ?u.1127420
γ : Type ?u.1127423
δ : Type ?u.1127426
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝ : NormedRing 𝕜
f✝ f g : α → 𝕜
c : ℝ
hg : Integrable g
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ Integrable fun x => f x * g x
refine' Integrable.mono' (hg.norm.smul c) (hf.mul hg.1) _
case h
α : Type u_2
β : Type ?u.1127420
γ : Type ?u.1127423
δ : Type ?u.1127426
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝ : NormedRing 𝕜
f✝ f g : α → 𝕜
c : ℝ
hg : Integrable g
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
hx : ‖f x‖ ≤ c
⊢ ‖f x * g x‖ ≤ (c • fun a => ‖g a‖) x
α : Type u_2
β : Type ?u.1127420
γ : Type ?u.1127423
δ : Type ?u.1127426
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝ : NormedRing 𝕜
f✝ f g : α → 𝕜
c : ℝ
hg : Integrable g
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ ∀ᵐ (a : α) ∂μ, ‖f a * g a‖ ≤ (c • fun a => ‖g a‖) a
filter_upwards [hf_bound] with x hx
case h
α : Type u_2
β : Type ?u.1127420
γ : Type ?u.1127423
δ : Type ?u.1127426
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝ : NormedRing 𝕜
f✝ f g : α → 𝕜
c : ℝ
hg : Integrable g
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
hx : ‖f x‖ ≤ c
⊢ ‖f x * g x‖ ≤ c * ‖g x‖
case h
α : Type u_2
β : Type ?u.1127420
γ : Type ?u.1127423
δ : Type ?u.1127426
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝ : NormedRing 𝕜
f✝ f g : α → 𝕜
c : ℝ
hg : Integrable g
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
hx : ‖f x‖ ≤ c
⊢ ‖f x * g x‖ ≤ (c • fun a => ‖g a‖) x
rw [Pi.smul_apply, smul_eq_mul]
no goals
case h
α : Type u_2
β : Type ?u.1127420
γ : Type ?u.1127423
δ : Type ?u.1127426
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝ : NormedRing 𝕜
f✝ f g : α → 𝕜
c : ℝ
hg : Integrable g
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
hx : ‖f x‖ ≤ c
⊢ ‖f x * g x‖ ≤ c * ‖g x‖
exact (norm_mul_le _ _).trans (mul_le_mul_of_nonneg_right hx (norm_nonneg _))