case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
⊢ withDensity ν (rnDeriv μ ν) = μ
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
⊢ withDensity ν (rnDeriv μ ν) = μ
obtain ⟨_, ⟨E, hE₁, hE₂, hE₃⟩, hadd⟩ := haveLebesgueDecomposition_spec μ ν
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
this : singularPart μ ν = 0
⊢ withDensity ν (rnDeriv μ ν) = μ
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
⊢ withDensity ν (rnDeriv μ ν) = μ
have : singularPart μ ν = 0 := by
  refine' le_antisymm (fun A (_ : MeasurableSet A) => _) (Measure.zero_le _)
  suffices singularPart μ ν Set.univ = 0 by
    rw [Measure.coe_zero, Pi.zero_apply, ← this]
    exact measure_mono (Set.subset_univ _)
  rw [← measure_add_measure_compl hE₁, hE₂, zero_add]
  have : (singularPart μ ν + ν.withDensity (rnDeriv μ ν)) (Eᶜ) = μ (Eᶜ) := by rw [← hadd]
  rw [Measure.coe_add, Pi.add_apply, h hE₃] at this
  exact (add_eq_zero_iff.1 this).1
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
this : singularPart μ ν = 0
⊢ withDensity ν (rnDeriv μ ν) = μ
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
this : singularPart μ ν = 0
⊢ withDensity ν (rnDeriv μ ν) = μ
rw [this, zero_add] at hadd
no goals
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
this : singularPart μ ν = 0
⊢ withDensity ν (rnDeriv μ ν) = μ
exact hadd.symm
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
⊢ ↑↑(singularPart μ ν) A ≤ ↑↑0 A
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
⊢ singularPart μ ν = 0
refine' le_antisymm (fun A (_ : MeasurableSet A) => _) (Measure.zero_le _)
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
⊢ ↑↑(singularPart μ ν) Set.univ = 0
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
⊢ ↑↑(singularPart μ ν) A ≤ ↑↑0 A
suffices singularPart μ ν Set.univ = 0 by
  rw [Measure.coe_zero, Pi.zero_apply, ← this]
  exact measure_mono (Set.subset_univ _)
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
⊢ ↑↑(singularPart μ ν) (Eᶜ) = 0
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
⊢ ↑↑(singularPart μ ν) Set.univ = 0
rw [← measure_add_measure_compl hE₁, hE₂, zero_add]
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
this : ↑↑(singularPart μ ν + withDensity ν (rnDeriv μ ν)) (Eᶜ) = ↑↑μ (Eᶜ)
⊢ ↑↑(singularPart μ ν) (Eᶜ) = 0
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
⊢ ↑↑(singularPart μ ν) (Eᶜ) = 0
have : (singularPart μ ν + ν.withDensity (rnDeriv μ ν)) (Eᶜ) = μ (Eᶜ) := by rw [← hadd]
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
this : ↑↑(singularPart μ ν) (Eᶜ) + ↑↑(withDensity ν (rnDeriv μ ν)) (Eᶜ) = 0
⊢ ↑↑(singularPart μ ν) (Eᶜ) = 0
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
this : ↑↑(singularPart μ ν + withDensity ν (rnDeriv μ ν)) (Eᶜ) = ↑↑μ (Eᶜ)
⊢ ↑↑(singularPart μ ν) (Eᶜ) = 0
rw [Measure.coe_add, Pi.add_apply, h hE₃] at this
no goals
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
this : ↑↑(singularPart μ ν) (Eᶜ) + ↑↑(withDensity ν (rnDeriv μ ν)) (Eᶜ) = 0
⊢ ↑↑(singularPart μ ν) (Eᶜ) = 0
exact (add_eq_zero_iff.1 this).1
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
this : ↑↑(singularPart μ ν) Set.univ = 0
⊢ ↑↑(singularPart μ ν) A ≤ ↑↑(singularPart μ ν) Set.univ
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
this : ↑↑(singularPart μ ν) Set.univ = 0
⊢ ↑↑(singularPart μ ν) A ≤ ↑↑0 A
rw [Measure.coe_zero, Pi.zero_apply, ← this]
no goals
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
this : ↑↑(singularPart μ ν) Set.univ = 0
⊢ ↑↑(singularPart μ ν) A ≤ ↑↑(singularPart μ ν) Set.univ
exact measure_mono (Set.subset_univ _)
no goals
α : Type u_1
β : Type ?u.14
m : MeasurableSpace α
μ ν : Measure α
inst✝ : HaveLebesgueDecomposition μ ν
h : μ ≪ ν
left✝ : Measurable (rnDeriv μ ν)
hadd : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
E : Set α
hE₁ : MeasurableSet E
hE₂ : ↑↑(singularPart μ ν) E = 0
hE₃ : ↑↑ν (Eᶜ) = 0
A : Set α
x✝ : MeasurableSet A
⊢ ↑↑(singularPart μ ν + withDensity ν (rnDeriv μ ν)) (Eᶜ) = ↑↑μ (Eᶜ)
rw [← hadd]