awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
have mp : (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ S)) sorry) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ S)) sorry) : ℝ≥0∞) = 0
Tactic: rw [totalVariation, Measure.add_apply, hpos, hneg, toMeasureOfZeroLE_apply _ _ _ hS₁,
      toMeasureOfLEZero_apply _ _ _ hS₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ S)) ⋯) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ S)) ⋯) : ℝ≥0∞) = 0
have mp : ∀
  (h :
    ∀ ⦃s_1 : Set α⦄,
      Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (0 : ℝ≥0∞) → (↑s : Set α → ℝ) s_1 = 0)
  (S : Set α) (hS₁ : MeasurableSet S)
  (hS₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)) (i : Set α)
  (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0)
  (hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂)
  (hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ sorry hi₃),
  (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ S)) sorry) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ S)) sorry) : ℝ≥0∞) = 0
Tactic: rw [← VectorMeasure.AbsolutelyContinuous.ennrealToMeasure] at h
Cleared hypotheses: h, S, hS₁, hS₂, i, hi₁, hi₂, hi₃, hpos, hneg
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
⊢ s ≪ᵥ μ
have mpr : ∀ (S : Set α) (hS₁ : MeasurableSet S) (hS₂ : (↑μ : Set α → ℝ≥0∞) S = 0), (↑s : Set α → ℝ) S = 0
Tactic: refine VectorMeasure.AbsolutelyContinuous.mk fun S hS₁ hS₂ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : (↑μ : Set α → ℝ≥0∞) S = 0
⊢ (↑s : Set α → ℝ) S = 0
have hS₃ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← VectorMeasure.ennrealToMeasure_apply hS₁] at hS₂
Cleared hypotheses: hS₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.totalVariation ≪ μ ↔ s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
have mp : s.totalVariation ≪ μ → s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
mp : s.totalVariation ≪ μ → s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
⊢ s.totalVariation ≪ μ ↔ s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
have mpr : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ → s.totalVariation ≪ μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
have mp : s.toJordanDecomposition.posPart ≪ μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
mp : s.toJordanDecomposition.posPart ≪ μ
⊢ s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
have mp₁ : s.toJordanDecomposition.negPart ≪ μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.posPart ≪ μ
have mp : ∀ (S : Set α),
  MeasurableSet S →
    ∀ (hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
have this : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have := h hS₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
have this₁ : Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞) ∧
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [totalVariation, Measure.add_apply, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.negPart ≪ μ
have mp : ∀ (S : Set α),
  MeasurableSet S →
    ∀ (hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
have this : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have := h hS₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
have this₁ : Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞) ∧
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [totalVariation, Measure.add_apply, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
⊢ s.totalVariation ≪ μ
have mpr : ∀ (S : Set α),
  MeasurableSet S →
    ∀ (hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
have mpr : Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rw [totalVariation, Measure.add_apply, h.1 hS₂, h.2 hS₂, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
mpr :
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
have mpr₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞)
    ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) =
  0
Tactic: rw [totalVariation, Measure.add_apply, h.1 hS₂, h.2 hS₂, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
mpr :
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞)
    (0 : ℝ≥0∞)
mpr₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞)
      ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) =
    0
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
have mpr₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) = 0
Tactic: rw [totalVariation, Measure.add_apply, h.1 hS₂, h.2 hS₂, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
mpr :
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞)
    (0 : ℝ≥0∞)
mpr₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞)
      ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) =
    0
mpr₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
have mpr₃ : HAdd.hAdd (α := ℝ≥0∞) 0 0 = 0
Tactic: rw [totalVariation, Measure.add_apply, h.1 hS₂, h.2 hS₂, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
mpr :
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞)
    (0 : ℝ≥0∞)
mpr₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞)
      ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) =
    0
mpr₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) = 0
mpr₃ : HAdd.hAdd (α := ℝ≥0∞) 0 0 = 0
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
have mpr₄ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [totalVariation, Measure.add_apply, h.1 hS₂, h.2 hS₂, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
⊢ s ⟂ᵥ t ↔ s.totalVariation ⟂ₘ t.totalVariation
have mp : s ⟂ᵥ t → s.totalVariation ⟂ₘ t.totalVariation
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
mp : s ⟂ᵥ t → s.totalVariation ⟂ₘ t.totalVariation
⊢ s ⟂ᵥ t ↔ s.totalVariation ⟂ₘ t.totalVariation
have mpr : s.totalVariation ⟂ₘ t.totalVariation → s ⟂ᵥ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
⊢ s.totalVariation ⟂ₘ t.totalVariation
have mp : ∀ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0)
  (hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂)
  (hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ sorry hi₃), s.totalVariation ⟂ₘ t.totalVariation
Tactic: obtain ⟨i, hi₁, hi₂, hi₃, hipos, hineg⟩ := s.toJordanDecomposition_spec
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ s.totalVariation ⟂ₘ t.totalVariation
have mp : ∀ (j : Set α) (hj₁ : MeasurableSet j) (hj₂ : 0 ≤[j] t) (hj₃ : t ≤[jᶜ] 0)
  (hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂)
  (hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ sorry hj₃), s.totalVariation ⟂ₘ t.totalVariation
Tactic: obtain ⟨j, hj₁, hj₂, hj₃, hjpos, hjneg⟩ := t.toJordanDecomposition_spec
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ s.totalVariation ⟂ₘ t.totalVariation
have mp : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨u, hmeas, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
mp : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.totalVariation ⟂ₘ t.totalVariation
have mp₁ : Eq (α := ℝ≥0∞) ((t.totalVariation : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨u, hmeas, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
have mp : (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ u)) sorry) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ u)) sorry) : ℝ≥0∞) = 0
Tactic: rw [totalVariation, Measure.add_apply, hipos, hineg, toMeasureOfZeroLE_apply _ _ _ hmeas,
        toMeasureOfLEZero_apply _ _ _ hmeas]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ Eq (α := ℝ≥0∞) ((t.totalVariation : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have mp : (↑(NNReal.mk ((↑t : Set α → ℝ) (j ∩ uᶜ)) sorry) : ℝ≥0∞) + (↑(NNReal.mk (-(↑t : Set α → ℝ) (jᶜ ∩ uᶜ)) sorry) : ℝ≥0∞) = 0
Tactic: rw [totalVariation, Measure.add_apply, hjpos, hjneg,
        toMeasureOfZeroLE_apply _ _ _ hmeas.compl,
        toMeasureOfLEZero_apply _ _ _ hmeas.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ s ⟂ᵥ μ ↔ s.totalVariation ⟂ₘ μ.ennrealToMeasure
have mp : s ⟂ᵥ μ → s.totalVariation ⟂ₘ μ.ennrealToMeasure
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
mp : s ⟂ᵥ μ → s.totalVariation ⟂ₘ μ.ennrealToMeasure
⊢ s ⟂ᵥ μ ↔ s.totalVariation ⟂ₘ μ.ennrealToMeasure
have mpr : s.totalVariation ⟂ₘ μ.ennrealToMeasure → s ⟂ᵥ μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
⊢ s.totalVariation ⟂ₘ μ.ennrealToMeasure
have mp : ∀ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0)
  (hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂)
  (hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ sorry hi₃), s.totalVariation ⟂ₘ μ.ennrealToMeasure
Tactic: obtain ⟨i, hi₁, hi₂, hi₃, hpos, hneg⟩ := s.toJordanDecomposition_spec
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ s.totalVariation ⟂ₘ μ.ennrealToMeasure
have mp : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨u, hmeas, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
mp : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.totalVariation ⟂ₘ μ.ennrealToMeasure
have mp₁ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨u, hmeas, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
have mp : (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ u)) sorry) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ u)) sorry) : ℝ≥0∞) = 0
Tactic: rw [totalVariation, Measure.add_apply, hpos, hneg, toMeasureOfZeroLE_apply _ _ _ hmeas,
        toMeasureOfLEZero_apply _ _ _ hmeas]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have mp : (↑μ : Set α → ℝ≥0∞) uᶜ = 0
Tactic: rw [VectorMeasure.ennrealToMeasure_apply hmeas.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
hu₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s ⟂ᵥ μ
have mpr : ∀ (t : Set α) (htv : t ⊆ uᶜ) (hmt : MeasurableSet t), (↑μ : Set α → ℝ≥0∞) t = 0
Tactic: refine
      VectorMeasure.MutuallySingular.mk u hmeas
        (fun t htu _ => null_of_totalVariation_zero _ (measure_mono_null htu hu₁)) fun t htv hmt =>
        ?_