α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
⊢ HaveLebesgueDecomposition s μ
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
⊢ HaveLebesgueDecomposition s μ
have htμ' := htμ
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : totalVariation t ⟂ₘ VectorMeasure.ennrealToMeasure (toENNRealVectorMeasure μ)
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
⊢ HaveLebesgueDecomposition s μ
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
⊢ HaveLebesgueDecomposition s μ
rw [mutuallySingular_ennreal_iff] at htμ
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : totalVariation t ⟂ₘ Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ)
⊢ HaveLebesgueDecomposition s μ
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : totalVariation t ⟂ₘ VectorMeasure.ennrealToMeasure (toENNRealVectorMeasure μ)
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
⊢ HaveLebesgueDecomposition s μ
change _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ) at htμ
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ HaveLebesgueDecomposition s μ
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : totalVariation t ⟂ₘ Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ)
⊢ HaveLebesgueDecomposition s μ
rw [VectorMeasure.equivMeasure.right_inv, totalVariation_mutuallySingular_iff] at htμ
no goals
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ HaveLebesgueDecomposition s μ
refine'
  { posPart := by
      use ⟨t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)⟩
      refine' ⟨hf.ennreal_ofReal, htμ.1, _⟩
      rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
    negPart := by
      use ⟨t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)⟩
      refine' ⟨hf.neg.ennreal_ofReal, htμ.2, _⟩
      rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd] }
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ Measurable ((toJordanDecomposition t).posPart, fun x => ENNReal.ofReal (f x)).snd ∧
    ((toJordanDecomposition t).posPart, fun x => ENNReal.ofReal (f x)).fst ⟂ₘ μ ∧
      (toJordanDecomposition s).posPart =
        ((toJordanDecomposition t).posPart, fun x => ENNReal.ofReal (f x)).fst +
          withDensity μ ((toJordanDecomposition t).posPart, fun x => ENNReal.ofReal (f x)).snd
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ Measure.HaveLebesgueDecomposition (toJordanDecomposition s).posPart μ
use ⟨t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)⟩
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ (toJordanDecomposition s).posPart =
    ((toJordanDecomposition t).posPart, fun x => ENNReal.ofReal (f x)).fst +
      withDensity μ ((toJordanDecomposition t).posPart, fun x => ENNReal.ofReal (f x)).snd
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ Measurable ((toJordanDecomposition t).posPart, fun x => ENNReal.ofReal (f x)).snd ∧
    ((toJordanDecomposition t).posPart, fun x => ENNReal.ofReal (f x)).fst ⟂ₘ μ ∧
      (toJordanDecomposition s).posPart =
        ((toJordanDecomposition t).posPart, fun x => ENNReal.ofReal (f x)).fst +
          withDensity μ ((toJordanDecomposition t).posPart, fun x => ENNReal.ofReal (f x)).snd
refine' ⟨hf.ennreal_ofReal, htμ.1, _⟩
no goals
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ (toJordanDecomposition s).posPart =
    ((toJordanDecomposition t).posPart, fun x => ENNReal.ofReal (f x)).fst +
      withDensity μ ((toJordanDecomposition t).posPart, fun x => ENNReal.ofReal (f x)).snd
rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ Measurable ((toJordanDecomposition t).negPart, fun x => ENNReal.ofReal (-f x)).snd ∧
    ((toJordanDecomposition t).negPart, fun x => ENNReal.ofReal (-f x)).fst ⟂ₘ μ ∧
      (toJordanDecomposition s).negPart =
        ((toJordanDecomposition t).negPart, fun x => ENNReal.ofReal (-f x)).fst +
          withDensity μ ((toJordanDecomposition t).negPart, fun x => ENNReal.ofReal (-f x)).snd
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ Measure.HaveLebesgueDecomposition (toJordanDecomposition s).negPart μ
use ⟨t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)⟩
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ (toJordanDecomposition s).negPart =
    ((toJordanDecomposition t).negPart, fun x => ENNReal.ofReal (-f x)).fst +
      withDensity μ ((toJordanDecomposition t).negPart, fun x => ENNReal.ofReal (-f x)).snd
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ Measurable ((toJordanDecomposition t).negPart, fun x => ENNReal.ofReal (-f x)).snd ∧
    ((toJordanDecomposition t).negPart, fun x => ENNReal.ofReal (-f x)).fst ⟂ₘ μ ∧
      (toJordanDecomposition s).negPart =
        ((toJordanDecomposition t).negPart, fun x => ENNReal.ofReal (-f x)).fst +
          withDensity μ ((toJordanDecomposition t).negPart, fun x => ENNReal.ofReal (-f x)).snd
refine' ⟨hf.neg.ennreal_ofReal, htμ.2, _⟩
no goals
α : Type u_1
β : Type ?u.456531
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ (toJordanDecomposition s).negPart =
    ((toJordanDecomposition t).negPart, fun x => ENNReal.ofReal (-f x)).fst +
      withDensity μ ((toJordanDecomposition t).negPart, fun x => ENNReal.ofReal (-f x)).snd
rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]