case mp
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
⊢ (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ

case mpr
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
⊢ totalVariation s ≪ μ
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ totalVariation s ≪ μ ↔ (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
constructor <;> intro h
case mp.left
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
⊢ (toJordanDecomposition s).posPart ≪ μ

case mp.right
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
⊢ (toJordanDecomposition s).negPart ≪ μ
case mp
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
⊢ (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
constructor
case mp.left
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : ↑↑μ S = 0
this : ↑↑(toJordanDecomposition s).posPart S = 0 ∧ ↑↑(toJordanDecomposition s).negPart S = 0
⊢ ↑↑(toJordanDecomposition s).posPart S = 0

case mp.right
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : ↑↑μ S = 0
this : ↑↑(toJordanDecomposition s).posPart S = 0 ∧ ↑↑(toJordanDecomposition s).negPart S = 0
⊢ ↑↑(toJordanDecomposition s).negPart S = 0
case mp.left
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
⊢ (toJordanDecomposition s).posPart ≪ μ

case mp.right
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
⊢ (toJordanDecomposition s).negPart ≪ μ
all_goals
  refine' Measure.AbsolutelyContinuous.mk fun S _ hS₂ => _
  have := h hS₂
  rw [totalVariation, Measure.add_apply, add_eq_zero_iff] at this
no goals
case mp.left
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : ↑↑μ S = 0
this : ↑↑(toJordanDecomposition s).posPart S = 0 ∧ ↑↑(toJordanDecomposition s).negPart S = 0
⊢ ↑↑(toJordanDecomposition s).posPart S = 0

case mp.right
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : ↑↑μ S = 0
this : ↑↑(toJordanDecomposition s).posPart S = 0 ∧ ↑↑(toJordanDecomposition s).negPart S = 0
⊢ ↑↑(toJordanDecomposition s).negPart S = 0
exacts [this.1, this.2]
case mp.right
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : ↑↑μ S = 0
⊢ ↑↑(toJordanDecomposition s).negPart S = 0
case mp.right
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
⊢ (toJordanDecomposition s).negPart ≪ μ
refine' Measure.AbsolutelyContinuous.mk fun S _ hS₂ => _
case mp.right
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : ↑↑μ S = 0
this : ↑↑(totalVariation s) S = 0
⊢ ↑↑(toJordanDecomposition s).negPart S = 0
case mp.right
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : ↑↑μ S = 0
⊢ ↑↑(toJordanDecomposition s).negPart S = 0
have := h hS₂
case mp.right
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : ↑↑μ S = 0
this : ↑↑(toJordanDecomposition s).posPart S = 0 ∧ ↑↑(toJordanDecomposition s).negPart S = 0
⊢ ↑↑(toJordanDecomposition s).negPart S = 0
case mp.right
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : totalVariation s ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : ↑↑μ S = 0
this : ↑↑(totalVariation s) S = 0
⊢ ↑↑(toJordanDecomposition s).negPart S = 0
rw [totalVariation, Measure.add_apply, add_eq_zero_iff] at this
case mpr
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : ↑↑μ S = 0
⊢ ↑↑(totalVariation s) S = 0
case mpr
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
⊢ totalVariation s ≪ μ
refine' Measure.AbsolutelyContinuous.mk fun S _ hS₂ => _
no goals
case mpr
α : Type u_1
β : Type ?u.93781
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : (toJordanDecomposition s).posPart ≪ μ ∧ (toJordanDecomposition s).negPart ≪ μ
S : Set α
x✝ : MeasurableSet S
hS₂ : ↑↑μ S = 0
⊢ ↑↑(totalVariation s) S = 0
rw [totalVariation, Measure.add_apply, h.1 hS₂, h.2 hS₂, add_zero]