awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
refine_2 :
  (ae ν).EventuallyLE (β := ℝ) (fun (x : 𝓧) ↦ c * (μ.rnDeriv ν x).toReal + c') fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal
⊢ Integrable (ε := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
have refine_3 : (ae ν).EventuallyLE (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) fun (x : 𝓧) ↦
  @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal
Tactic: refine integrable_of_le_of_le (f := fun a ↦ f (μ.rnDeriv ν a).toReal)
    (g₁ := fun x ↦ c * (μ.rnDeriv ν x).toReal + c')
    (g₂ := fun x ↦ ∫ b, f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal ∂(η x))
    ?_ ?_ ?_ (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
refine_2 :
  (ae ν).EventuallyLE (β := ℝ) (fun (x : 𝓧) ↦ c * (μ.rnDeriv ν x).toReal + c') fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal
refine_3 :
  (ae ν).EventuallyLE (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) fun (x : 𝓧) ↦
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal
⊢ Integrable (ε := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
have refine_4 : Integrable (ε := ℝ)
  (fun (x : 𝓧) ↦
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal)
  ν
Tactic: refine integrable_of_le_of_le (f := fun a ↦ f (μ.rnDeriv ν a).toReal)
    (g₁ := fun x ↦ c * (μ.rnDeriv ν x).toReal + c')
    (g₂ := fun x ↦ ∫ b, f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal ∂(η x))
    ?_ ?_ ?_ (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ Measurable (μ.rnDeriv ν) ∧ μ.singularPart ν ⟂ₘ ν ∧ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
have rw : Measurable.{u_1, 0} (α := α)
    (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦ Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2)
        sorry).2 ∧
  (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦ Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2)
          sorry).1 ⟂ₘ
      ν ∧
    μ =
      (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
            Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) sorry).1 +
        ν.withDensity
          (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
              Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) sorry).2
Tactic: rw [singularPart, rnDeriv, dif_pos h, dif_pos h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.rnDeriv ν = 0
have rw : Eq.{u_1 + 1} (α := α → ℝ≥0∞)
  (if h : μ.HaveLebesgueDecomposition ν then
    (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦ Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2)
        sorry).2
  else 0)
  0
Tactic: rw [rnDeriv, dif_neg h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
rw :
  Eq.{u_1 + 1} (α := α → ℝ≥0∞)
    (if h : μ.HaveLebesgueDecomposition ν then
      (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
          Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).2
    else 0)
    0
⊢ μ.rnDeriv ν = 0
have rw₁ : Eq.{u_1 + 1} (α := α → ℝ≥0∞) 0 0
Tactic: rw [rnDeriv, dif_neg h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν = 0
have rw : Eq.{u_1 + 1} (α := Measure α)
  (if h : μ.HaveLebesgueDecomposition ν then
    (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦ Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2)
        sorry).1
  else 0)
  0
Tactic: rw [singularPart, dif_neg h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
rw :
  Eq.{u_1 + 1} (α := Measure α)
    (if h : μ.HaveLebesgueDecomposition ν then
      (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
          Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).1
    else 0)
    0
⊢ μ.singularPart ν = 0
have rw₁ : Eq.{u_1 + 1} (α := Measure α) 0 0
Tactic: rw [singularPart, dif_neg h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ Measurable (μ.rnDeriv ν)
have pos : ∀ (h : μ.HaveLebesgueDecomposition ν), Measurable (μ.rnDeriv ν)
Tactic: by_cases h : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
pos : ∀ (h : μ.HaveLebesgueDecomposition ν), Measurable (μ.rnDeriv ν)
⊢ Measurable (μ.rnDeriv ν)
have neg : ∀ (h : ¬μ.HaveLebesgueDecomposition ν), Measurable (μ.rnDeriv ν)
Tactic: by_cases h : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ Measurable (μ.rnDeriv ν)
have neg : Measurable.{u_1, 0} (α := α) (β := ℝ≥0∞) 0
Tactic: rw [rnDeriv_of_not_haveLebesgueDecomposition h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν
have pos : ∀ (h : μ.HaveLebesgueDecomposition ν), μ.singularPart ν ⟂ₘ ν
Tactic: by_cases h : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
pos : ∀ (h : μ.HaveLebesgueDecomposition ν), μ.singularPart ν ⟂ₘ ν
⊢ μ.singularPart ν ⟂ₘ ν
have neg : ∀ (h : ¬μ.HaveLebesgueDecomposition ν), μ.singularPart ν ⟂ₘ ν
Tactic: by_cases h : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ ν
have neg : 0 ⟂ₘ ν
Tactic: rw [singularPart_of_not_haveLebesgueDecomposition h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν = μ
have rw : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = μ
Tactic: rw [add_comm, singularPart_add_rnDeriv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
rw : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = μ
⊢ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν = μ
have rw₁ : μ = μ
Tactic: rw [add_comm, singularPart_add_rnDeriv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν μ' : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : μ'.HaveLebesgueDecomposition ν
⊢ (μ + μ').HaveLebesgueDecomposition ν
have this : ∀ (b : Bool), (bif b then μ else μ').HaveLebesgueDecomposition ν
Tactic: have : ∀ b, HaveLebesgueDecomposition (cond b μ μ') ν := by simp [*]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ r • μ = p.1 + ν.withDensity p.2
have hmeas : Measurable (μ.rnDeriv ν)
Tactic: obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
hmeas : Measurable (μ.rnDeriv ν)
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ r • μ = p.1 + ν.withDensity p.2
have hsing : μ.singularPart ν ⟂ₘ ν
Tactic: obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ r • μ = p.1 + ν.withDensity p.2
have hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
Tactic: obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ r • μ = p.1 + ν.withDensity p.2
have refine : r • μ = (r • μ.singularPart ν, r • μ.rnDeriv ν).1 + ν.withDensity (r • μ.singularPart ν, r • μ.rnDeriv ν).2
Tactic: refine ⟨⟨r • μ.singularPart ν, r • μ.rnDeriv ν⟩, hmeas.const_smul _, hsing.smul _, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ r • μ = r • μ.singularPart ν + ν.withDensity (r • μ.rnDeriv ν)
have rw : r • μ = r • μ.singularPart ν + r • ν.withDensity (μ.rnDeriv ν)
Tactic: rw [withDensity_smul _ hmeas, ← smul_add, ← hadd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
rw : r • μ = r • μ.singularPart ν + r • ν.withDensity (μ.rnDeriv ν)
⊢ r • μ = r • μ.singularPart ν + ν.withDensity (r • μ.rnDeriv ν)
have rw₁ : r • μ = r • (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν))
Tactic: rw [withDensity_smul _ hmeas, ← smul_add, ← hadd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
rw : r • μ = r • μ.singularPart ν + r • ν.withDensity (μ.rnDeriv ν)
rw₁ : r • μ = r • (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν))
⊢ r • μ = r • μ.singularPart ν + ν.withDensity (r • μ.rnDeriv ν)
have rw₂ : r • μ = r • μ
Tactic: rw [withDensity_smul _ hmeas, ← smul_add, ← hadd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2
have hmeas : Measurable (μ.rnDeriv ν)
Tactic: obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2
have hsing : μ.singularPart ν ⟂ₘ ν
Tactic: obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2
have hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
Tactic: obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2
have pos : ∀ (hr : r = 0), ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
pos : ∀ (hr : r = 0), ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2
have neg : ∀ (hr : ¬r = 0), ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2
have neg : μ = (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).1 + (r • ν).withDensity (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).2
Tactic: refine ⟨⟨μ.singularPart ν, r⁻¹ • μ.rnDeriv ν⟩, hmeas.const_smul _,
      hsing.mono_ac AbsolutelyContinuous.rfl smul_absolutelyContinuous, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
⊢ μ = (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).1 + (r • ν).withDensity (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).2
have this : r⁻¹ • μ.rnDeriv ν = (↑r⁻¹ : ℝ≥0∞) • μ.rnDeriv ν
Tactic: have : r⁻¹ • rnDeriv μ ν = ((r⁻¹ : ℝ≥0) : ℝ≥0∞) • rnDeriv μ ν := by simp [ENNReal.smul_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = (↑r⁻¹ : ℝ≥0∞) • μ.rnDeriv ν
⊢ μ = (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).1 + (r • ν).withDensity (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).2
have neg : μ = (μ.singularPart ν, (↑r : ℝ≥0∞)⁻¹ • μ.rnDeriv ν).1 + ν.withDensity (μ.rnDeriv ν)
Tactic: rw [this, withDensity_smul _ hmeas, ENNReal.smul_def r, withDensity_smul_measure,
      ← smul_assoc, smul_eq_mul, ENNReal.coe_inv hr, ENNReal.inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = (↑r⁻¹ : ℝ≥0∞) • μ.rnDeriv ν
neg : μ = (μ.singularPart ν, (↑r : ℝ≥0∞)⁻¹ • μ.rnDeriv ν).1 + ν.withDensity (μ.rnDeriv ν)
⊢ μ = (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).1 + (r • ν).withDensity (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).2
have neg₁ : (↑r : ℝ≥0∞) ≠ 0
Tactic: rw [this, withDensity_smul _ hmeas, ENNReal.smul_def r, withDensity_smul_measure,
      ← smul_assoc, smul_eq_mul, ENNReal.coe_inv hr, ENNReal.inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = (↑r⁻¹ : ℝ≥0∞) • μ.rnDeriv ν
neg : μ = (μ.singularPart ν, (↑r : ℝ≥0∞)⁻¹ • μ.rnDeriv ν).1 + ν.withDensity (μ.rnDeriv ν)
neg₁ : (↑r : ℝ≥0∞) ≠ 0
⊢ μ = (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).1 + (r • ν).withDensity (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).2
have neg₂ : (↑r : ℝ≥0∞) ≠ ∞
Tactic: rw [this, withDensity_smul _ hmeas, ENNReal.smul_def r, withDensity_smul_measure,
      ← smul_assoc, smul_eq_mul, ENNReal.coe_inv hr, ENNReal.inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ≤ μ
have pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), μ.singularPart ν ≤ μ
Tactic: by_cases hl : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), μ.singularPart ν ≤ μ
⊢ μ.singularPart ν ≤ μ
have neg : ∀ (hl : ¬μ.HaveLebesgueDecomposition ν), μ.singularPart ν ≤ μ
Tactic: by_cases hl : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
| μ
have rw : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
Tactic: rw [haveLebesgueDecomposition_add μ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ≤ μ
have pos : μ.singularPart ν ≤ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
Tactic: conv_rhs => rw [haveLebesgueDecomposition_add μ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ≤ μ
have neg : 0 ≤ μ
Tactic: rw [singularPart, dif_neg hl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ
have pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), ν.withDensity (μ.rnDeriv ν) ≤ μ
Tactic: by_cases hl : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), ν.withDensity (μ.rnDeriv ν) ≤ μ
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ
have neg : ∀ (hl : ¬μ.HaveLebesgueDecomposition ν), ν.withDensity (μ.rnDeriv ν) ≤ μ
Tactic: by_cases hl : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ
have pos : ν.withDensity (μ.rnDeriv ν) ≤ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
Tactic: conv_rhs => rw [haveLebesgueDecomposition_add μ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ
have neg : 0 ≤ μ
Tactic: rw [rnDeriv, dif_neg hl, withDensity_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν
⊢ μ ≪ μ.withDensity (ν.rnDeriv μ)
have hμν₁ : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
Tactic: rw [haveLebesgueDecomposition_add ν μ] at hμν
Cleared hypotheses: hμν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
⊢ μ ≪ μ.withDensity (ν.rnDeriv μ)
have refine : ∀ (s : Set α),
  MeasurableSet s →
    ∀ (hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine AbsolutelyContinuous.mk (fun s _ hνs ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have obtain : ∀ (t : Set α),
  MeasurableSet t →
    ∀ (ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
      (ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: obtain ⟨t, _, ht1, ht2⟩ := mutuallySingular_singularPart ν μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← inter_union_compl s, ← nonpos_iff_eq_zero]