case pos
α : Type u_1
β : Type ?u.458599
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
hfi : Integrable f
⊢ HaveLebesgueDecomposition s μ

case neg
α : Type u_1
β : Type ?u.458599
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
hfi : ¬Integrable f
⊢ HaveLebesgueDecomposition s μ
α : Type u_1
β : Type ?u.458599
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
⊢ HaveLebesgueDecomposition s μ
by_cases hfi : Integrable f μ
no goals
case pos
α : Type u_1
β : Type ?u.458599
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
hfi : Integrable f
⊢ HaveLebesgueDecomposition s μ
exact haveLebesgueDecomposition_mk' μ hf hfi htμ hadd
case neg
α : Type u_1
β : Type ?u.458599
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t
hfi : ¬Integrable f
⊢ HaveLebesgueDecomposition s μ
case neg
α : Type u_1
β : Type ?u.458599
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
hfi : ¬Integrable f
⊢ HaveLebesgueDecomposition s μ
rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd
case neg
α : Type u_1
β : Type ?u.458599
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t
hfi : ¬Integrable f
⊢ s = t + withDensityᵥ μ 0
case neg
α : Type u_1
β : Type ?u.458599
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t
hfi : ¬Integrable f
⊢ HaveLebesgueDecomposition s μ
refine' haveLebesgueDecomposition_mk' μ measurable_zero (integrable_zero _ _ μ) htμ _
no goals
case neg
α : Type u_1
β : Type ?u.458599
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t
hfi : ¬Integrable f
⊢ s = t + withDensityᵥ μ 0
rwa [withDensityᵥ_zero, add_zero]