case inl
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
hα : IsEmpty α
⊢ Integrable fun x => f x * g x

case inr
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
hα : Nonempty α
⊢ Integrable fun x => f x * g x
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
⊢ Integrable fun x => f x * g x
cases' isEmpty_or_nonempty α with hα hα
case inl
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
hα : IsEmpty α
⊢ Integrable fun x => f x * g x
case inl
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
hα : IsEmpty α
⊢ Integrable fun x => f x * g x
rw [μ.eq_zero_of_isEmpty]
no goals
case inl
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
hα : IsEmpty α
⊢ Integrable fun x => f x * g x
exact integrable_zero_measure
case inr
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
hα : Nonempty α
⊢ HasFiniteIntegral fun x => f x * g x
case inr
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
hα : Nonempty α
⊢ Integrable fun x => f x * g x
refine' ⟨hm.mul hint.1, _⟩
case inr.intro
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
⊢ HasFiniteIntegral fun x => f x * g x
case inr
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
hα : Nonempty α
⊢ HasFiniteIntegral fun x => f x * g x
obtain ⟨C, hC⟩ := hfbdd
case inr.intro
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
⊢ HasFiniteIntegral fun x => f x * g x
case inr.intro
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
⊢ HasFiniteIntegral fun x => f x * g x
have hCnonneg : 0 ≤ C := le_trans (norm_nonneg _) (hC hα.some)
case inr.intro
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
⊢ HasFiniteIntegral fun x => f x * g x
case inr.intro
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
⊢ HasFiniteIntegral fun x => f x * g x
have : (fun x => ‖f x * g x‖₊) ≤ fun x => ⟨C, hCnonneg⟩ * ‖g x‖₊ := by
  intro x
  simp only [nnnorm_mul]
  exact mul_le_mul_of_nonneg_right (hC x) (zero_le _)
case inr.intro
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
⊢ (∫⁻ (a : α), ↑({ val := C, property := hCnonneg } * ‖g a‖₊) ∂μ) < ⊤
case inr.intro
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
⊢ HasFiniteIntegral fun x => f x * g x
refine' lt_of_le_of_lt (lintegral_mono_nnreal this) _
case inr.intro
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
⊢ (∫⁻ (a : α), ↑{ val := C, property := hCnonneg } * ↑‖g a‖₊ ∂μ) < ⊤
case inr.intro
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
⊢ (∫⁻ (a : α), ↑({ val := C, property := hCnonneg } * ‖g a‖₊) ∂μ) < ⊤
simp only [ENNReal.coe_mul]
case inr.intro
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
⊢ (↑{ val := C, property := hCnonneg } * ∫⁻ (a : α), ↑‖g a‖₊ ∂μ) < ⊤
case inr.intro
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
⊢ (∫⁻ (a : α), ↑{ val := C, property := hCnonneg } * ↑‖g a‖₊ ∂μ) < ⊤
rw [lintegral_const_mul' _ _ ENNReal.coe_ne_top]
no goals
case inr.intro
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
this : (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
⊢ (↑{ val := C, property := hCnonneg } * ∫⁻ (a : α), ↑‖g a‖₊ ∂μ) < ⊤
exact ENNReal.mul_lt_top ENNReal.coe_ne_top (ne_of_lt hint.2)
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
x : α
⊢ (fun x => ‖f x * g x‖₊) x ≤ (fun x => { val := C, property := hCnonneg } * ‖g x‖₊) x
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
⊢ (fun x => ‖f x * g x‖₊) ≤ fun x => { val := C, property := hCnonneg } * ‖g x‖₊
intro x
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
x : α
⊢ ‖f x‖₊ * ‖g x‖₊ ≤ { val := C, property := hCnonneg } * ‖g x‖₊
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
x : α
⊢ (fun x => ‖f x * g x‖₊) x ≤ (fun x => { val := C, property := hCnonneg } * ‖g x‖₊) x
simp only [nnnorm_mul]
no goals
α : Type u_2
β : Type ?u.955935
γ : Type ?u.955938
δ : Type ?u.955941
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
F : Type u_1
inst✝ : NormedDivisionRing F
f g : α → F
hint : Integrable g
hm : AEStronglyMeasurable f μ
hα : Nonempty α
C : ℝ
hC : ∀ (x : α), ‖f x‖ ≤ C
hCnonneg : 0 ≤ C
x : α
⊢ ‖f x‖₊ * ‖g x‖₊ ≤ { val := C, property := hCnonneg } * ‖g x‖₊
exact mul_le_mul_of_nonneg_right (hC x) (zero_le _)