-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
/-- Radon-Nikodym derivative of a sum of two measures.
See also `rnDeriv_add'`, which requires sigma-finite `ν₁`, `ν₂` and `μ`. -/
lemma rnDeriv_add (ν₁ ν₂ μ : Measure α) [IsFiniteMeasure ν₁] [IsFiniteMeasure ν₂]
    [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ]
    [(ν₁ + ν₂).HaveLebesgueDecomposition μ] :
    (ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ

Proof state:
case hfi
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), (ν₁ + ν₂).rnDeriv μ x ∂μ ≠ ⊤

Tactic:
exact (lintegral_rnDeriv_lt_top (ν₁ + ν₂) μ).ne

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Tactic:
suffices (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ)
    = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ) by
  rwa [add_right_inj] at this

Result:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Proof state:
case hg
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ

Tactic:
exact ((measurable_rnDeriv _ _).add (measurable_rnDeriv _ _)).aemeasurable

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
this :
  (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Tactic:
rwa [add_right_inj] at this

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Tactic:
rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
  withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
  add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
  ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff]

Result:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

case hf
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ

case hg
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ

case hfi
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), (ν₁ + ν₂).rnDeriv μ x ∂μ ≠ ⊤

Proof state:
case hf
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ

Tactic:
exact (measurable_rnDeriv _ _).aemeasurable

Result:
no goals