-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem rnDeriv_smul_right (ν μ : Measure α) [IsFiniteMeasure ν]
    [ν.HaveLebesgueDecomposition μ] {r : ℝ≥0} (hr : r ≠ 0) :
    ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ

Proof state:
case hf
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)

Tactic:
exact (measurable_rnDeriv _ _).aemeasurable

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ

Tactic:
refine (absolutelyContinuous_smul <| ENNReal.coe_ne_zero.2 hr).ae_le
  (?_ : ν.rnDeriv (r • μ) =ᵐ[r • μ] r⁻¹ • ν.rnDeriv μ)

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ

Proof state:
case hg
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)

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

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (↑r • μ).withDensity (ν.rnDeriv (↑r • μ)) = (↑r • μ).withDensity (↑r⁻¹ • ν.rnDeriv μ)

Tactic:
rw [withDensity_smul _ (measurable_rnDeriv _ _)]

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (↑r • μ).withDensity (ν.rnDeriv (↑r • μ)) = ↑r⁻¹ • (↑r • μ).withDensity (ν.rnDeriv μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (↑r • μ).withDensity (ν.rnDeriv (↑r • μ)) = ↑r⁻¹ • (↑r • μ).withDensity (ν.rnDeriv μ)

Tactic:
suffices ν.singularPart (r • μ) + withDensity (r • μ) (rnDeriv ν (r • μ))
    = ν.singularPart (r • μ) + r⁻¹ • withDensity (r • μ) (rnDeriv ν μ) by
  rwa [add_right_inj] at this

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff]

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)

case hf
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)

case hg
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)

case hfi
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ∫⁻ (x : α), ν.rnDeriv (r • μ) x ∂r • μ ≠ ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν = ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)

Tactic:
exact ν.haveLebesgueDecomposition_add μ

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)

Tactic:
rw [← ν.haveLebesgueDecomposition_add (r • μ), singularPart_smul_right _ _ _ hr,
  ENNReal.smul_def r, withDensity_smul_measure, ← ENNReal.smul_def, ← smul_assoc,
  smul_eq_mul, inv_mul_cancel₀ hr, one_smul]

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν = ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
this :
  ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
⊢ (↑r • μ).withDensity (ν.rnDeriv (↑r • μ)) = ↑r⁻¹ • (↑r • μ).withDensity (ν.rnDeriv μ)

Tactic:
rwa [add_right_inj] at this

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)

case hf
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)

case hg
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)

case hfi
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ∫⁻ (x : α), ν.rnDeriv (r • μ) x ∂r • μ ≠ ⊤

Tactic:
rotate_left

Result:
case hf
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)

case hg
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)

case hfi
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ∫⁻ (x : α), ν.rnDeriv (r • μ) x ∂r • μ ≠ ⊤

α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)

Tactic:
simp_rw [ENNReal.smul_def]

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (↑r • μ).withDensity (ν.rnDeriv (↑r • μ)) = (↑r • μ).withDensity (↑r⁻¹ • ν.rnDeriv μ)

Proof state:
case hfi
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ∫⁻ (x : α), ν.rnDeriv (r • μ) x ∂r • μ ≠ ⊤

Tactic:
exact (lintegral_rnDeriv_lt_top ν _).ne

Result:
no goals