awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
⊢ (ν.withDensity (μ.rnDeriv ν)).withDensity ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)⁻¹ = ν
have conv : (ν.withDensity (μ.rnDeriv ν)).withDensity (μ.rnDeriv ν)⁻¹ = ν
Tactic: conv in ((ν.withDensity (μ.rnDeriv ν)).rnDeriv ν)⁻¹ => rw [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 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 < μ.rnDeriv ν x) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv ν x ≠ 0) x} x}
    a
Tactic: filter_upwards [hνμ.ae_le (rnDeriv_pos hμν)] with x hx using hx.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 < μ.rnDeriv ν x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv ν x ≠ 0) x} x}
      a
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0
have h₁ : ∀ (a : α), 0 < μ.rnDeriv ν a → μ.rnDeriv ν a ≠ 0
Tactic: filter_upwards [hνμ.ae_le (rnDeriv_pos hμν)] with x hx using hx.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : ν.HaveLebesgueDecomposition μ
inst_2 : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity fun (x : α) ↦ (μ.rnDeriv ν x)⁻¹) = ν
have rw : ν = ν
Tactic: rw [withDensity_inv_same (measurable_rnDeriv _ _)
    (by filter_upwards [hνμ.ae_le (rnDeriv_pos hμν)] with x hx using hx.ne')
    (rnDeriv_ne_top _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
this :
  (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] ν.rnDeriv μ
have refine : (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
Tactic: refine (this.1.trans (Filter.EventuallyEq.trans ?_ this.2.symm))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] ν.rnDeriv μ
have suffices : (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
  ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
Tactic: suffices (μ.rnDeriv ν)⁻¹ =ᵐ[μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹
      ∧ ν.rnDeriv μ =ᵐ[μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ by
    refine (this.1.trans (Filter.EventuallyEq.trans ?_ this.2.symm))
    exact Measure.inv_rnDeriv_aux (absolutelyContinuous_withDensity_rnDeriv hμν)
      (withDensity_absolutelyContinuous _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
have left : (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
left : (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧
    ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
have right : ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ (μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹
have h : ∀ (x : α) (hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x),
  (μ.rnDeriv ν)⁻¹ x = (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ x
Tactic: filter_upwards [rnDeriv_withDensity_rnDeriv hμν] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x = μ.rnDeriv ν x
⊢ (μ.rnDeriv ν)⁻¹ x = (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ x
have h : μ.rnDeriv ν x = μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) x
Tactic: simp only [Pi.inv_apply, inv_inj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ (ν.rnDeriv μ)⁻¹ =ᶠ[ae μ] μ.rnDeriv ν
have h : ∀ (x : α) (hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x), (ν.rnDeriv μ)⁻¹ x = μ.rnDeriv ν x
Tactic: filter_upwards [inv_rnDeriv hμν] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (a : α) ∂ν, μ.rnDeriv ν a ≠ 0 → p a
have rw : (∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x) ∧
  ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
Tactic: rw [ν.haveLebesgueDecomposition_add μ, ae_add_measure_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ (∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x) ∧
    ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
have left : ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
left : ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
⊢ (∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x) ∧
    ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
have right : ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
have left : ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x ≠ 0 → p x
Tactic: rw [← ν.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x ≠ 0 → p x
have this : ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0
Tactic: have : ∀ᵐ x ∂(ν.singularPart μ), μ.rnDeriv ν x = 0 := μ.rnDeriv_eq_zero_ae_singularPart ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
this : ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x ≠ 0 → p x
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv ν x = 0) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv ν x ≠ 0 → p x) x} x}
    a
Tactic: filter_upwards [this] with x hx h_absurd using absurd hx h_absurd
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
this : ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv ν x = 0) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv ν x ≠ 0 → p x) x} x}
      a
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x ≠ 0 → p x
have h₂ : ∀ (a : α), μ.rnDeriv ν a = 0 → μ.rnDeriv ν a ≠ 0 → p a
Tactic: filter_upwards [this] with x hx h_absurd using absurd hx h_absurd
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
have h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
Tactic: have h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ := withDensity_absolutelyContinuous _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
⊢ ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
have right : ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv ν x ≠ 0 → p x
Tactic: rw [← ν.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
⊢ ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv ν x ≠ 0 → p x
have right : ∀ᵐ (x : α) ∂μ, μ.rnDeriv ν x ≠ 0 → p x
Tactic: suffices ∀ᵐx ∂μ, μ.rnDeriv ν x ≠ 0 → p x from h_ac this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
⊢ ∀ᵐ (x : α) ∂μ, μ.rnDeriv ν x ≠ 0 → p x
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ p a) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv ν x ≠ 0 → p x) x} x}
    a
Tactic: filter_upwards [h] with _ h _ using h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ p a) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv ν x ≠ 0 → p x) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ, μ.rnDeriv ν x ≠ 0 → p x
have h₂ : ∀ (a : α), p a → μ.rnDeriv ν a ≠ 0 → p a
Tactic: filter_upwards [h] with _ h _ using h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = (μ : (a : Set α) → ℝ≥0∞) s
have rw : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← withDensity_apply _ hs, 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 ν
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = (μ : (a : Set α) → ℝ≥0∞) s
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← withDensity_apply _ hs, 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 : SFinite ν
hμν : μ ≪ ν
s : Set α
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = (μ : (a : Set α) → ℝ≥0∞) s
have rw : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← withDensity_apply' _ s, 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 : SFinite ν
hμν : μ ≪ ν
s : Set α
rw : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = (μ : (a : Set α) → ℝ≥0∞) s
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← withDensity_apply' _ s, 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 ν
hμν : μ ≪ ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x ∂ν = (μ : (a : Set α) → ℝ≥0∞) Set.univ
have rw : ∫⁻ (x : α) in Set.univ, μ.rnDeriv ν x ∂ν = (μ : (a : Set α) → ℝ≥0∞) Set.univ
Tactic: rw [← setLIntegral_univ, setLIntegral_rnDeriv' hμν MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
rw : ∫⁻ (x : α) in Set.univ, μ.rnDeriv ν x ∂ν = (μ : (a : Set α) → ℝ≥0∞) Set.univ
⊢ ∫⁻ (x : α), μ.rnDeriv ν x ∂ν = (μ : (a : Set α) → ℝ≥0∞) Set.univ
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: rw [← setLIntegral_univ, setLIntegral_rnDeriv' hμν MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal) s ν
have refine : ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≠ ∞
Tactic: refine integrable_toReal_of_lintegral_ne_top (Measure.measurable_rnDeriv _ _).aemeasurable ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real s
have rw : (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s)
Tactic: rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hs : MeasurableSet s
rw : (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s)
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real s
have rw₁ : ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
Tactic: rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s)
have rw : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∨
  Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SFinite ν
s : Set α
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real s
have rw : (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s)
Tactic: rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SFinite ν
s : Set α
rw : (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s)
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real s
have rw₁ : ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞
Tactic: rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SFinite ν
s : Set α
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s)
have rw : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∨
  Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply' _ s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s
have ht : let t := toMeasurable μ s;
t = toMeasurable μ s
Tactic: set t := toMeasurable μ s with ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s
have ht_m : MeasurableSet t
Tactic: have ht_m : MeasurableSet t := measurableSet_toMeasurable μ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s
have hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hμt : μ t ≠ ∞ := by rwa [ht, measure_toMeasurable s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α) in t, (μ.rnDeriv ν x).toReal ∂ν)
have refine_1 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal) t ν
Tactic: refine setIntegral_mono_set ?_ ?_ (HasSubset.Subset.eventuallyLE (subset_toMeasurable _ _))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal) t ν
⊢ LE.le (α := ℝ) (∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α) in t, (μ.rnDeriv ν x).toReal ∂ν)
have refine_2 : (ae (ν.restrict t)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (μ.rnDeriv ν x).toReal
Tactic: refine setIntegral_mono_set ?_ ?_ (HasSubset.Subset.eventuallyLE (subset_toMeasurable _ _))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) t) ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)
have h : ν.withDensity (μ.rnDeriv ν) ≤ μ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real t = μ.real s
have rw : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) = μ.real s
Tactic: rw [measureReal_def, measureReal_def, measure_toMeasurable s]