α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
⊢ s = singularPart μ ν
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + withDensity ν f
⊢ s = singularPart μ ν
haveI : HaveLebesgueDecomposition μ ν := ⟨⟨⟨s, f⟩, hf, hs, hadd⟩⟩
case intro.intro
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hsing : singularPart μ ν ⟂ₘ ν
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ s = singularPart μ ν
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
⊢ s = singularPart μ ν
obtain ⟨hmeas, hsing, hadd'⟩ := haveLebesgueDecomposition_spec μ ν
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
⊢ s = singularPart μ ν
case intro.intro
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hsing : singularPart μ ν ⟂ₘ ν
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
⊢ s = singularPart μ ν
obtain ⟨⟨S, hS₁, hS₂, hS₃⟩, ⟨T, hT₁, hT₂, hT₃⟩⟩ := hs, hsing
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
⊢ s = singularPart μ ν
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
⊢ s = singularPart μ ν
rw [hadd'] at hadd
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
⊢ s = singularPart μ ν
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
⊢ s = singularPart μ ν
have hνinter : ν ((S ∩ T)ᶜ) = 0 := by
  rw [compl_inter]
  refine' nonpos_iff_eq_zero.1 (le_trans (measure_union_le _ _) _)
  rw [hT₃, hS₃, add_zero]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
⊢ s = singularPart μ ν
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
⊢ s = singularPart μ ν
have heq : s.restrict ((S ∩ T)ᶜ) = (μ.singularPart ν).restrict ((S ∩ T)ᶜ) := by
  ext1 A hA
  have hf : ν.withDensity f (A ∩ (S ∩ T)ᶜ) = 0 := by
    refine' withDensity_absolutelyContinuous ν _ _
    rw [← nonpos_iff_eq_zero]
    exact hνinter ▸ measure_mono (inter_subset_right _ _)
  have hrn : ν.withDensity (μ.rnDeriv ν) (A ∩ (S ∩ T)ᶜ) = 0 := by
    refine' withDensity_absolutelyContinuous ν _ _
    rw [← nonpos_iff_eq_zero]
    exact hνinter ▸ measure_mono (inter_subset_right _ _)
  rw [restrict_apply hA, restrict_apply hA, ← add_zero (s (A ∩ (S ∩ T)ᶜ)), ← hf, ← add_apply, ←
    hadd, add_apply, hrn, add_zero]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
heq' : ∀ (A : Set α), MeasurableSet A → ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
⊢ s = singularPart μ ν
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
⊢ s = singularPart μ ν
have heq' : ∀ A : Set α, MeasurableSet A → s A = s.restrict ((S ∩ T)ᶜ) A := by
  intro A hA
  have hsinter : s (A ∩ (S ∩ T)) = 0 := by
    rw [← nonpos_iff_eq_zero]
    exact hS₂ ▸ measure_mono ((inter_subset_right _ _).trans (inter_subset_left _ _))
  rw [restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hsinter]
case intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
heq' : ∀ (A : Set α), MeasurableSet A → ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
A : Set α
hA : MeasurableSet A
⊢ ↑↑s A = ↑↑(singularPart μ ν) A
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
heq' : ∀ (A : Set α), MeasurableSet A → ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
⊢ s = singularPart μ ν
ext1 A hA
case intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
heq' : ∀ (A : Set α), MeasurableSet A → ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
A : Set α
hA : MeasurableSet A
hμinter : ↑↑(singularPart μ ν) (A ∩ (S ∩ T)) = 0
⊢ ↑↑s A = ↑↑(singularPart μ ν) A
case intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
heq' : ∀ (A : Set α), MeasurableSet A → ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
A : Set α
hA : MeasurableSet A
⊢ ↑↑s A = ↑↑(singularPart μ ν) A
have hμinter : μ.singularPart ν (A ∩ (S ∩ T)) = 0 := by
  rw [← nonpos_iff_eq_zero]
  exact hT₂ ▸ measure_mono ((inter_subset_right _ _).trans (inter_subset_right _ _))
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
heq' : ∀ (A : Set α), MeasurableSet A → ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
A : Set α
hA : MeasurableSet A
hμinter : ↑↑(singularPart μ ν) (A ∩ (S ∩ T)) = 0
⊢ ↑↑s A = ↑↑(singularPart μ ν) A
rw [heq' A hA, heq, restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hμinter]
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
⊢ ↑↑ν (Sᶜ ∪ Tᶜ) = 0
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
⊢ ↑↑ν ((S ∩ T)ᶜ) = 0
rw [compl_inter]
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
⊢ ↑↑ν (Sᶜ) + ↑↑ν (Tᶜ) ≤ 0
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
⊢ ↑↑ν (Sᶜ ∪ Tᶜ) = 0
refine' nonpos_iff_eq_zero.1 (le_trans (measure_union_le _ _) _)
no goals
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
⊢ ↑↑ν (Sᶜ) + ↑↑ν (Tᶜ) ≤ 0
rw [hT₃, hS₃, add_zero]
case h
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
⊢ ↑↑(restrict s ((S ∩ T)ᶜ)) A = ↑↑(restrict (singularPart μ ν) ((S ∩ T)ᶜ)) A
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
⊢ restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
ext1 A hA
case h
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf✝ : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
hf : ↑↑(withDensity ν f) (A ∩ (S ∩ T)ᶜ) = 0
⊢ ↑↑(restrict s ((S ∩ T)ᶜ)) A = ↑↑(restrict (singularPart μ ν) ((S ∩ T)ᶜ)) A
case h
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
⊢ ↑↑(restrict s ((S ∩ T)ᶜ)) A = ↑↑(restrict (singularPart μ ν) ((S ∩ T)ᶜ)) A
have hf : ν.withDensity f (A ∩ (S ∩ T)ᶜ) = 0 := by
  refine' withDensity_absolutelyContinuous ν _ _
  rw [← nonpos_iff_eq_zero]
  exact hνinter ▸ measure_mono (inter_subset_right _ _)
case h
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf✝ : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
hf : ↑↑(withDensity ν f) (A ∩ (S ∩ T)ᶜ) = 0
hrn : ↑↑(withDensity ν (rnDeriv μ ν)) (A ∩ (S ∩ T)ᶜ) = 0
⊢ ↑↑(restrict s ((S ∩ T)ᶜ)) A = ↑↑(restrict (singularPart μ ν) ((S ∩ T)ᶜ)) A
case h
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf✝ : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
hf : ↑↑(withDensity ν f) (A ∩ (S ∩ T)ᶜ) = 0
⊢ ↑↑(restrict s ((S ∩ T)ᶜ)) A = ↑↑(restrict (singularPart μ ν) ((S ∩ T)ᶜ)) A
have hrn : ν.withDensity (μ.rnDeriv ν) (A ∩ (S ∩ T)ᶜ) = 0 := by
  refine' withDensity_absolutelyContinuous ν _ _
  rw [← nonpos_iff_eq_zero]
  exact hνinter ▸ measure_mono (inter_subset_right _ _)
no goals
case h
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf✝ : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
hf : ↑↑(withDensity ν f) (A ∩ (S ∩ T)ᶜ) = 0
hrn : ↑↑(withDensity ν (rnDeriv μ ν)) (A ∩ (S ∩ T)ᶜ) = 0
⊢ ↑↑(restrict s ((S ∩ T)ᶜ)) A = ↑↑(restrict (singularPart μ ν) ((S ∩ T)ᶜ)) A
rw [restrict_apply hA, restrict_apply hA, ← add_zero (s (A ∩ (S ∩ T)ᶜ)), ← hf, ← add_apply, ←
  hadd, add_apply, hrn, add_zero]
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
⊢ ↑↑ν (A ∩ (S ∩ T)ᶜ) = 0
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
⊢ ↑↑(withDensity ν f) (A ∩ (S ∩ T)ᶜ) = 0
refine' withDensity_absolutelyContinuous ν _ _
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
⊢ ↑↑ν (A ∩ (S ∩ T)ᶜ) ≤ 0
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
⊢ ↑↑ν (A ∩ (S ∩ T)ᶜ) = 0
rw [← nonpos_iff_eq_zero]
no goals
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
⊢ ↑↑ν (A ∩ (S ∩ T)ᶜ) ≤ 0
exact hνinter ▸ measure_mono (inter_subset_right _ _)
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf✝ : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
hf : ↑↑(withDensity ν f) (A ∩ (S ∩ T)ᶜ) = 0
⊢ ↑↑ν (A ∩ (S ∩ T)ᶜ) = 0
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf✝ : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
hf : ↑↑(withDensity ν f) (A ∩ (S ∩ T)ᶜ) = 0
⊢ ↑↑(withDensity ν (rnDeriv μ ν)) (A ∩ (S ∩ T)ᶜ) = 0
refine' withDensity_absolutelyContinuous ν _ _
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf✝ : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
hf : ↑↑(withDensity ν f) (A ∩ (S ∩ T)ᶜ) = 0
⊢ ↑↑ν (A ∩ (S ∩ T)ᶜ) ≤ 0
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf✝ : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
hf : ↑↑(withDensity ν f) (A ∩ (S ∩ T)ᶜ) = 0
⊢ ↑↑ν (A ∩ (S ∩ T)ᶜ) = 0
rw [← nonpos_iff_eq_zero]
no goals
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf✝ : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
A : Set α
hA : MeasurableSet A
hf : ↑↑(withDensity ν f) (A ∩ (S ∩ T)ᶜ) = 0
⊢ ↑↑ν (A ∩ (S ∩ T)ᶜ) ≤ 0
exact hνinter ▸ measure_mono (inter_subset_right _ _)
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
A : Set α
hA : MeasurableSet A
⊢ ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
⊢ ∀ (A : Set α), MeasurableSet A → ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
intro A hA
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
A : Set α
hA : MeasurableSet A
hsinter : ↑↑s (A ∩ (S ∩ T)) = 0
⊢ ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
A : Set α
hA : MeasurableSet A
⊢ ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
have hsinter : s (A ∩ (S ∩ T)) = 0 := by
  rw [← nonpos_iff_eq_zero]
  exact hS₂ ▸ measure_mono ((inter_subset_right _ _).trans (inter_subset_left _ _))
no goals
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
A : Set α
hA : MeasurableSet A
hsinter : ↑↑s (A ∩ (S ∩ T)) = 0
⊢ ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
rw [restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hsinter]
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
A : Set α
hA : MeasurableSet A
⊢ ↑↑s (A ∩ (S ∩ T)) ≤ 0
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
A : Set α
hA : MeasurableSet A
⊢ ↑↑s (A ∩ (S ∩ T)) = 0
rw [← nonpos_iff_eq_zero]
no goals
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
A : Set α
hA : MeasurableSet A
⊢ ↑↑s (A ∩ (S ∩ T)) ≤ 0
exact hS₂ ▸ measure_mono ((inter_subset_right _ _).trans (inter_subset_left _ _))
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
heq' : ∀ (A : Set α), MeasurableSet A → ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
A : Set α
hA : MeasurableSet A
⊢ ↑↑(singularPart μ ν) (A ∩ (S ∩ T)) ≤ 0
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
heq' : ∀ (A : Set α), MeasurableSet A → ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
A : Set α
hA : MeasurableSet A
⊢ ↑↑(singularPart μ ν) (A ∩ (S ∩ T)) = 0
rw [← nonpos_iff_eq_zero]
no goals
α : Type u_1
β : Type ?u.39986
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : singularPart μ ν + withDensity ν (rnDeriv μ ν) = s + withDensity ν f
this : HaveLebesgueDecomposition μ ν
hmeas : Measurable (rnDeriv μ ν)
hadd' : μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑s S = 0
hS₃ : ↑↑ν (Sᶜ) = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : ↑↑(singularPart μ ν) T = 0
hT₃ : ↑↑ν (Tᶜ) = 0
hνinter : ↑↑ν ((S ∩ T)ᶜ) = 0
heq : restrict s ((S ∩ T)ᶜ) = restrict (singularPart μ ν) ((S ∩ T)ᶜ)
heq' : ∀ (A : Set α), MeasurableSet A → ↑↑s A = ↑↑(restrict s ((S ∩ T)ᶜ)) A
A : Set α
hA : MeasurableSet A
⊢ ↑↑(singularPart μ ν) (A ∩ (S ∩ T)) ≤ 0
exact hT₂ ▸ measure_mono ((inter_subset_right _ _).trans (inter_subset_right _ _))