case pos
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f

case neg
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f
by_cases hf : Integrable f μ
case pos.h
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ (r • f)) i = ↑(r • withDensityᵥ μ f) i
case pos
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f
ext1 i hi
case pos.h
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ (∫ (x : α) in i, (r • f) x ∂μ) = ∫ (a : α) in i, r • f a ∂μ
case pos.h
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ (r • f)) i = ↑(r • withDensityᵥ μ f) i
rw [withDensityᵥ_apply (hf.smul r) hi, VectorMeasure.smul_apply, withDensityᵥ_apply hf hi, ←
  integral_smul r f]
no goals
case pos.h
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ (∫ (x : α) in i, (r • f) x ∂μ) = ∫ (a : α) in i, r • f a ∂μ
rfl
case pos
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f
hr : r = 0
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f

case neg
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f
hr : ¬r = 0
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f
case neg
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f
by_cases hr : r = 0
no goals
case pos
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f
hr : r = 0
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f
rw [hr, zero_smul, zero_smul, withDensityᵥ_zero]
case neg.hnc
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f
hr : ¬r = 0
⊢ ¬Integrable (r • f)
case neg
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f
hr : ¬r = 0
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f
rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, smul_zero]
no goals
case neg.hnc
α : Type u_3
β : Type ?u.41128
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f
hr : ¬r = 0
⊢ ¬Integrable (r • f)
rwa [integrable_smul_iff hr f]