α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤ → (∫⁻ (a : α), ↑‖(c • f) a‖₊ ∂μ) < ⊤
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
⊢ HasFiniteIntegral f → HasFiniteIntegral (c • f)
simp only [HasFiniteIntegral]
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
⊢ (∫⁻ (a : α), ↑‖(c • f) a‖₊ ∂μ) < ⊤
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤ → (∫⁻ (a : α), ↑‖(c • f) a‖₊ ∂μ) < ⊤
intro hfi
no goals
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
⊢ (∫⁻ (a : α), ↑‖(c • f) a‖₊ ∂μ) < ⊤
calc
  (∫⁻ a : α, ‖c • f a‖₊ ∂μ) ≤ ∫⁻ a : α, ‖c‖₊ * ‖f a‖₊ ∂μ := by
    refine' lintegral_mono _
    intro i
    exact_mod_cast (nnnorm_smul_le c (f i))
  _ < ∞ := by
    rw [lintegral_const_mul']
    exacts [mul_lt_top coe_ne_top hfi.ne, coe_ne_top]
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
⊢ (fun a => ↑‖c • f a‖₊) ≤ fun a => ↑‖c‖₊ * ↑‖f a‖₊
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
⊢ (∫⁻ (a : α), ↑‖c • f a‖₊ ∂μ) ≤ ∫⁻ (a : α), ↑‖c‖₊ * ↑‖f a‖₊ ∂μ
refine' lintegral_mono _
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
i : α
⊢ (fun a => ↑‖c • f a‖₊) i ≤ (fun a => ↑‖c‖₊ * ↑‖f a‖₊) i
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
⊢ (fun a => ↑‖c • f a‖₊) ≤ fun a => ↑‖c‖₊ * ↑‖f a‖₊
intro i
no goals
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
i : α
⊢ (fun a => ↑‖c • f a‖₊) i ≤ (fun a => ↑‖c‖₊ * ↑‖f a‖₊) i
exact_mod_cast (nnnorm_smul_le c (f i))
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
⊢ (↑‖c‖₊ * ∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤

case hr
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
⊢ ↑‖c‖₊ ≠ ⊤
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
⊢ (∫⁻ (a : α), ↑‖c‖₊ * ↑‖f a‖₊ ∂μ) < ⊤
rw [lintegral_const_mul']
no goals
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
⊢ (↑‖c‖₊ * ∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤

case hr
α : Type u_3
β : Type u_2
γ : Type ?u.775481
δ : Type ?u.775484
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : MeasurableSpace δ
inst✝⁴ : NormedAddCommGroup β
inst✝³ : NormedAddCommGroup γ
𝕜 : Type u_1
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
f : α → β
hfi : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
⊢ ↑‖c‖₊ ≠ ⊤
exacts [mul_lt_top coe_ne_top hfi.ne, coe_ne_top]