awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
s : Set β
hs : MeasurableSet s
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ (fun (x : α) ↦ rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) x = μ.rnDeriv ν x) x}
            x →
          Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ x ∈ f ⁻¹' s → μ.rnDeriv ν x = rnDeriv (m := mβ) (map f μ) (map f ν) (f x)) x} x}
      a
h₁ h₂ :
  ∀ (a : α) (ha : rnDeriv (m := mβ) (map f μ) (map f ν) (f a) = μ.rnDeriv ν a),
    a ∈ f ⁻¹' s → μ.rnDeriv ν a = rnDeriv (m := mβ) (map f μ) (map f ν) (f a)
⊢ ∀ᵐ (x : α) ∂ν, x ∈ f ⁻¹' s → μ.rnDeriv ν x = rnDeriv (m := mβ) (map f μ) (map f ν) (f x)

Tactic:
filter_upwards [hf.rnDeriv_map μ ν] with a ha _ using ha.symm

Premises used: MeasurableEmbedding.rnDeriv_map
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
rw : map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν))
| map f μ

Tactic:
rw [μ.haveLebesgueDecomposition_add ν]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
conv_lhs :
  map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
⊢ map f μ =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))

Tactic:
conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
rw :
  HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν))) =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
rw₁ rw₂ :
  HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν))) =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν)) (map f (ν.withDensity (μ.rnDeriv ν)))
⊢ map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))

Tactic:
rw [Measure.map_add _ _ hf.measurable, ← hf.map_withDensity_rnDeriv μ ν]

Premises used: MeasureTheory.Measure.map_add, MeasurableEmbedding.measurable, MeasurableEmbedding.map_withDensity_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ map f μ =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))

Tactic:
have h_add : μ.map f = (μ.singularPart ν).map f
      + (ν.map f).withDensity ((μ.map f).rnDeriv (ν.map f)) := by
    conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]
    rw [Measure.map_add _ _ hf.measurable, ← hf.map_withDensity_rnDeriv μ ν]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add :
  map f μ =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
⊢ Eq (α := Measure β) (singularPart (map f μ) (map f ν)) (map f (μ.singularPart ν))

Tactic:
(Measure.eq_singularPart (Measure.measurable_rnDeriv _ _) ?_ h_add).symm

Premises used: Eq.symm, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add :
  map f μ =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
refine : @MutuallySingular _ mβ (map f (μ.singularPart ν)) (map f ν)
⊢ Eq (α := Measure β) (singularPart (map f μ) (map f ν)) (map f (μ.singularPart ν))

Tactic:
refine (Measure.eq_singularPart (Measure.measurable_rnDeriv _ _) ?_ h_add).symm

Premises used: Eq.symm, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add :
  map f μ =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
⊢ @MutuallySingular _ mβ (map f (μ.singularPart ν)) (map f ν)

Tactic:
hf.mutuallySingular_map (μ.mutuallySingular_singularPart ν)

Premises used: MeasurableEmbedding.mutuallySingular_map, MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
h_add :
  map f μ =
    HAdd.hAdd (α := Measure β) (map f (μ.singularPart ν))
      (withDensity (map f ν) (rnDeriv (m := mβ) (map f μ) (map f ν)))
⊢ @MutuallySingular _ mβ (map f (μ.singularPart ν)) (map f ν)

Tactic:
exact hf.mutuallySingular_map (μ.mutuallySingular_singularPart ν)

Premises used: MeasurableEmbedding.mutuallySingular_map, MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
nth_rw : ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂ν.withDensity (μ.rnDeriv ν)
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂μ

Tactic:
nth_rw 2 [← withDensity_rnDeriv_eq μ ν hμν]

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
rw : ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α), (μ.rnDeriv ν * f) a ∂ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [lintegral_withDensity_eq_lintegral_mul₀ (measurable_rnDeriv μ ν).aemeasurable hf]

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α), (μ.rnDeriv ν * f) a ∂ν

Tactic:
simp only [Pi.mul_apply]

Premises used: Pi.mul_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
nth_rw : ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂ν.withDensity (μ.rnDeriv ν)
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
nth_rw 2 [← Measure.withDensity_rnDeriv_eq μ ν hμν]

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
rw : ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [setLIntegral_withDensity_eq_lintegral_mul₀ (measurable_rnDeriv μ ν).aemeasurable hf hs]

Premises used: Measurable.aemeasurable, MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν

Tactic:
simp only [Pi.mul_apply]

Premises used: Pi.mul_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
nth_rw :
  Integrable.{u_4, u_3} (ε := E) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal • f x) ν ↔
    Integrable f (ν.withDensity (μ.rnDeriv ν))
⊢ Integrable.{u_4, u_3} (ε := E) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f μ

Tactic:
nth_rw 2 [← withDensity_rnDeriv_eq μ ν hμν]

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
rw rw₁ : Integrable f (ν.withDensity (μ.rnDeriv ν)) ↔ Integrable f (ν.withDensity (μ.rnDeriv ν))
⊢ Integrable.{u_4, u_3} (ε := E) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal • f x) ν ↔
    Integrable f (ν.withDensity (μ.rnDeriv ν))

Tactic:
rw [← integrable_withDensity_iff_integrable_smul' (E := E)
    (measurable_rnDeriv μ ν) (rnDeriv_lt_top μ ν)]

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.integrable_withDensity_iff_integrable_smul', MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite μ
hμν : μ ≪ ν
f : α → ℝ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * f x) ν ↔ Integrable f μ

Tactic:
integrable_rnDeriv_smul_iff hμν

Premises used: MeasureTheory.integrable_rnDeriv_smul_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
rw : Eq.{u_4 + 1} (α := E) (∫ (x : α), f x ∂ν.withDensity (μ.rnDeriv ν)) (∫ (x : α), f x ∂μ)
rw₁ rw₂ : Eq.{u_4 + 1} (α := E) (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂μ)
⊢ Eq.{u_4 + 1} (α := E) (∫ (x : α), (μ.rnDeriv ν x).toReal • f x ∂ν) (∫ (x : α), f x ∂μ)

Tactic:
rw [← integral_withDensity_eq_integral_toReal_smul (measurable_rnDeriv _ _) (rnDeriv_lt_top _ _),
    withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, integral_withDensity_eq_integral_toReal_smul, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite μ
hμν : μ ≪ ν
f : α → ℝ
⊢ Eq (α := ℝ) (∫ (x : α), (μ.rnDeriv ν x).toReal * f x ∂ν) (∫ (x : α), f x ∂μ)

Tactic:
integral_rnDeriv_smul hμν

Premises used: MeasureTheory.integral_rnDeriv_smul
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
hf : Measurable (μ.rnDeriv ν)
hf_top : ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
hs₁ : MeasurableSet s
⊢ Eq.{u_4 + 1} (α := E) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν) (∫ (x : α) in s, f x ∂μ)

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

Premises used: setIntegral_withDensity_eq_setIntegral_toReal_smul, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ Measurable (μ.rnDeriv ν)

Tactic:
measurable_rnDeriv _ _

Premises used: MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

Tactic:
ae_restrict_of_ae (rnDeriv_lt_top _ _)

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
hs
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : μ.HaveLebesgueDecomposition ν
inst_3 : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ Measurable (μ.rnDeriv ν)

Tactic:
exacts [measurable_rnDeriv _ _, ae_restrict_of_ae (rnDeriv_lt_top _ _), hs]

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.ae_restrict_of_ae, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : SigmaFinite μ
hμν : μ ≪ ν
f : α → ℝ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal * f x ∂ν) (∫ (x : α) in s, f x ∂μ)

Tactic:
setIntegral_rnDeriv_smul hμν hs

Premises used: MeasureTheory.setIntegral_rnDeriv_smul
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SigmaFinite μ
f : α → E
inst_3 : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
hf : Measurable (μ.rnDeriv ν)
hf_top : ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
⊢ Eq.{u_4 + 1} (α := E) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν) (∫ (x : α) in s, f x ∂μ)

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

Premises used: setIntegral_withDensity_eq_setIntegral_toReal_smul', MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SigmaFinite μ
f : α → E
inst_3 : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
⊢ Measurable (μ.rnDeriv ν)

Tactic:
measurable_rnDeriv _ _

Premises used: MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SigmaFinite μ
f : α → E
inst_3 : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

Tactic:
ae_restrict_of_ae (rnDeriv_lt_top _ _)

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SigmaFinite μ
f : α → E
inst_3 : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
⊢ Measurable (μ.rnDeriv ν)

Tactic:
exacts [measurable_rnDeriv _ _, ae_restrict_of_ae (rnDeriv_lt_top _ _)]

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.ae_restrict_of_ae, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
f : α → ℝ
s : Set α
⊢ Eq (α := ℝ) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal * f x ∂ν) (∫ (x : α) in s, f x ∂μ)

Tactic:
setIntegral_rnDeriv_smul' hμν s

Premises used: MeasureTheory.setIntegral_rnDeriv_smul'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : ν₁.HaveLebesgueDecomposition μ
inst_6 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ Measurable (ν₁.rnDeriv μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : ν₁.HaveLebesgueDecomposition μ
inst_6 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ Measurable (ν₂.rnDeriv μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : ν₁.HaveLebesgueDecomposition μ
inst_6 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
rw : ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ) ∗ₘ μ.withDensity (ν₂.rnDeriv μ)
rw₁ : ν₁ ∗ₘ ν₂ = ν₁ ∗ₘ μ.withDensity (ν₂.rnDeriv μ)
rw₂ rw₃ : ν₁ ∗ₘ ν₂ = ν₁ ∗ₘ ν₂
⊢ ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)

Tactic:
rw [← mconv_withDensity_eq_mlconvolution (by fun_prop) (by fun_prop),
    withDensity_rnDeriv_eq _ _ hν₁, withDensity_rnDeriv_eq _ _ hν₂]

Premises used: MeasureTheory.mconv_withDensity_eq_mlconvolution, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : ν₁.HaveLebesgueDecomposition μ
inst_6 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ Measurable (0, ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ).2

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : ν₁.HaveLebesgueDecomposition μ
inst_6 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ (0, ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ).1 ⟂ₘ μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : ν₁.HaveLebesgueDecomposition μ
inst_6 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ ν₁ ∗ₘ ν₂ = (0, ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ).1 + μ.withDensity (0, ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ).2

Tactic:
simpa using mconv_eq_withDensity_mlconvolution_rnDeriv hν₁ hν₂

Premises used: MeasureTheory.mconv_eq_withDensity_mlconvolution_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : IsFiniteMeasure ν₁
inst_6 : IsFiniteMeasure ν₂
inst_7 : ν₁.HaveLebesgueDecomposition μ
inst_8 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ

Tactic:
have := HaveLebesgueDecomposition.mconv hν₁ hν₂
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : IsFiniteMeasure ν₁
inst_6 : IsFiniteMeasure ν₂
inst_7 : ν₁.HaveLebesgueDecomposition μ
inst_8 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ AEMeasurable ((ν₁ ∗ₘ ν₂).rnDeriv μ) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : IsFiniteMeasure ν₁
inst_6 : IsFiniteMeasure ν₂
inst_7 : ν₁.HaveLebesgueDecomposition μ
inst_8 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ AEMeasurable (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : IsFiniteMeasure ν₁
inst_6 : IsFiniteMeasure ν₂
inst_7 : ν₁.HaveLebesgueDecomposition μ
inst_8 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
rw : ∫⁻ (x : G), (ν₁ ∗ₘ ν₂).rnDeriv μ x ∂μ ≠ ∞
⊢ (ν₁ ∗ₘ ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff (by fun_prop) (by fun_prop),
    withDensity_rnDeriv_eq _ _ (mconv_absolutelyContinuous hν₂),
    mconv_eq_withDensity_mlconvolution_rnDeriv hν₁ hν₂]

Premises used: MeasureTheory.mconv_eq_withDensity_mlconvolution_rnDeriv, MeasureTheory.withDensity_eq_iff, MeasureTheory.Measure.mconv_absolutelyContinuous, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
ν₁ ν₂ : Measure G
inst_5 : IsFiniteMeasure ν₁
inst_6 : IsFiniteMeasure ν₂
inst_7 : ν₁.HaveLebesgueDecomposition μ
inst_8 : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : G), (ν₁ ∗ₘ ν₂).rnDeriv μ x ∂μ ≠ ∞

Tactic:
(lintegral_rnDeriv_lt_top (ν₁ ∗ₘ ν₂) μ).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, MeasureTheory.Measure.mconv, LT.lt.ne