α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
⊢ t = singularPart s μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
⊢ t = singularPart s μ
have htμ' := htμ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ :
  (toJordanDecomposition t).posPart ⟂ₘ VectorMeasure.ennrealToMeasure (toENNRealVectorMeasure μ) ∧
    (toJordanDecomposition t).negPart ⟂ₘ VectorMeasure.ennrealToMeasure (toENNRealVectorMeasure μ)
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
⊢ t = singularPart s μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ : t ⟂ᵥ toENNRealVectorMeasure μ
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
⊢ t = singularPart s μ
rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff] at htμ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ :
  (toJordanDecomposition t).posPart ⟂ₘ
      Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ) ∧
    (toJordanDecomposition t).negPart ⟂ₘ
      Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ)
⊢ t = singularPart s μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
htμ :
  (toJordanDecomposition t).posPart ⟂ₘ VectorMeasure.ennrealToMeasure (toENNRealVectorMeasure μ) ∧
    (toJordanDecomposition t).negPart ⟂ₘ VectorMeasure.ennrealToMeasure (toENNRealVectorMeasure μ)
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
⊢ t = singularPart s μ
change
  _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ) ∧
    _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ) at htμ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ t = singularPart s μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ :
  (toJordanDecomposition t).posPart ⟂ₘ
      Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ) ∧
    (toJordanDecomposition t).negPart ⟂ₘ
      Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ)
⊢ t = singularPart s μ
rw [VectorMeasure.equivMeasure.right_inv] at htμ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ toSignedMeasure (toJordanDecomposition t).posPart - toSignedMeasure (toJordanDecomposition t).negPart =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ) -
      toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ)
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ t = singularPart s μ
rw [singularPart, ← t.toSignedMeasure_toJordanDecomposition,
  JordanDecomposition.toSignedMeasure]
case e_a.e_μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ (toJordanDecomposition t).posPart = Measure.singularPart (toJordanDecomposition s).posPart μ

case e_a.e_μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ (toJordanDecomposition t).negPart = Measure.singularPart (toJordanDecomposition s).negPart μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ toSignedMeasure (toJordanDecomposition t).posPart - toSignedMeasure (toJordanDecomposition t).negPart =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ) -
      toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ)
congr
case e_a.e_μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
hfpos : Measurable fun x => ENNReal.ofReal (f x)
⊢ (toJordanDecomposition t).posPart = Measure.singularPart (toJordanDecomposition s).posPart μ
case e_a.e_μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ (toJordanDecomposition t).posPart = Measure.singularPart (toJordanDecomposition s).posPart μ
have hfpos : Measurable fun x => ENNReal.ofReal (f x) := by measurability
case e_a.e_μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
hfpos : Measurable fun x => ENNReal.ofReal (f x)
⊢ (toJordanDecomposition s).posPart = (toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)
case e_a.e_μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
hfpos : Measurable fun x => ENNReal.ofReal (f x)
⊢ (toJordanDecomposition t).posPart = Measure.singularPart (toJordanDecomposition s).posPart μ
refine' eq_singularPart hfpos htμ.1 _
no goals
case e_a.e_μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
hfpos : Measurable fun x => ENNReal.ofReal (f x)
⊢ (toJordanDecomposition s).posPart = (toJordanDecomposition t).posPart + withDensity μ fun x => ENNReal.ofReal (f x)
rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
no goals
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ Measurable fun x => ENNReal.ofReal (f x)
measurability
case e_a.e_μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
hfneg : Measurable fun x => ENNReal.ofReal (-f x)
⊢ (toJordanDecomposition t).negPart = Measure.singularPart (toJordanDecomposition s).negPart μ
case e_a.e_μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ (toJordanDecomposition t).negPart = Measure.singularPart (toJordanDecomposition s).negPart μ
have hfneg : Measurable fun x => ENNReal.ofReal (-f x) := by measurability
case e_a.e_μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
hfneg : Measurable fun x => ENNReal.ofReal (-f x)
⊢ (toJordanDecomposition s).negPart = (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)
case e_a.e_μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
hfneg : Measurable fun x => ENNReal.ofReal (-f x)
⊢ (toJordanDecomposition t).negPart = Measure.singularPart (toJordanDecomposition s).negPart μ
refine' eq_singularPart hfneg htμ.2 _
no goals
case e_a.e_μ
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
hfneg : Measurable fun x => ENNReal.ofReal (-f x)
⊢ (toJordanDecomposition s).negPart = (toJordanDecomposition t).negPart + withDensity μ fun x => ENNReal.ofReal (-f x)
rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
no goals
α : Type u_1
β : Type ?u.494818
m : MeasurableSpace α
μ ν : Measure α
s t✝ t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f
hadd : s = t + withDensityᵥ μ f
htμ' : t ⟂ᵥ toENNRealVectorMeasure μ
htμ : (toJordanDecomposition t).posPart ⟂ₘ μ ∧ (toJordanDecomposition t).negPart ⟂ₘ μ
⊢ Measurable fun x => ENNReal.ofReal (-f x)
measurability