[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h : μ ≤ ν
⊢ μ ≤ 0 + ν
[PROOFSTEP]
rwa [zero_add]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
⊢ ↑↑(μ - ν) s = ↑↑μ s - ↑↑ν s
[PROOFSTEP]
let measure_sub : Measure α :=
  MeasureTheory.Measure.ofMeasurable (fun (t : Set α) (_ : MeasurableSet t) => μ t - ν t) (by simp)
    (by
      intro g h_meas h_disj; simp only; rw [ENNReal.tsum_sub]
      repeat' rw [← MeasureTheory.measure_iUnion h_disj h_meas]
      exacts [MeasureTheory.measure_ne_top _ _, fun i => h₂ _ (h_meas _)])
      -- Now, we demonstrate `μ - ν = measure_sub`, and apply it.
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
⊢ (fun t x => ↑↑μ t - ↑↑ν t) ∅ (_ : MeasurableSet ∅) = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
⊢ ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) =
        ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (f i) (_ : MeasurableSet (f i))
[PROOFSTEP]
intro g h_meas h_disj
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Disjoint on g)
⊢ (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
    ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i))
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Disjoint on g)
⊢ ↑↑μ (⋃ (i : ℕ), g i) - ↑↑ν (⋃ (i : ℕ), g i) = ∑' (i : ℕ), (↑↑μ (g i) - ↑↑ν (g i))
[PROOFSTEP]
rw [ENNReal.tsum_sub]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Disjoint on g)
⊢ ↑↑μ (⋃ (i : ℕ), g i) - ↑↑ν (⋃ (i : ℕ), g i) = ∑' (i : ℕ), ↑↑μ (g i) - ∑' (i : ℕ), ↑↑ν (g i)
case h₁
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Disjoint on g)
⊢ ∑' (i : ℕ), ↑↑ν (g i) ≠ ⊤
case h₂
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Disjoint on g)
⊢ (fun i => ↑↑ν (g i)) ≤ fun i => ↑↑μ (g i)
[PROOFSTEP]
repeat' rw [← MeasureTheory.measure_iUnion h_disj h_meas]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Disjoint on g)
⊢ ↑↑μ (⋃ (i : ℕ), g i) - ↑↑ν (⋃ (i : ℕ), g i) = ∑' (i : ℕ), ↑↑μ (g i) - ∑' (i : ℕ), ↑↑ν (g i)
[PROOFSTEP]
rw [← MeasureTheory.measure_iUnion h_disj h_meas]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Disjoint on g)
⊢ ↑↑μ (⋃ (i : ℕ), g i) - ↑↑ν (⋃ (i : ℕ), g i) = ↑↑μ (⋃ (i : ℕ), g i) - ∑' (i : ℕ), ↑↑ν (g i)
[PROOFSTEP]
rw [← MeasureTheory.measure_iUnion h_disj h_meas]
[GOAL]
case h₁
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Disjoint on g)
⊢ ∑' (i : ℕ), ↑↑ν (g i) ≠ ⊤
[PROOFSTEP]
rw [← MeasureTheory.measure_iUnion h_disj h_meas]
[GOAL]
case h₁
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Disjoint on g)
⊢ ↑↑ν (⋃ (i : ℕ), g i) ≠ ⊤
[PROOFSTEP]
rw [← MeasureTheory.measure_iUnion h_disj h_meas]
[GOAL]
case h₂
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Disjoint on g)
⊢ (fun i => ↑↑ν (g i)) ≤ fun i => ↑↑μ (g i)
[PROOFSTEP]
rw [← MeasureTheory.measure_iUnion h_disj h_meas]
[GOAL]
case h₁
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Disjoint on g)
⊢ ↑↑ν (⋃ (i : ℕ), g i) ≠ ⊤
case h₂
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
g : ℕ → Set α
h_meas : ∀ (i : ℕ), MeasurableSet (g i)
h_disj : Pairwise (Disjoint on g)
⊢ (fun i => ↑↑ν (g i)) ≤ fun i => ↑↑μ (g i)
[PROOFSTEP]
exacts [MeasureTheory.measure_ne_top _ _, fun i => h₂ _ (h_meas _)]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
⊢ ↑↑(μ - ν) s = ↑↑μ s - ↑↑ν s
[PROOFSTEP]
have h_measure_sub_add : ν + measure_sub = μ :=
  by
  ext1 t h_t_measurable_set
  simp only [Pi.add_apply, coe_add]
  rw [MeasureTheory.Measure.ofMeasurable_apply _ h_t_measurable_set, add_comm,
    tsub_add_cancel_of_le (h₂ t h_t_measurable_set)]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
⊢ ν + measure_sub = μ
[PROOFSTEP]
ext1 t h_t_measurable_set
[GOAL]
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
t : Set α
h_t_measurable_set : MeasurableSet t
⊢ ↑↑(ν + measure_sub) t = ↑↑μ t
[PROOFSTEP]
simp only [Pi.add_apply, coe_add]
[GOAL]
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
t : Set α
h_t_measurable_set : MeasurableSet t
⊢ ↑↑ν t +
      ↑↑(ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
              (_ :
                ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
                  Pairwise (Disjoint on g) →
                    (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
                      ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i))))
        t =
    ↑↑μ t
[PROOFSTEP]
rw [MeasureTheory.Measure.ofMeasurable_apply _ h_t_measurable_set, add_comm,
  tsub_add_cancel_of_le (h₂ t h_t_measurable_set)]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
h_measure_sub_add : ν + measure_sub = μ
⊢ ↑↑(μ - ν) s = ↑↑μ s - ↑↑ν s
[PROOFSTEP]
have h_measure_sub_eq : μ - ν = measure_sub :=
  by
  rw [MeasureTheory.Measure.sub_def]
  apply le_antisymm
  · apply sInf_le
    simp [le_refl, add_comm, h_measure_sub_add]
  apply le_sInf
  intro d h_d
  rw [← h_measure_sub_add, mem_setOf_eq, add_comm d] at h_d
  apply Measure.le_of_add_le_add_left h_d
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
h_measure_sub_add : ν + measure_sub = μ
⊢ μ - ν = measure_sub
[PROOFSTEP]
rw [MeasureTheory.Measure.sub_def]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
h_measure_sub_add : ν + measure_sub = μ
⊢ sInf {d | μ ≤ d + ν} = measure_sub
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
h_measure_sub_add : ν + measure_sub = μ
⊢ sInf {d | μ ≤ d + ν} ≤ measure_sub
[PROOFSTEP]
apply sInf_le
[GOAL]
case a.a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
h_measure_sub_add : ν + measure_sub = μ
⊢ measure_sub ∈ {d | μ ≤ d + ν}
[PROOFSTEP]
simp [le_refl, add_comm, h_measure_sub_add]
[GOAL]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
h_measure_sub_add : ν + measure_sub = μ
⊢ measure_sub ≤ sInf {d | μ ≤ d + ν}
[PROOFSTEP]
apply le_sInf
[GOAL]
case a.a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
h_measure_sub_add : ν + measure_sub = μ
⊢ ∀ (b : Measure α), b ∈ {d | μ ≤ d + ν} → measure_sub ≤ b
[PROOFSTEP]
intro d h_d
[GOAL]
case a.a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
h_measure_sub_add : ν + measure_sub = μ
d : Measure α
h_d : d ∈ {d | μ ≤ d + ν}
⊢ measure_sub ≤ d
[PROOFSTEP]
rw [← h_measure_sub_add, mem_setOf_eq, add_comm d] at h_d
[GOAL]
case a.a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
h_measure_sub_add : ν + measure_sub = μ
d : Measure α
h_d : ν + measure_sub ≤ ν + d
⊢ measure_sub ≤ d
[PROOFSTEP]
apply Measure.le_of_add_le_add_left h_d
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
h_measure_sub_add : ν + measure_sub = μ
h_measure_sub_eq : μ - ν = measure_sub
⊢ ↑↑(μ - ν) s = ↑↑μ s - ↑↑ν s
[PROOFSTEP]
rw [h_measure_sub_eq]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α :=
  ofMeasurable (fun t x => ↑↑μ t - ↑↑ν t) (_ : ↑↑μ ∅ - ↑↑ν ∅ = 0)
    (_ :
      ∀ ⦃g : ℕ → Set α⦄ (h_meas : ∀ (i : ℕ), MeasurableSet (g i)),
        Pairwise (Disjoint on g) →
          (fun t x => ↑↑μ t - ↑↑ν t) (⋃ (i : ℕ), g i) (_ : MeasurableSet (⋃ (b : ℕ), g b)) =
            ∑' (i : ℕ), (fun t x => ↑↑μ t - ↑↑ν t) (g i) (_ : MeasurableSet (g i)))
h_measure_sub_add : ν + measure_sub = μ
h_measure_sub_eq : μ - ν = measure_sub
⊢ ↑↑measure_sub s = ↑↑μ s - ↑↑ν s
[PROOFSTEP]
apply Measure.ofMeasurable_apply _ h₁
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : ν ≤ μ
⊢ μ - ν + ν = μ
[PROOFSTEP]
ext1 s h_s_meas
[GOAL]
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s✝ : Set α
inst✝ : IsFiniteMeasure ν
h₁ : ν ≤ μ
s : Set α
h_s_meas : MeasurableSet s
⊢ ↑↑(μ - ν + ν) s = ↑↑μ s
[PROOFSTEP]
rw [add_apply, sub_apply h_s_meas h₁, tsub_add_cancel_of_le (h₁ s h_s_meas)]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ restrict (μ - ν) s = restrict μ s - restrict ν s
[PROOFSTEP]
repeat' rw [sub_def]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ restrict (μ - ν) s = restrict μ s - restrict ν s
[PROOFSTEP]
rw [sub_def]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ restrict (sInf {d | μ ≤ d + ν}) s = restrict μ s - restrict ν s
[PROOFSTEP]
rw [sub_def]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ restrict (sInf {d | μ ≤ d + ν}) s = sInf {d | restrict μ s ≤ d + restrict ν s}
[PROOFSTEP]
rw [sub_def]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ restrict (sInf {d | μ ≤ d + ν}) s = sInf {d | restrict μ s ≤ d + restrict ν s}
[PROOFSTEP]
have h_nonempty : {d | μ ≤ d + ν}.Nonempty := ⟨μ, Measure.le_add_right le_rfl⟩
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ restrict (sInf {d | μ ≤ d + ν}) s = sInf {d | restrict μ s ≤ d + restrict ν s}
[PROOFSTEP]
rw [restrict_sInf_eq_sInf_restrict h_nonempty h_meas_s]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ sInf ((fun μ => restrict μ s) '' {d | μ ≤ d + ν}) = sInf {d | restrict μ s ≤ d + restrict ν s}
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ sInf ((fun μ => restrict μ s) '' {d | μ ≤ d + ν}) ≤ sInf {d | restrict μ s ≤ d + restrict ν s}
[PROOFSTEP]
refine' sInf_le_sInf_of_forall_exists_le _
[GOAL]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ ∀ (x : Measure α),
    x ∈ {d | restrict μ s ≤ d + restrict ν s} → ∃ y, y ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν} ∧ y ≤ x
[PROOFSTEP]
intro ν' h_ν'_in
[GOAL]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : ν' ∈ {d | restrict μ s ≤ d + restrict ν s}
⊢ ∃ y, y ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν} ∧ y ≤ ν'
[PROOFSTEP]
rw [mem_setOf_eq] at h_ν'_in
[GOAL]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ ∃ y, y ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν} ∧ y ≤ ν'
[PROOFSTEP]
refine' ⟨ν'.restrict s, _, restrict_le_self⟩
[GOAL]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ restrict ν' s ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν}
[PROOFSTEP]
refine' ⟨ν' + (⊤ : Measure α).restrict sᶜ, _, _⟩
[GOAL]
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ ν' + restrict ⊤ sᶜ ∈ {d | μ ≤ d + ν}
[PROOFSTEP]
rw [mem_setOf_eq, add_right_comm, Measure.le_iff]
[GOAL]
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → ↑↑μ s_1 ≤ ↑↑(ν' + ν + restrict ⊤ sᶜ) s_1
[PROOFSTEP]
intro t h_meas_t
[GOAL]
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ t ≤ ↑↑(ν' + ν + restrict ⊤ sᶜ) t
[PROOFSTEP]
repeat' rw [← measure_inter_add_diff t h_meas_s]
[GOAL]
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ t ≤ ↑↑(ν' + ν + restrict ⊤ sᶜ) t
[PROOFSTEP]
rw [← measure_inter_add_diff t h_meas_s]
[GOAL]
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) + ↑↑μ (t \ s) ≤ ↑↑(ν' + ν + restrict ⊤ sᶜ) t
[PROOFSTEP]
rw [← measure_inter_add_diff t h_meas_s]
[GOAL]
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) + ↑↑μ (t \ s) ≤ ↑↑(ν' + ν + restrict ⊤ sᶜ) (t ∩ s) + ↑↑(ν' + ν + restrict ⊤ sᶜ) (t \ s)
[PROOFSTEP]
rw [← measure_inter_add_diff t h_meas_s]
[GOAL]
case a.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) + ↑↑μ (t \ s) ≤ ↑↑(ν' + ν + restrict ⊤ sᶜ) (t ∩ s) + ↑↑(ν' + ν + restrict ⊤ sᶜ) (t \ s)
[PROOFSTEP]
refine' add_le_add _ _
[GOAL]
case a.refine'_1.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) ≤ ↑↑(ν' + ν + restrict ⊤ sᶜ) (t ∩ s)
[PROOFSTEP]
rw [add_apply, add_apply]
[GOAL]
case a.refine'_1.refine'_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) ≤ ↑↑ν' (t ∩ s) + ↑↑ν (t ∩ s) + ↑↑(restrict ⊤ sᶜ) (t ∩ s)
[PROOFSTEP]
apply le_add_right _
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ s) ≤ ↑↑ν' (t ∩ s) + ↑↑ν (t ∩ s)
[PROOFSTEP]
rw [← restrict_eq_self μ (inter_subset_right _ _), ← restrict_eq_self ν (inter_subset_right _ _)]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑(restrict μ s) (t ∩ s) ≤ ↑↑ν' (t ∩ s) + ↑↑(restrict ν s) (t ∩ s)
[PROOFSTEP]
apply h_ν'_in _ (h_meas_t.inter h_meas_s)
[GOAL]
case a.refine'_1.refine'_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t \ s) ≤ ↑↑(ν' + ν + restrict ⊤ sᶜ) (t \ s)
[PROOFSTEP]
rw [add_apply, restrict_apply (h_meas_t.diff h_meas_s), diff_eq, inter_assoc, inter_self, ← add_apply]
[GOAL]
case a.refine'_1.refine'_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑μ (t ∩ sᶜ) ≤ ↑↑(ν' + ν + ⊤) (t ∩ sᶜ)
[PROOFSTEP]
have h_mu_le_add_top : μ ≤ ν' + ν + ⊤ := by simp only [add_top, le_top]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ μ ≤ ν' + ν + ⊤
[PROOFSTEP]
simp only [add_top, le_top]
[GOAL]
case a.refine'_1.refine'_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
h_mu_le_add_top : μ ≤ ν' + ν + ⊤
⊢ ↑↑μ (t ∩ sᶜ) ≤ ↑↑(ν' + ν + ⊤) (t ∩ sᶜ)
[PROOFSTEP]
exact Measure.le_iff'.1 h_mu_le_add_top _
[GOAL]
case a.refine'_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
⊢ (fun μ => restrict μ s) (ν' + restrict ⊤ sᶜ) = restrict ν' s
[PROOFSTEP]
ext1 t h_meas_t
[GOAL]
case a.refine'_2.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
ν' : Measure α
h_ν'_in : restrict μ s ≤ ν' + restrict ν s
t : Set α
h_meas_t : MeasurableSet t
⊢ ↑↑((fun μ => restrict μ s) (ν' + restrict ⊤ sᶜ)) t = ↑↑(restrict ν' s) t
[PROOFSTEP]
simp [restrict_apply h_meas_t, restrict_apply (h_meas_t.inter h_meas_s), inter_assoc]
[GOAL]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ sInf {d | restrict μ s ≤ d + restrict ν s} ≤ sInf ((fun μ => restrict μ s) '' {d | μ ≤ d + ν})
[PROOFSTEP]
refine' sInf_le_sInf_of_forall_exists_le _
[GOAL]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
⊢ ∀ (x : Measure α),
    x ∈ (fun μ => restrict μ s) '' {d | μ ≤ d + ν} → ∃ y, y ∈ {d | restrict μ s ≤ d + restrict ν s} ∧ y ≤ x
[PROOFSTEP]
refine' ball_image_iff.2 fun t h_t_in => ⟨t.restrict s, _, le_rfl⟩
[GOAL]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
t : Measure α
h_t_in : t ∈ {d | μ ≤ d + ν}
⊢ restrict t s ∈ {d | restrict μ s ≤ d + restrict ν s}
[PROOFSTEP]
rw [Set.mem_setOf_eq, ← restrict_add]
[GOAL]
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : Set.Nonempty {d | μ ≤ d + ν}
t : Measure α
h_t_in : t ∈ {d | μ ≤ d + ν}
⊢ restrict μ s ≤ restrict (t + ν) s
[PROOFSTEP]
exact restrict_mono Subset.rfl h_t_in
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_le : restrict μ s ≤ restrict ν s
h_meas_s : MeasurableSet s
⊢ ↑↑(μ - ν) s = 0
[PROOFSTEP]
rw [← restrict_apply_self, restrict_sub_eq_restrict_sub_restrict, sub_eq_zero_of_le]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_le : restrict μ s ≤ restrict ν s
h_meas_s : MeasurableSet s
⊢ ↑↑0 s = 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_le : restrict μ s ≤ restrict ν s
h_meas_s : MeasurableSet s
⊢ restrict μ s ≤ restrict ν s
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_le : restrict μ s ≤ restrict ν s
h_meas_s : MeasurableSet s
⊢ MeasurableSet s
[PROOFSTEP]
simp [*]


[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
s : ℕ → Set (NullMeasurableSpace α)
hs : ∀ (i : ℕ), (fun s => ∃ t, MeasurableSet t ∧ s =ᵐ[μ] t) (s i)
⊢ (fun s => ∃ t, MeasurableSet t ∧ s =ᵐ[μ] t) (⋃ (i : ℕ), s i)
[PROOFSTEP]
choose t htm hts using hs
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
s : ℕ → Set (NullMeasurableSpace α)
t : ℕ → Set α
htm : ∀ (i : ℕ), MeasurableSet (t i)
hts : ∀ (i : ℕ), s i =ᵐ[μ] t i
⊢ ∃ t, MeasurableSet t ∧ ⋃ (i : ℕ), s i =ᵐ[μ] t
[PROOFSTEP]
exact ⟨⋃ i, t i, MeasurableSet.iUnion htm, EventuallyEq.countable_iUnion hts⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → NullMeasurableSet t
⊢ NullMeasurableSet (⋃₀ s)
[PROOFSTEP]
rw [sUnion_eq_biUnion]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
s : Set (Set α)
hs : Set.Countable s
h : ∀ (t : Set α), t ∈ s → NullMeasurableSet t
⊢ NullMeasurableSet (⋃ (i : Set α) (_ : i ∈ s), i)
[PROOFSTEP]
exact MeasurableSet.biUnion hs h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
[PROOFSTEP]
rcases h with ⟨t, htm, hst⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
[PROOFSTEP]
refine' ⟨t ∪ toMeasurable μ (s \ t), _, htm.union (measurableSet_toMeasurable _ _), _⟩
[GOAL]
case intro.intro.refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ t ∪ toMeasurable μ (s \ t) ⊇ s
[PROOFSTEP]
exact diff_subset_iff.1 (subset_toMeasurable _ _)
[GOAL]
case intro.intro.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s
[PROOFSTEP]
have : toMeasurable μ (s \ t) =ᵐ[μ] (∅ : Set α) := by simp [ae_le_set.1 hst.le]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ toMeasurable μ (s \ t) =ᵐ[μ] ∅
[PROOFSTEP]
simp [ae_le_set.1 hst.le]
[GOAL]
case intro.intro.refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
this : toMeasurable μ (s \ t) =ᵐ[μ] ∅
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s
[PROOFSTEP]
simpa only [union_empty] using hst.symm.union this
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ toMeasurable μ s =ᵐ[μ] s
[PROOFSTEP]
rw [toMeasurable_def, dif_pos]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ Exists.choose ?hc =ᵐ[μ] s
case hc
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : NullMeasurableSet s
⊢ ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
[PROOFSTEP]
exact (exists_measurable_superset_ae_eq h).choose_spec.snd.2
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i)
hd : Pairwise (AEDisjoint μ on s)
⊢ ∃ t, (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᵐ[μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
[PROOFSTEP]
choose t ht_sub htm ht_eq using fun i => exists_measurable_subset_ae_eq (h i)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i)
hd : Pairwise (AEDisjoint μ on s)
t : ι → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᵐ[μ] s i
⊢ ∃ t, (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᵐ[μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
[PROOFSTEP]
rcases exists_null_pairwise_disjoint_diff hd with ⟨u, hum, hu₀, hud⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i)
hd : Pairwise (AEDisjoint μ on s)
t : ι → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᵐ[μ] s i
u : ι → Set α
hum : ∀ (i : ι), MeasurableSet (u i)
hu₀ : ∀ (i : ι), ↑↑μ (u i) = 0
hud : Pairwise (Disjoint on fun i => s i \ u i)
⊢ ∃ t, (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᵐ[μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
[PROOFSTEP]
exact
  ⟨fun i => t i \ u i, fun i => (diff_subset _ _).trans (ht_sub _), fun i =>
    (ht_eq _).symm.trans (diff_null_ae_eq_self (hu₀ i)).symm, fun i => (htm i).diff (hum i),
    hud.mono fun i j h => h.mono (diff_subset_diff_left (ht_sub i)) (diff_subset_diff_left (ht_sub j))⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ↑↑μ (⋃ (i : ι), f i) = ∑' (i : ι), ↑↑μ (f i)
[PROOFSTEP]
rw [measure_eq_extend (MeasurableSet.iUnion h), extend_iUnion MeasurableSet.empty _ MeasurableSet.iUnion _ hn h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∑' (i : ι), extend (fun t _ht => ↑↑μ t) (f i) = ∑' (i : ι), ↑↑μ (f i)
[PROOFSTEP]
simp [measure_eq_extend, h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ↑↑μ ∅ = 0
[PROOFSTEP]
exact μ.empty
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0✝ : MeasurableSpace α
μ✝ : Measure α
s t : Set α
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → ↑↑μ (⋃ (i : ℕ), f i) = ∑' (i : ℕ), ↑↑μ (f i)
[PROOFSTEP]
exact μ.m_iUnion
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i)
⊢ ↑↑μ (⋃ (i : ι), f i) = ∑' (i : ι), ↑↑μ (f i)
[PROOFSTEP]
rcases exists_subordinate_pairwise_disjoint h hd with ⟨t, _ht_sub, ht_eq, htm, htd⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i)
t : ι → Set α
_ht_sub : ∀ (i : ι), t i ⊆ f i
ht_eq : ∀ (i : ι), f i =ᵐ[μ] t i
htm : ∀ (i : ι), MeasurableSet (t i)
htd : Pairwise (Disjoint on t)
⊢ ↑↑μ (⋃ (i : ι), f i) = ∑' (i : ι), ↑↑μ (f i)
[PROOFSTEP]
calc
  μ (⋃ i, f i) = μ (⋃ i, t i) := measure_congr (EventuallyEq.countable_iUnion ht_eq)
  _ = ∑' i, μ (t i) := (measure_iUnion htd htm)
  _ = ∑' i, μ (f i) := tsum_congr fun i => measure_congr (ht_eq _).symm
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ ↑↑μ (s ∪ t) = ↑↑μ s + ↑↑μ t
[PROOFSTEP]
rw [union_eq_iUnion, measure_iUnion₀, tsum_fintype, Fintype.sum_bool, cond, cond]
[GOAL]
case hd
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ Pairwise (AEDisjoint μ on fun b => bif b then s else t)
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ ∀ (i : Bool), NullMeasurableSet (bif i then s else t)
[PROOFSTEP]
exacts [(pairwise_on_bool AEDisjoint.symmetric).2 hd, fun b => Bool.casesOn b ht hs]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) = ↑↑μ s
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) ≤ ↑↑μ s
[PROOFSTEP]
rcases exists_measurable_superset μ s with ⟨s', hsub, hs'm, hs'⟩
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
s' : Set α
hsub : s ⊆ s'
hs'm : MeasurableSet s'
hs' : ↑↑μ s' = ↑↑μ s
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) ≤ ↑↑μ s
[PROOFSTEP]
replace hs'm : NullMeasurableSet s' μ := hs'm.nullMeasurableSet
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
s' : Set α
hsub : s ⊆ s'
hs' : ↑↑μ s' = ↑↑μ s
hs'm : NullMeasurableSet s'
⊢ ↑↑μ (s ∩ t) + ↑↑μ (s \ t) ≤ ↑↑μ s
[PROOFSTEP]
calc
  μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t) :=
    add_le_add (measure_mono <| inter_subset_inter_left _ hsub) (measure_mono <| diff_subset_diff_left hsub)
  _ = μ (s' ∩ t ∪ s' \ t) :=
    (measure_union₀_aux (hs'm.inter ht) (hs'm.diff ht) <| (@disjoint_inf_sdiff _ s' t _).aedisjoint).symm
  _ = μ s' := (congr_arg μ (inter_union_diff _ _))
  _ = μ s := hs'
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ s ≤ ↑↑μ (s ∩ t) + ↑↑μ (s \ t)
[PROOFSTEP]
calc
  μ s = μ (s ∩ t ∪ s \ t) := by rw [inter_union_diff]
  _ ≤ μ (s ∩ t) + μ (s \ t) := measure_union_le _ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ s = ↑↑μ (s ∩ t ∪ s \ t)
[PROOFSTEP]
rw [inter_union_diff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
ht : NullMeasurableSet t
⊢ ↑↑μ (s ∪ t) + ↑↑μ (s ∩ t) = ↑↑μ s + ↑↑μ t
[PROOFSTEP]
rw [← measure_inter_add_diff₀ (s ∪ t) ht, union_inter_cancel_right, union_diff_right, ← measure_inter_add_diff₀ s ht,
  add_comm, ← add_assoc, add_right_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
hs : NullMeasurableSet s
t : Set α
⊢ ↑↑μ (s ∪ t) + ↑↑μ (s ∩ t) = ↑↑μ s + ↑↑μ t
[PROOFSTEP]
rw [union_comm, inter_comm, measure_union_add_inter₀ t hs, add_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ ↑↑μ (s ∪ t) = ↑↑μ s + ↑↑μ t
[PROOFSTEP]
rw [← measure_union_add_inter₀ s ht, hd, add_zero]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
hd : AEDisjoint μ s t
⊢ ↑↑μ (s ∪ t) = ↑↑μ s + ↑↑μ t
[PROOFSTEP]
rw [union_comm, measure_union₀ hs (AEDisjoint.symm hd), add_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t s : Set α
hs : NullMeasurableSet s
⊢ ↑↑μ s + ↑↑μ sᶜ = ↑↑μ univ
[PROOFSTEP]
rw [← measure_union₀' hs aedisjoint_compl_right, union_compl_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝ : MeasurableSingletonClass (NullMeasurableSpace α)
s : Finset α
⊢ NullMeasurableSet ↑s
[PROOFSTEP]
apply Finset.measurableSet
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : α → β
hf : NullMeasurable f
hg : f =ᵐ[μ] g
s : Set β
hs : MeasurableSet s
x : α
hx : f x = g x
⊢ x ∈ f ⁻¹' s ↔ x ∈ g ⁻¹' s
[PROOFSTEP]
rw [mem_preimage, mem_preimage, hx]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s t : Set α
x✝ : MeasurableSpace α
μ : Measure α
⊢ OuterMeasure.trim ↑μ = ↑μ
[PROOFSTEP]
refine' le_antisymm (fun s => _) (@OuterMeasure.le_trim (NullMeasurableSpace α μ) _ _)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s✝ t : Set α
x✝ : MeasurableSpace α
μ : Measure α
s : Set (NullMeasurableSpace α)
⊢ ↑(OuterMeasure.trim ↑μ) s ≤ ↑↑μ s
[PROOFSTEP]
rw [@OuterMeasure.trim_eq_iInf (NullMeasurableSpace α μ) _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s✝ t : Set α
x✝ : MeasurableSpace α
μ : Measure α
s : Set (NullMeasurableSpace α)
⊢ ⨅ (t : Set (NullMeasurableSpace α)) (_ : s ⊆ t) (_ : MeasurableSet t), ↑↑μ t ≤ ↑↑μ s
[PROOFSTEP]
have : ∀ s, μ.toOuterMeasure s = μ s := by simp only [forall_const]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s✝ t : Set α
x✝ : MeasurableSpace α
μ : Measure α
s : Set (NullMeasurableSpace α)
⊢ ∀ (s : Set α), ↑↑μ s = ↑↑μ s
[PROOFSTEP]
simp only [forall_const]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s✝ t : Set α
x✝ : MeasurableSpace α
μ : Measure α
s : Set (NullMeasurableSpace α)
this : ∀ (s : Set α), ↑↑μ s = ↑↑μ s
⊢ ⨅ (t : Set (NullMeasurableSpace α)) (_ : s ⊆ t) (_ : MeasurableSet t), ↑↑μ t ≤ ↑↑μ s
[PROOFSTEP]
rw [this, measure_eq_iInf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s✝ t : Set α
x✝ : MeasurableSpace α
μ : Measure α
s : Set (NullMeasurableSpace α)
this : ∀ (s : Set α), ↑↑μ s = ↑↑μ s
⊢ ⨅ (t : Set (NullMeasurableSpace α)) (_ : s ⊆ t) (_ : MeasurableSet t), ↑↑μ t ≤
    ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑↑μ t
[PROOFSTEP]
apply iInf₂_mono
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ✝ : Measure α
s✝ t : Set α
x✝ : MeasurableSpace α
μ : Measure α
s : Set (NullMeasurableSpace α)
this : ∀ (s : Set α), ↑↑μ s = ↑↑μ s
⊢ ∀ (i : Set (NullMeasurableSpace α)), s ⊆ i → ⨅ (_ : MeasurableSet i), ↑↑μ i ≤ ⨅ (_ : MeasurableSet i), ↑↑μ i
[PROOFSTEP]
exact fun t _ht => iInf_mono' fun h => ⟨MeasurableSet.nullMeasurableSet h, le_rfl⟩