α : Type u_2
β : Type ?u.1111558
γ : Type ?u.1111561
δ : Type ?u.1111564
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ AEStronglyMeasurable f μ → ((∫⁻ (a : α), ↑‖f a‖₊ * ↑‖c‖₊ ∂μ) < ⊤ ↔ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤)
α : Type u_2
β : Type ?u.1111558
γ : Type ?u.1111561
δ : Type ?u.1111564
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ (Integrable fun x => f x • c) ↔ Integrable f
simp_rw [Integrable, aestronglyMeasurable_smul_const_iff (f := f) hc, and_congr_right_iff,
  HasFiniteIntegral, nnnorm_smul, ENNReal.coe_mul]
α : Type u_2
β : Type ?u.1111558
γ : Type ?u.1111561
δ : Type ?u.1111564
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ↑‖f a‖₊ * ↑‖c‖₊ ∂μ) < ⊤ ↔ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
α : Type u_2
β : Type ?u.1111558
γ : Type ?u.1111561
δ : Type ?u.1111564
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ AEStronglyMeasurable f μ → ((∫⁻ (a : α), ↑‖f a‖₊ * ↑‖c‖₊ ∂μ) < ⊤ ↔ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤)
intro _
α : Type u_2
β : Type ?u.1111558
γ : Type ?u.1111561
δ : Type ?u.1111564
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤ ∧ ↑‖c‖₊ < ⊤ ∨ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) = 0 ∨ ↑‖c‖₊ = 0 ↔ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
α : Type u_2
β : Type ?u.1111558
γ : Type ?u.1111561
δ : Type ?u.1111564
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ↑‖f a‖₊ * ↑‖c‖₊ ∂μ) < ⊤ ↔ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
rw [lintegral_mul_const' _ _ ENNReal.coe_ne_top, ENNReal.mul_lt_top_iff]
α : Type u_2
β : Type ?u.1111558
γ : Type ?u.1111561
δ : Type ?u.1111564
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
this : ∀ (x : ℝ≥0∞), x = 0 → x < ⊤
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤ ∧ ↑‖c‖₊ < ⊤ ∨ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) = 0 ∨ ↑‖c‖₊ = 0 ↔ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
α : Type u_2
β : Type ?u.1111558
γ : Type ?u.1111561
δ : Type ?u.1111564
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤ ∧ ↑‖c‖₊ < ⊤ ∨ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) = 0 ∨ ↑‖c‖₊ = 0 ↔ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
have : ∀ x : ℝ≥0∞, x = 0 → x < ∞ := by simp
no goals
α : Type u_2
β : Type ?u.1111558
γ : Type ?u.1111561
δ : Type ?u.1111564
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
this : ∀ (x : ℝ≥0∞), x = 0 → x < ⊤
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤ ∧ ↑‖c‖₊ < ⊤ ∨ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) = 0 ∨ ↑‖c‖₊ = 0 ↔ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
simp [hc, or_iff_left_of_imp (this _)]
no goals
α : Type u_2
β : Type ?u.1111558
γ : Type ?u.1111561
δ : Type ?u.1111564
m : MeasurableSpace α
μ ν : Measure α
inst✝⁶ : MeasurableSpace δ
inst✝⁵ : NormedAddCommGroup β
inst✝⁴ : NormedAddCommGroup γ
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
⊢ ∀ (x : ℝ≥0∞), x = 0 → x < ⊤
simp