case mp
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
⊢ totalVariation s ≪ VectorMeasure.ennrealToMeasure μ

case mpr
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : totalVariation s ≪ VectorMeasure.ennrealToMeasure μ
⊢ s ≪ᵥ μ
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ s ≪ᵥ μ ↔ totalVariation s ≪ VectorMeasure.ennrealToMeasure μ
constructor <;> intro h
case mp
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) S = 0
⊢ ↑↑(totalVariation s) S = 0
case mp
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
⊢ totalVariation s ≪ VectorMeasure.ennrealToMeasure μ
refine' Measure.AbsolutelyContinuous.mk fun S hS₁ hS₂ => _
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hpos : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hneg : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
⊢ ↑↑(totalVariation s) S = 0
case mp
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) S = 0
⊢ ↑↑(totalVariation s) S = 0
obtain ⟨i, hi₁, hi₂, hi₃, hpos, hneg⟩ := s.toJordanDecomposition_spec
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hpos : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hneg : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
⊢ ↑{ val := ↑s (i ∩ S), property := (_ : 0 ≤ ↑s (i ∩ S)) } +
      ↑{ val := -↑s (iᶜ ∩ S), property := (_ : 0 ≤ -↑s (iᶜ ∩ S)) } =
    0
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hpos : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hneg : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
⊢ ↑↑(totalVariation s) S = 0
rw [totalVariation, Measure.add_apply, hpos, hneg, toMeasureOfZeroLE_apply _ _ _ hS₁,
  toMeasureOfLEZero_apply _ _ _ hS₁]
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s_1 : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s_1 = 0 → ↑s s_1 = 0
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hpos : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hneg : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
⊢ ↑{ val := ↑s (i ∩ S), property := (_ : 0 ≤ ↑s (i ∩ S)) } +
      ↑{ val := -↑s (iᶜ ∩ S), property := (_ : 0 ≤ -↑s (iᶜ ∩ S)) } =
    0
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hpos : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hneg : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
⊢ ↑{ val := ↑s (i ∩ S), property := (_ : 0 ≤ ↑s (i ∩ S)) } +
      ↑{ val := -↑s (iᶜ ∩ S), property := (_ : 0 ≤ -↑s (iᶜ ∩ S)) } =
    0
rw [← VectorMeasure.AbsolutelyContinuous.ennrealToMeasure] at h
no goals
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s_1 : Set α⦄, ↑↑(VectorMeasure.ennrealToMeasure μ) s_1 = 0 → ↑s s_1 = 0
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hpos : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hneg : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
⊢ ↑{ val := ↑s (i ∩ S), property := (_ : 0 ≤ ↑s (i ∩ S)) } +
      ↑{ val := -↑s (iᶜ ∩ S), property := (_ : 0 ≤ -↑s (iᶜ ∩ S)) } =
    0
simp [h (measure_mono_null (i.inter_subset_right S) hS₂),
  h (measure_mono_null (iᶜ.inter_subset_right S) hS₂), ← NNReal.eq_iff]
case mpr
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : totalVariation s ≪ VectorMeasure.ennrealToMeasure μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑μ S = 0
⊢ ↑s S = 0
case mpr
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : totalVariation s ≪ VectorMeasure.ennrealToMeasure μ
⊢ s ≪ᵥ μ
refine' VectorMeasure.AbsolutelyContinuous.mk fun S hS₁ hS₂ => _
case mpr
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : totalVariation s ≪ VectorMeasure.ennrealToMeasure μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) S = 0
⊢ ↑s S = 0
case mpr
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : totalVariation s ≪ VectorMeasure.ennrealToMeasure μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑μ S = 0
⊢ ↑s S = 0
rw [← VectorMeasure.ennrealToMeasure_apply hS₁] at hS₂
no goals
case mpr
α : Type u_1
β : Type ?u.89974
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : totalVariation s ≪ VectorMeasure.ennrealToMeasure μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) S = 0
⊢ ↑s S = 0
exact null_of_totalVariation_zero s (h hS₂)