case mp
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ s ⟂ᵥ μ → totalVariation s ⟂ₘ VectorMeasure.ennrealToMeasure μ

case mpr
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ totalVariation s ⟂ₘ VectorMeasure.ennrealToMeasure μ → s ⟂ᵥ μ
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ s ⟂ᵥ μ ↔ totalVariation s ⟂ₘ VectorMeasure.ennrealToMeasure μ
constructor
case mp.intro.intro.intro
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑s t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑μ t = 0
⊢ totalVariation s ⟂ₘ VectorMeasure.ennrealToMeasure μ
case mp
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ s ⟂ᵥ μ → totalVariation s ⟂ₘ VectorMeasure.ennrealToMeasure μ
rintro ⟨u, hmeas, hu₁, hu₂⟩
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑s t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑μ t = 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 ⟂ₘ VectorMeasure.ennrealToMeasure μ
case mp.intro.intro.intro
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑s t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑μ t = 0
⊢ totalVariation s ⟂ₘ VectorMeasure.ennrealToMeasure μ
obtain ⟨i, hi₁, hi₂, hi₃, hpos, hneg⟩ := s.toJordanDecomposition_spec
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑s t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑μ t = 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) u = 0

case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑s t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑μ t = 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₃
⊢ ↑↑(VectorMeasure.ennrealToMeasure μ) (uᶜ) = 0
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑s t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑μ t = 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 ⟂ₘ VectorMeasure.ennrealToMeasure μ
refine' ⟨u, hmeas, _, _⟩
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑s t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑μ t = 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 ∩ u), property := (_ : 0 ≤ ↑s (i ∩ u)) } +
      ↑{ val := -↑s (iᶜ ∩ u), property := (_ : 0 ≤ -↑s (iᶜ ∩ u)) } =
    0
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑s t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑μ t = 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) u = 0
rw [totalVariation, Measure.add_apply, hpos, hneg, toMeasureOfZeroLE_apply _ _ _ hmeas,
  toMeasureOfLEZero_apply _ _ _ hmeas]
no goals
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑s t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑μ t = 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 ∩ u), property := (_ : 0 ≤ ↑s (i ∩ u)) } +
      ↑{ val := -↑s (iᶜ ∩ u), property := (_ : 0 ≤ -↑s (iᶜ ∩ u)) } =
    0
simp [hu₁ _ (Set.inter_subset_right _ _), ← NNReal.eq_iff]
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑s t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑μ t = 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₃
⊢ ↑μ (uᶜ) = 0
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑s t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑μ t = 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₃
⊢ ↑↑(VectorMeasure.ennrealToMeasure μ) (uᶜ) = 0
rw [VectorMeasure.ennrealToMeasure_apply hmeas.compl]
no goals
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑s t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑μ t = 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₃
⊢ ↑μ (uᶜ) = 0
exact hu₂ _ (Set.Subset.refl _)
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ↑↑(totalVariation s) u = 0
hu₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) (uᶜ) = 0
⊢ s ⟂ᵥ μ
case mpr
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ totalVariation s ⟂ₘ VectorMeasure.ennrealToMeasure μ → s ⟂ᵥ μ
rintro ⟨u, hmeas, hu₁, hu₂⟩
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ↑↑(totalVariation s) u = 0
hu₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) (uᶜ) = 0
t : Set α
htv : t ⊆ uᶜ
hmt : MeasurableSet t
⊢ ↑μ t = 0
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ↑↑(totalVariation s) u = 0
hu₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) (uᶜ) = 0
⊢ s ⟂ᵥ μ
refine'
  VectorMeasure.MutuallySingular.mk u hmeas
    (fun t htu _ => null_of_totalVariation_zero _ (measure_mono_null htu hu₁)) fun t htv hmt =>
    _
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ↑↑(totalVariation s) u = 0
hu₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) (uᶜ) = 0
t : Set α
htv : t ⊆ uᶜ
hmt : MeasurableSet t
⊢ ↑↑(VectorMeasure.ennrealToMeasure μ) t = 0
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ↑↑(totalVariation s) u = 0
hu₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) (uᶜ) = 0
t : Set α
htv : t ⊆ uᶜ
hmt : MeasurableSet t
⊢ ↑μ t = 0
rw [← VectorMeasure.ennrealToMeasure_apply hmt]
no goals
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.98874
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ↑↑(totalVariation s) u = 0
hu₂ : ↑↑(VectorMeasure.ennrealToMeasure μ) (uᶜ) = 0
t : Set α
htv : t ⊆ uᶜ
hmt : MeasurableSet t
⊢ ↑↑(VectorMeasure.ennrealToMeasure μ) t = 0
exact measure_mono_null htv hu₂