awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.MeasurableEquiv (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν : Measure A
g_1 : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Eq (α := Measure A)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) (g * g')⁻¹ : G) x) μ)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x)
      (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x) μ))
have rw : Eq (α := Measure A)
  (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) (g * g')⁻¹ : G) x) μ)
  (map
    ((fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) ∘ fun (x : A) ↦
      HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x)
    μ)
Tactic: rw [map_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.MeasurableEquiv (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν : Measure A
g_1 : G
g g' : Gᵈᵐᵃ
μ : Measure A
rw :
  Eq (α := Measure A)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) (g * g')⁻¹ : G) x) μ)
    (map
      ((fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) ∘ fun (x : A) ↦
        HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x)
      μ)
⊢ Eq (α := Measure A)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) (g * g')⁻¹ : G) x) μ)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x)
      (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x) μ))
have hg : Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x
Tactic: rw [map_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.MeasurableEquiv (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν : Measure A
g_1 : G
g g' : Gᵈᵐᵃ
μ : Measure A
rw :
  Eq (α := Measure A)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) (g * g')⁻¹ : G) x) μ)
    (map
      ((fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) ∘ fun (x : A) ↦
        HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x)
      μ)
hg : Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x
⊢ Eq (α := Measure A)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) (g * g')⁻¹ : G) x) μ)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x)
      (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x) μ))
have hf : Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x
Tactic: rw [map_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.MeasurableEquiv (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν_1 : Measure A
g_1 : G
g : Gᵈᵐᵃ
μ ν : Measure A
⊢ map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) (μ + ν) =
    HAdd.hAdd (α := Measure A)
      (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) μ)
      (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) ν)
have hf : Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x
Tactic: rw [Measure.map_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.MeasurableEquiv (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
⊢ Eq (α := ENNReal) ((g • μ : (a : Set A) → ENNReal) s : ENNReal)
    ((μ : (a : Set A) → ENNReal) (HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g : G) s) : ENNReal)
have refine : Eq (α := ENNReal)
  ((μ : (a : Set A) → ENNReal)
      ((⇑(MeasurableEquiv.smul (G := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G)) : (a : A) → A) ⁻¹' s) :
    ENNReal)
  ((μ : (a : Set A) → ENNReal) (HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g : G) s) : ENNReal)
Tactic: refine ((MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)).map_apply _).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.MeasurableEquiv (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ : Measure A
g : Gᵈᵐᵃ
s : Set A
⊢ Eq (α := ENNReal)
    ((μ : (a : Set A) → ENNReal)
        ((⇑(MeasurableEquiv.smul (G := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G)) : (a : A) → A) ⁻¹'
          s) :
      ENNReal)
    ((μ : (a : Set A) → ENNReal) (HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g : G) s) : ENNReal)
have h : (⇑(MeasurableEquiv.smul (G := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G)) : (a : A) → A) ⁻¹' s =
  HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g : G) s
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
this : μ.singularPart ν = 0
| μ
have rw : ν.withDensity (μ.rnDeriv ν)
Tactic: rw [haveLebesgueDecomposition_add μ ν, this, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
this : μ.singularPart ν = 0
⊢ ν.withDensity (μ.rnDeriv ν) = μ
have conv_rhs : ν.withDensity (μ.rnDeriv ν) = μ
Tactic: conv_rhs => rw [haveLebesgueDecomposition_add μ ν, this, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
this : μ.singularPart ν = 0
conv_rhs : ν.withDensity (μ.rnDeriv ν) = μ
⊢ ν.withDensity (μ.rnDeriv ν) = μ
have conv_rhs₁ : ν.withDensity (μ.rnDeriv ν) = ν.withDensity (μ.rnDeriv ν)
Tactic: conv_rhs => rw [haveLebesgueDecomposition_add μ ν, this, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
⊢ ν.withDensity (μ.rnDeriv ν) = μ
have suffices : μ.singularPart ν = 0
Tactic: suffices μ.singularPart ν = 0 by
    conv_rhs => rw [haveLebesgueDecomposition_add μ ν, this, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂μ, 0 < μ.rnDeriv ν x
have rw : ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0 → 0 < μ.rnDeriv ν x
Tactic: rw [← Measure.withDensity_rnDeriv_eq _ _ hμν,
    ae_withDensity_iff (Measure.measurable_rnDeriv _ _), Measure.withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
inst_1 : SigmaFinite μ
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂μ, 0 < ν.rnDeriv μ x
have refine : {x : α | (fun (x : α) ↦ 0 < ν.rnDeriv μ x) x} ∈ ae (μ.withDensity (ν.rnDeriv μ))
Tactic: refine (absolutelyContinuous_withDensity_rnDeriv hμν).ae_le ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
inst_1 : SigmaFinite μ
hμν : μ ≪ ν
⊢ {x : α | (fun (x : α) ↦ 0 < ν.rnDeriv μ x) x} ∈ ae (μ.withDensity (ν.rnDeriv μ))
have h : ∀ (x : α) (hx : 0 < (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x)
  (hx2 : (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x = ν.rnDeriv μ x), 0 < ν.rnDeriv μ x
Tactic: filter_upwards [Measure.rnDeriv_pos (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)),
    (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)).ae_le
    (Measure.rnDeriv_withDensity μ (Measure.measurable_rnDeriv ν μ))] with x hx hx2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
| (μ.withDensity f).rnDeriv ν
have rw : ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν
Tactic: rw [μ.haveLebesgueDecomposition_add ν, add_comm, withDensity_add_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν
have conv_rhs : ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν]
  ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν
Tactic: conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm, withDensity_add_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν
have this : SigmaFinite ((μ.singularPart ν).withDensity f)
Tactic: have : SigmaFinite ((μ.singularPart ν).withDensity f) :=
    SigmaFinite.withDensity_of_ne_top (ae_mono (Measure.singularPart_le _ _) hf_ne_top)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : SigmaFinite ((μ.singularPart ν).withDensity f)
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν]
    ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν
have this₁ : SigmaFinite ((ν.withDensity (μ.rnDeriv ν)).withDensity f)
Tactic: have : SigmaFinite ((ν.withDensity (μ.rnDeriv ν)).withDensity f) :=
    SigmaFinite.withDensity_of_ne_top (ae_mono (Measure.withDensity_rnDeriv_le _ _) hf_ne_top)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
| μ.rnDeriv (ν.withDensity f)
have rw : (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
Tactic: rw [μ.haveLebesgueDecomposition_add ν, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)
have conv_rhs : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν]
  (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
Tactic: conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
have hν_ac : ν ≪ ν.withDensity f
Tactic: have hν_ac : ν ≪ ν.withDensity f := withDensity_absolutelyContinuous' hf hf_ne_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
hν_ac : ν ≪ ν.withDensity f
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
have refine : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)]
  (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
Tactic: refine hν_ac.ae_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
hν_ac : ν ≪ ν.withDensity f
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
have this : SigmaFinite (ν.withDensity f)
Tactic: have : SigmaFinite (ν.withDensity f) := SigmaFinite.withDensity_of_ne_top hf_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
hν_ac : ν ≪ ν.withDensity f
this : SigmaFinite (ν.withDensity f)
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae (ν.withDensity f)]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
have refine : μ.singularPart ν ⟂ₘ ν.withDensity f
Tactic: refine (rnDeriv_add_of_mutuallySingular _ _ _ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ (μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ.rnDeriv ν x
have refine_1 : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ f x * μ.rnDeriv ν x) ν
Tactic: refine (Measure.eq_rnDeriv₀ ?_ Measure.MutuallySingular.zero_left ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
refine_1 : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ f x * μ.rnDeriv ν x) ν
⊢ (μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ.rnDeriv ν x
have refine_2 : μ.withDensity f = 0 + ν.withDensity fun (x : α) ↦ f x * μ.rnDeriv ν x
Tactic: refine (Measure.eq_rnDeriv₀ ?_ Measure.MutuallySingular.zero_left ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ μ.withDensity f = 0 + ν.withDensity fun (x : α) ↦ f x * μ.rnDeriv ν x
have refine_2 : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((0 + ν.withDensity fun (x : α) ↦ f x * μ.rnDeriv ν x : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((0 + ν.withDensity fun (x : α) ↦ f x * μ.rnDeriv ν x : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have refine_2 : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
Tactic: rw [zero_add, withDensity_apply _ hs, withDensity_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
| ∫⁻ (a : α) in s, f a ∂μ
have rw : ∫⁻ (a : α) in s, f a ∂ν.withDensity (μ.rnDeriv ν)
Tactic: rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
have refine_2 : ∫⁻ (a : α) in s, f a ∂ν.withDensity (μ.rnDeriv ν) = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
Tactic: conv_lhs => rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂ν.withDensity (μ.rnDeriv ν) = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
have refine_2 : ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
Tactic: rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
refine_2 : ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
⊢ ∫⁻ (a : α) in s, f a ∂ν.withDensity (μ.rnDeriv ν) = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
have refine_2₁ : ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
Tactic: rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
refine_2 : ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
refine_2₁ : ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
⊢ ∫⁻ (a : α) in s, f a ∂ν.withDensity (μ.rnDeriv ν) = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
have rw : AEMeasurable (μ.rnDeriv ν) (ν.restrict s)
Tactic: rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (μ.rnDeriv ν * f) a ∂ν = ∫⁻ (a : α) in s, f a * μ.rnDeriv ν a ∂ν
have refine_2 : ∀ (x : α), (μ.rnDeriv ν * f) x = f x * μ.rnDeriv ν x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
x : α
⊢ (μ.rnDeriv ν * f) x = f x * μ.rnDeriv ν x
have refine_2 : (f * μ.rnDeriv ν) x = f x * μ.rnDeriv ν x
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
have refine_2 : ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x < ∞
Tactic: refine ae_restrict_of_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
⊢ (μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ.rnDeriv ν x
have hμ'ν : μ' ≪ ν
Tactic: have hμ'ν : μ' ≪ ν := withDensity_absolutelyContinuous _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ'.rnDeriv ν x
⊢ (μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ.rnDeriv ν x
have h1 : μ'.rnDeriv ν =ᶠ[ae ν] μ.rnDeriv ν
Tactic: have h1 : μ'.rnDeriv ν =ᵐ[ν] μ.rnDeriv ν :=
    Measure.rnDeriv_withDensity _ (Measure.measurable_rnDeriv _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ'.rnDeriv ν x
h1 : μ'.rnDeriv ν =ᶠ[ae ν] μ.rnDeriv ν
⊢ (μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ.rnDeriv ν x
have h2 : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν
Tactic: have h2 : (μ'.withDensity f).rnDeriv ν =ᵐ[ν] (μ.withDensity f).rnDeriv ν := by
    exact rnDeriv_withDensity_withDensity_rnDeriv_left μ ν hf_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ'.rnDeriv ν x
h1 : μ'.rnDeriv ν =ᶠ[ae ν] μ.rnDeriv ν
h2 : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν
⊢ (μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ f x * μ.rnDeriv ν x
have h₁ : ∀ (x : α) (hx : (μ'.withDensity f).rnDeriv ν x = f x * μ'.rnDeriv ν x) (hx1 : μ'.rnDeriv ν x = μ.rnDeriv ν x)
  (hx2 : (μ'.withDensity f).rnDeriv ν x = (μ.withDensity f).rnDeriv ν x),
  (μ.withDensity f).rnDeriv ν x = f x * μ.rnDeriv ν x
Tactic: filter_upwards [h, h1, h2] with x hx hx1 hx2