case pos
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f
⊢ withDensityᵥ μ f = withDensityᵥ μ g

case neg
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f
⊢ withDensityᵥ μ f = withDensityᵥ μ g
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
⊢ withDensityᵥ μ f = withDensityᵥ μ g
by_cases hf : Integrable f μ
case pos.h
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f
i : Set α
⊢ MeasurableSet i → ↑(withDensityᵥ μ f) i = ↑(withDensityᵥ μ g) i
case pos
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f
⊢ withDensityᵥ μ f = withDensityᵥ μ g
ext i
case pos.h
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ f) i = ↑(withDensityᵥ μ g) i
case pos.h
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f
i : Set α
⊢ MeasurableSet i → ↑(withDensityᵥ μ f) i = ↑(withDensityᵥ μ g) i
intro hi
case pos.h
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ (∫ (x : α) in i, f x ∂μ) = ∫ (x : α) in i, g x ∂μ
case pos.h
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ f) i = ↑(withDensityᵥ μ g) i
rw [withDensityᵥ_apply hf hi, withDensityᵥ_apply (hf.congr h) hi]
no goals
case pos.h
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ (∫ (x : α) in i, f x ∂μ) = ∫ (x : α) in i, g x ∂μ
exact integral_congr_ae (ae_restrict_of_ae h)
case neg
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f
hg : ¬Integrable g
⊢ withDensityᵥ μ f = withDensityᵥ μ g
case neg
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f
⊢ withDensityᵥ μ f = withDensityᵥ μ g
have hg : ¬Integrable g μ := by intro hg; exact hf (hg.congr h.symm)
no goals
case neg
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f
hg : ¬Integrable g
⊢ withDensityᵥ μ f = withDensityᵥ μ g
rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg hg]
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f
hg : Integrable g
⊢ False
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f
⊢ ¬Integrable g
intro hg
no goals
α : Type u_1
β : Type ?u.63324
m : MeasurableSpace α
μ ν : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f
hg : Integrable g
⊢ False
exact hf (hg.congr h.symm)