-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.bdd_mul {F : Type*} [NormedDivisionRing F] {f g : α → F} (hint : Integrable g μ)
    (hm : AEStronglyMeasurable f μ) (hfbdd : ∃ C, ∀ x, ‖f x‖ ≤ C) :
    Integrable (fun x => f x * g x) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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 => ⟨C, hCnonneg⟩ * ‖g x‖₊) x

Tactic:
simp only [nnnorm_mul]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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‖₊ ≤ ⟨C, hCnonneg⟩ * ‖g x‖₊

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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) μ

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Result:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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) μ

Proof state:
case inr.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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) μ

Tactic:
have hCnonneg : 0 ≤ C := le_trans (norm_nonneg _) (hC hα.some)

Result:
case inr.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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) μ

Proof state:
case inr.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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 => ⟨C, hCnonneg⟩ * ‖g x‖₊
⊢ ∫⁻ (a : α), ↑(⟨C, hCnonneg⟩ * ‖g a‖₊) ∂μ < ⊤

Tactic:
simp only [ENNReal.coe_mul]

Result:
case inr.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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 => ⟨C, hCnonneg⟩ * ‖g x‖₊
⊢ ∫⁻ (a : α), ↑⟨C, hCnonneg⟩ * ↑‖g a‖₊ ∂μ < ⊤

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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) μ

Tactic:
obtain ⟨C, hC⟩ := hfbdd

Result:
case inr.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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) μ

Proof state:
case inr.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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) μ

Tactic:
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 _)

Result:
case inr.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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 => ⟨C, hCnonneg⟩ * ‖g x‖₊
⊢ HasFiniteIntegral (fun x => f x * g x) μ

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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) μ

Tactic:
refine ⟨hm.mul hint.1, ?_⟩

Result:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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‖₊ ≤ ⟨C, hCnonneg⟩ * ‖g x‖₊

Tactic:
exact mul_le_mul_of_nonneg_right (hC x) (zero_le _)

Result:
no goals

Proof state:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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) 0

Tactic:
exact integrable_zero_measure

Result:
no goals

Proof state:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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) μ

Tactic:
rw [μ.eq_zero_of_isEmpty]

Result:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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) 0

Proof state:
case inr.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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 => ⟨C, hCnonneg⟩ * ‖g x‖₊
⊢ HasFiniteIntegral (fun x => f x * g x) μ

Tactic:
refine lt_of_le_of_lt (lintegral_mono_nnreal this) ?_

Result:
case inr.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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 => ⟨C, hCnonneg⟩ * ‖g x‖₊
⊢ ∫⁻ (a : α), ↑(⟨C, hCnonneg⟩ * ‖g a‖₊) ∂μ < ⊤

Proof state:
case inr.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : Type u_6
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 => ⟨C, hCnonneg⟩ * ‖g x‖₊
⊢ ↑⟨C, hCnonneg⟩ * ∫⁻ (a : α), ↑‖g a‖₊ ∂μ < ⊤

Tactic:
exact ENNReal.mul_lt_top ENNReal.coe_lt_top hint.2

Result:
no goals