awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
rw :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) - (μ.singularPart ν).real Set.univ
rw₁ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) -
      ENNReal.toReal ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
rw₂ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν =
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)).toReal
rw₃ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ENNReal.toReal ((μ - μ.singularPart ν : (a : Set α) → ℝ≥0∞) Set.univ)
rw₄ :
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) Set.univ)
rw₅ : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real Set.univ
rw₆ : Eq (α := ℝ) (∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α) in Set.univ, (μ.rnDeriv ν x).toReal ∂ν)
rw₇ rw₈ : Eq (α := ℝ) (∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν)
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ - (μ.singularPart ν).real Set.univ

Tactic:
rw [measureReal_def, measureReal_def,
    ← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _),
    ← Measure.sub_apply .univ (Measure.singularPart_le μ ν), Measure.measure_sub_singularPart,
    ← measureReal_def, ← Measure.setIntegral_toReal_rnDeriv_eq_withDensity, setIntegral_univ]

Premises used: MeasureTheory.Measure.measure_sub_singularPart, Set.univ, MeasureTheory.measure_ne_top, MeasureTheory.Measure.singularPart_le, MeasureTheory.Measure.sub_apply, ENNReal.toReal_sub_of_le, MeasureTheory.measureReal_def, MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity, MeasureTheory.setIntegral_univ, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hμν : μ ≪ ν
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ

Tactic:
(rnDeriv_withDensity_left ?_ ?_).symm.trans ?_

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.symm, MeasureTheory.Measure.rnDeriv_withDensity_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hμν : μ ≪ ν
refine_1 : AEMeasurable (μ.rnDeriv ν) κ
refine_2 : ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ∞
refine_3 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ

Tactic:
refine (rnDeriv_withDensity_left ?_ ?_).symm.trans ?_

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.symm, MeasureTheory.Measure.rnDeriv_withDensity_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hμν : μ ≪ ν
⊢ AEMeasurable (μ.rnDeriv ν) κ

Tactic:
(Measure.measurable_rnDeriv _ _).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hμν : μ ≪ ν
⊢ AEMeasurable (μ.rnDeriv ν) κ

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

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ∞

Tactic:
rnDeriv_ne_top _ _

Premises used: MeasureTheory.Measure.rnDeriv_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ∞

Tactic:
exact rnDeriv_ne_top _ _

Premises used: MeasureTheory.Measure.rnDeriv_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hμν : μ ≪ ν
refine_3 refine_3₁ : μ.rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ

Tactic:
rw [Measure.withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hνκ : ν ≪ κ
⊢ Measurable (μ.rnDeriv ν)

Tactic:
obtain ⟨h_meas, h_sing, hμν⟩ := Measure.haveLebesgueDecomposition_spec μ ν

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
obtain ⟨h_meas, h_sing, hμν⟩ := Measure.haveLebesgueDecomposition_spec μ ν

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
⊢ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
obtain ⟨h_meas, h_sing, hμν⟩ := Measure.haveLebesgueDecomposition_spec μ ν

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h :
  ∀ (x : α)
    (hx1 :
      (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
        ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x)
    (hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x)
    (hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x), (μ.rnDeriv ν * ν.rnDeriv κ) x = μ.rnDeriv κ x
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᶠ[ae ν] μ.rnDeriv κ

Tactic:
filter_upwards [hνκ <| Measure.rnDeriv_add' (μ.singularPart ν) (ν.withDensity (μ.rnDeriv ν)) κ,
    hνκ <| Measure.rnDeriv_withDensity_left_of_absolutelyContinuous hνκ h_meas.aemeasurable,
    Measure.rnDeriv_eq_zero_of_mutuallySingular h_sing hνκ] with x hx1 hx2 hx3

Premises used: MeasureTheory.Measure.withDensity, Measurable.aemeasurable, MeasureTheory.Measure.rnDeriv, MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular, MeasureTheory.Measure.singularPart, MeasureTheory.Measure.rnDeriv_withDensity_left_of_absolutelyContinuous, MeasureTheory.Measure.rnDeriv_add'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
h : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = μ.rnDeriv κ x

Tactic:
nth_rw 2 [hμν]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
h : (μ.rnDeriv ν * ν.rnDeriv κ) x = ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
h₁ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
h₂ : (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x
h₃ : μ.rnDeriv ν x * ν.rnDeriv κ x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x
h₄ : μ.rnDeriv ν x * ν.rnDeriv κ x = 0 x + μ.rnDeriv ν x * ν.rnDeriv κ x
h₅ : μ.rnDeriv ν x * ν.rnDeriv κ x = 0 + μ.rnDeriv ν x * ν.rnDeriv κ x
h₆ h₇ : μ.rnDeriv ν x * ν.rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x

Tactic:
rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]

Premises used: Pi.mul_apply, Pi.zero_apply, zero_add, Pi.add_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst : SigmaFinite ν
⊢ μ.rnDeriv ν ≤ᶠ[ae ν] 1

Tactic:
ae_le_of_forall_setLIntegral_le_of_sigmaFinite (μ.measurable_rnDeriv ν) fun s _ _ ↦ ?_

Premises used: MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst : SigmaFinite ν
refine :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ ∫⁻ (x : α) in s, 1 x ∂ν
⊢ μ.rnDeriv ν ≤ᶠ[ae ν] 1

Tactic:
refine ae_le_of_forall_setLIntegral_le_of_sigmaFinite (μ.measurable_rnDeriv ν) fun s _ _ ↦ ?_

Premises used: MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
simp : ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ (ν : (a : Set α) → ℝ≥0∞) s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ ∫⁻ (x : α) in s, 1 x ∂ν

Tactic:
simp only [Pi.one_apply, MeasureTheory.setLIntegral_one]

Premises used: Pi.one_apply, MeasureTheory.setLIntegral_one
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ (ν : (a : Set α) → ℝ≥0∞) s

Tactic:
(Measure.setLIntegral_rnDeriv_le s).trans (hμν s)

Premises used: LE.le.trans, MeasureTheory.Measure.setLIntegral_rnDeriv_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst : SigmaFinite ν
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ (ν : (a : Set α) → ℝ≥0∞) s

Tactic:
exact (Measure.setLIntegral_rnDeriv_le s).trans (hμν s)

Premises used: LE.le.trans, MeasureTheory.Measure.setLIntegral_rnDeriv_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv ν ≤ᶠ[ae ν] 1 ↔ μ ≤ ν

Tactic:
⟨fun h s ↦ ?_, fun h ↦ rnDeriv_le_one_of_le h⟩

Premises used: Iff.intro, MeasureTheory.Measure.rnDeriv_le_one_of_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
refine :
  ∀ (h : μ.rnDeriv ν ≤ᶠ[ae ν] 1) (s : Set α),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.rnDeriv ν ≤ᶠ[ae ν] 1 ↔ μ ≤ ν

Tactic:
refine ⟨fun h s ↦ ?_, fun h ↦ rnDeriv_le_one_of_le h⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν ≤ᶠ[ae ν] 1
s : Set α
rw : ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν ≤ ∫⁻ (x : α) in s, 1 ∂ν
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_apply', ← setLIntegral_one]

Premises used: MeasureTheory.setLIntegral_one, MeasureTheory.withDensity_apply', MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν ≤ᶠ[ae ν] 1
s : Set α
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν ≤ ∫⁻ (x : α) in s, 1 ∂ν

Tactic:
setLIntegral_mono_ae aemeasurable_const (h.mono fun _ hh _ ↦ hh)

Premises used: MeasureTheory.setLIntegral_mono_ae, Filter.Eventually.mono, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν ≤ᶠ[ae ν] 1
s : Set α
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν ≤ ∫⁻ (x : α) in s, 1 ∂ν

Tactic:
exact setLIntegral_mono_ae aemeasurable_const (h.mono fun _ hh _ ↦ hh)

Premises used: MeasureTheory.setLIntegral_mono_ae, Filter.Eventually.mono, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 1 ↔ μ = ν

Tactic:
⟨fun h ↦ ?_, fun h ↦ h ▸ ν.rnDeriv_self⟩

Premises used: Eq.rec, Iff.intro, Eq.symm, MeasureTheory.Measure.rnDeriv_self
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
refine : ∀ (h : μ.rnDeriv ν =ᶠ[ae ν] 1), μ = ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 1 ↔ μ = ν

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ ν.rnDeriv_self⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν =ᶠ[ae ν] 1
rw : ν.withDensity (μ.rnDeriv ν) = ν
rw₁ : ν.withDensity 1 = ν
rw₂ rw₃ : ν = ν
⊢ μ = ν

Tactic:
rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_congr_ae h, withDensity_one]

Premises used: MeasureTheory.withDensity_one, MeasureTheory.withDensity_congr_ae, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ μ ≪ ν + μ

Tactic:
have hν_ac : μ ≪ ν + μ := rfl.absolutelyContinuous.add_right' _
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hν_ac : μ ≪ ν + μ
h :
  ∀ (a : α) (h1 : (ν + μ).rnDeriv μ a = (ν.rnDeriv μ + μ.rnDeriv μ) a) (h2 : μ.rnDeriv μ a = 1)
    (h3 : (μ.rnDeriv (ν + μ))⁻¹ a = (ν + μ).rnDeriv μ a), μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹
⊢ μ.rnDeriv (ν + μ) =ᶠ[ae μ] fun (x : α) ↦ (ν.rnDeriv μ x + 1)⁻¹

Tactic:
filter_upwards [ν.rnDeriv_add' μ μ, μ.rnDeriv_self, Measure.inv_rnDeriv hν_ac] with a h1 h2 h3

Premises used: MeasureTheory.Measure.inv_rnDeriv, MeasureTheory.Measure.rnDeriv_self, MeasureTheory.Measure.rnDeriv_add'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hν_ac : μ ≪ ν + μ
a : α
h1 : (ν + μ).rnDeriv μ a = (ν.rnDeriv μ + μ.rnDeriv μ) a
h2 : μ.rnDeriv μ a = 1
h3 : (μ.rnDeriv (ν + μ))⁻¹ a = (ν + μ).rnDeriv μ a
⊢ μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹

Tactic:
rw [Pi.inv_apply, h1, Pi.add_apply, h2, inv_eq_iff_eq_inv] at h3

Premises used: Pi.add_apply, inv_eq_iff_eq_inv, Pi.inv_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hν_ac : μ ≪ ν + μ
a : α
h1 : (ν + μ).rnDeriv μ a = (ν.rnDeriv μ + μ.rnDeriv μ) a
h2 : μ.rnDeriv μ a = 1
h3 : μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹
h h₁ : (ν.rnDeriv μ a + 1)⁻¹ = (ν.rnDeriv μ a + 1)⁻¹
⊢ μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹

Tactic:
rw [h3]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)

Tactic:
have h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν) :=
    (ae_add_measure_iff.mp (μ.rnDeriv_add' ν (μ + ν))).2
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
⊢ ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x

Tactic:
have h_one_add := (ae_add_measure_iff.mp (μ + ν).rnDeriv_self).2
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
h :
  ∀ (a : α) (h4 : (μ + ν).rnDeriv (μ + ν) a = (μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)) a)
    (h5 : (μ + ν).rnDeriv (μ + ν) a = 1) (h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹),
    μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹

Tactic:
filter_upwards [h_add, h_one_add, rnDeriv_add_self ν μ] with a h4 h5 h6

Premises used: MeasureTheory.Measure.rnDeriv_add_self
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
a : α
h4 : (μ + ν).rnDeriv (μ + ν) a = (μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a

Tactic:
rw [h5, Pi.add_apply] at h4

Premises used: Pi.add_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
a : α
h4 : (μ + ν).rnDeriv (μ + ν) a = (μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
h4₁ : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
⊢ (μ + ν).rnDeriv (μ + ν) a = 1

Tactic:
rw [h5, Pi.add_apply] at h4

Premises used: Pi.add_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
a : α
h4 : (μ + ν).rnDeriv (μ + ν) a = (μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
h4₁ : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
h5₁ : (μ + ν).rnDeriv (μ + ν) a = 1
⊢ ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹

Tactic:
rw [h5, Pi.add_apply] at h4

Premises used: Pi.add_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
a : α
h4 : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
h : μ.rnDeriv (μ + ν) a = μ.rnDeriv (μ + ν) a + (μ.rnDeriv ν a + 1)⁻¹ - (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹

Tactic:
nth_rw 1 [h4, h6]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
a : α
h4 : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = μ.rnDeriv (μ + ν) a + (μ.rnDeriv ν a + 1)⁻¹ - (μ.rnDeriv ν a + 1)⁻¹

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
⊢ μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹

Tactic:
have : (μ.rnDeriv (μ + ν)) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹ := by
    filter_upwards [h_add, h_one_add, rnDeriv_add_self ν μ] with a h4 h5 h6
    rw [h5, Pi.add_apply] at h4
    nth_rw 1 [h4, h6]
    simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
this : μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
h :
  ∀ (a : α) (ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹) (ha_lt_top : μ.rnDeriv ν a < ∞),
    μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
⊢ μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ μ.rnDeriv ν x / (μ.rnDeriv ν x + 1)

Tactic:
filter_upwards [this, μ.rnDeriv_lt_top ν] with a ha ha_lt_top

Premises used: MeasureTheory.Measure.rnDeriv_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᶠ[ae ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x
this : μ.rnDeriv (μ + ν) =ᶠ[ae ν] fun (x : α) ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
h : 1 - (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)

Tactic:
rw [ha, div_eq_mul_inv]

Premises used: div_eq_mul_inv