case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
⊢ JordanDecomposition.toSignedMeasure (toJordanDecomposition s) = s
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
⊢ JordanDecomposition.toSignedMeasure (toJordanDecomposition s) = s
obtain ⟨i, hi₁, hi₂, hi₃, hμ, hν⟩ := s.toJordanDecomposition_spec
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
⊢ Measure.toSignedMeasure (toMeasureOfZeroLE s i hi₁ hi₂) -
      Measure.toSignedMeasure (toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃) =
    s
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
⊢ JordanDecomposition.toSignedMeasure (toJordanDecomposition s) = s
simp only [JordanDecomposition.toSignedMeasure, hμ, hν]
case intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
k : Set α
⊢ MeasurableSet k →
    ↑(Measure.toSignedMeasure (toMeasureOfZeroLE s i hi₁ hi₂) -
            Measure.toSignedMeasure (toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃))
        k =
      ↑s k
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
⊢ Measure.toSignedMeasure (toMeasureOfZeroLE s i hi₁ hi₂) -
      Measure.toSignedMeasure (toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃) =
    s
ext k
case intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
k : Set α
hk : MeasurableSet k
⊢ ↑(Measure.toSignedMeasure (toMeasureOfZeroLE s i hi₁ hi₂) -
          Measure.toSignedMeasure (toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃))
      k =
    ↑s k
case intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
k : Set α
⊢ MeasurableSet k →
    ↑(Measure.toSignedMeasure (toMeasureOfZeroLE s i hi₁ hi₂) -
            Measure.toSignedMeasure (toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃))
        k =
      ↑s k
intro hk
case intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
k : Set α
hk : MeasurableSet k
⊢ ENNReal.toReal ↑{ val := ↑s (i ∩ k), property := (_ : 0 ≤ ↑s (i ∩ k)) } -
      ENNReal.toReal ↑{ val := -↑s (iᶜ ∩ k), property := (_ : 0 ≤ -↑s (iᶜ ∩ k)) } =
    ↑s k
case intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
k : Set α
hk : MeasurableSet k
⊢ ↑(Measure.toSignedMeasure (toMeasureOfZeroLE s i hi₁ hi₂) -
          Measure.toSignedMeasure (toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃))
      k =
    ↑s k
rw [toSignedMeasure_sub_apply hk, toMeasureOfZeroLE_apply _ hi₂ hi₁ hk,
  toMeasureOfLEZero_apply _ hi₃ hi₁.compl hk]
case intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
k : Set α
hk : MeasurableSet k
⊢ ↑s (i ∩ k) + ↑s (iᶜ ∩ k) = ↑s k
case intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
k : Set α
hk : MeasurableSet k
⊢ ENNReal.toReal ↑{ val := ↑s (i ∩ k), property := (_ : 0 ≤ ↑s (i ∩ k)) } -
      ENNReal.toReal ↑{ val := -↑s (iᶜ ∩ k), property := (_ : 0 ≤ -↑s (iᶜ ∩ k)) } =
    ↑s k
simp only [ENNReal.coe_toReal, NNReal.coe_mk, ENNReal.some_eq_coe, sub_neg_eq_add]
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
k : Set α
hk : MeasurableSet k
⊢ Disjoint (i ∩ k) (iᶜ ∩ k)
case intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
k : Set α
hk : MeasurableSet k
⊢ ↑s (i ∩ k) + ↑s (iᶜ ∩ k) = ↑s k
rw [← of_union _ (MeasurableSet.inter hi₁ hk) (MeasurableSet.inter hi₁.compl hk),
  Set.inter_comm i, Set.inter_comm (iᶜ), Set.inter_union_compl _ _]
no goals
α : Type u_1
β : Type ?u.39165
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i
hi₃ : VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)
hμ : (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂
hν : (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
k : Set α
hk : MeasurableSet k
⊢ Disjoint (i ∩ k) (iᶜ ∩ k)
exact (disjoint_compl_right.inf_left _).inf_right _