[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 [*]
