awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
⊢ μ = (μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2
have refine_2 : ∀ (A : Set α) (hA : MeasurableSet A),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: ext1 A hA
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
A : Set α
hA : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have refine_2 : (μ : (a : Set α) → ℝ≥0∞) A =
  HAdd.hAdd (α := (a : Set α) → ℝ≥0∞) (β := (a : Set α) → ℝ≥0∞) (⇑(μ - ν.withDensity ξ, ξ).1 : (a : Set α) → ℝ≥0∞)
    (⇑(ν.withDensity (μ - ν.withDensity ξ, ξ).2) : (a : Set α) → ℝ≥0∞) A
Tactic: rw [Measure.coe_add, Pi.add_apply, Measure.sub_apply hA hle, add_comm,
        add_tsub_cancel_of_le (hle A)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
A : Set α
hA : MeasurableSet A
refine_2 :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := (a : Set α) → ℝ≥0∞) (β := (a : Set α) → ℝ≥0∞) (⇑(μ - ν.withDensity ξ, ξ).1 : (a : Set α) → ℝ≥0∞)
      (⇑(ν.withDensity (μ - ν.withDensity ξ, ξ).2) : (a : Set α) → ℝ≥0∞) A
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have refine_2₁ : (μ : (a : Set α) → ℝ≥0∞) A =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ - ν.withDensity ξ, ξ).1 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [Measure.coe_add, Pi.add_apply, Measure.sub_apply hA hle, add_comm,
        add_tsub_cancel_of_le (hle A)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
A : Set α
hA : MeasurableSet A
refine_2 :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := (a : Set α) → ℝ≥0∞) (β := (a : Set α) → ℝ≥0∞) (⇑(μ - ν.withDensity ξ, ξ).1 : (a : Set α) → ℝ≥0∞)
      (⇑(ν.withDensity (μ - ν.withDensity ξ, ξ).2) : (a : Set α) → ℝ≥0∞) A
refine_2₁ :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ - ν.withDensity ξ, ξ).1 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      ((ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have refine_2₂ : (μ : (a : Set α) → ℝ≥0∞) A =
  HAdd.hAdd (β := ℝ≥0∞)
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞))
    ((ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [Measure.coe_add, Pi.add_apply, Measure.sub_apply hA hle, add_comm,
        add_tsub_cancel_of_le (hle A)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
A : Set α
hA : MeasurableSet A
refine_2 :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := (a : Set α) → ℝ≥0∞) (β := (a : Set α) → ℝ≥0∞) (⇑(μ - ν.withDensity ξ, ξ).1 : (a : Set α) → ℝ≥0∞)
      (⇑(ν.withDensity (μ - ν.withDensity ξ, ξ).2) : (a : Set α) → ℝ≥0∞) A
refine_2₁ :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ - ν.withDensity ξ, ξ).1 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      ((ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
refine_2₂ :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
        ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞))
      ((ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have refine_2₃ : (μ : (a : Set α) → ℝ≥0∞) A =
  HAdd.hAdd (α := ℝ≥0∞) ((ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞))
Tactic: rw [Measure.coe_add, Pi.add_apply, Measure.sub_apply hA hle, add_comm,
        add_tsub_cancel_of_le (hle A)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
A : Set α
hA : MeasurableSet A
refine_2 :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := (a : Set α) → ℝ≥0∞) (β := (a : Set α) → ℝ≥0∞) (⇑(μ - ν.withDensity ξ, ξ).1 : (a : Set α) → ℝ≥0∞)
      (⇑(ν.withDensity (μ - ν.withDensity ξ, ξ).2) : (a : Set α) → ℝ≥0∞) A
refine_2₁ :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ - ν.withDensity ξ, ξ).1 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      ((ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
refine_2₂ :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
        ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞))
      ((ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
refine_2₃ :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := ℝ≥0∞) ((ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
        ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have refine_2₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [Measure.coe_add, Pi.add_apply, Measure.sub_apply hA hle, add_comm,
        add_tsub_cancel_of_le (hle A)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SFinite μ
inst_1 : SigmaFinite ν
⊢ μ.HaveLebesgueDecomposition ν
have inr : ∀ (this : ∀ (μ : Measure α) [SFinite μ] (hμ : IsFiniteMeasure μ), μ.HaveLebesgueDecomposition ν)
  (hμ : ¬IsFiniteMeasure μ), μ.HaveLebesgueDecomposition ν
Tactic: wlog hμ : IsFiniteMeasure μ generalizing μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SFinite μ
inst_1 : SigmaFinite ν
inr :
  ∀ (this : ∀ (μ : Measure α) [SFinite μ] (hμ : IsFiniteMeasure μ), μ.HaveLebesgueDecomposition ν)
    (hμ : ¬IsFiniteMeasure μ), μ.HaveLebesgueDecomposition ν
⊢ μ.HaveLebesgueDecomposition ν
have wlog : ∀ (μ : Measure α) [SFinite μ] (hμ : IsFiniteMeasure μ), μ.HaveLebesgueDecomposition ν
Tactic: wlog hμ : IsFiniteMeasure μ generalizing μ
Cleared hypotheses: μ, inst
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
⊢ μ.HaveLebesgueDecomposition ν
have hsm : ∀ (n : ℕ), MeasurableSet (s n)
Tactic: have hsm : ∀ n, MeasurableSet (s n) := .disjointed <| measurableSet_spanningSets _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
⊢ μ.HaveLebesgueDecomposition ν
have hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have hs : ∀ n, Fact (ν (s n) < ⊤) := fun n ↦
    ⟨lt_of_le_of_lt (measure_mono <| disjointed_le ..) (measure_spanningSets_lt_top ν n)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
⊢ μ.HaveLebesgueDecomposition ν
have hfm : ∀ (n : ℕ), Measurable (f n)
Tactic: have hfm (n : ℕ) : Measurable (f n) := by measurability
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
⊢ sum ξ ⟂ₘ ν
have refine : ∀ (n : ℕ), ξ n ⟂ₘ ν
Tactic: refine MutuallySingular.sum_left.2 fun n ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
⊢ ξ n ⟂ₘ ν
have rw : ξ n ⟂ₘ ν.restrict (s n) + ν.restrict (s n)ᶜ
Tactic: rw [← ν.restrict_add_restrict_compl (hsm n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
⊢ ξ n ⟂ₘ ν.restrict (s n) + ν.restrict (s n)ᶜ
have refine : μ.restrict (s n) ⟂ₘ ν.restrict (s n)ᶜ
Tactic: refine (mutuallySingular_singularPart ..).add_right (.singularPart ?_ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
⊢ μ.restrict (s n) ⟂ₘ ν.restrict (s n)ᶜ
have refine : Eq (α := ℝ≥0∞) ((μ.restrict (s n) : (a : Set α) → ℝ≥0∞) (s n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
  Eq (α := ℝ≥0∞) ((ν.restrict (s n)ᶜ : (a : Set α) → ℝ≥0∞) (s n)ᶜᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨(s n)ᶜ, (hsm n).compl, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
⊢ μ.HaveLebesgueDecomposition ν
have hξ : sum ξ ⟂ₘ ν
Tactic: have hξ : .sum ξ ⟂ₘ ν := by
    refine MutuallySingular.sum_left.2 fun n ↦ ?_
    rw [← ν.restrict_add_restrict_compl (hsm n)]
    refine (mutuallySingular_singularPart ..).add_right (.singularPart ?_ _)
    refine ⟨(s n)ᶜ, (hsm n).compl, ?_⟩
    simp [hsm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
hξ : sum ξ ⟂ₘ ν
⊢ sum ξ + ν.withDensity (∑' (n : ℕ), f n) = sum fun (n : ℕ) ↦ ξ n + ν.withDensity (f n)
have rw : (sum ξ + sum fun (n : ℕ) ↦ ν.withDensity (f n)) = sum fun (n : ℕ) ↦ ξ n + ν.withDensity (f n)
Tactic: rw [withDensity_tsum hfm, Measure.sum_add_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
hξ : sum ξ ⟂ₘ ν
rw : (sum ξ + sum fun (n : ℕ) ↦ ν.withDensity (f n)) = sum fun (n : ℕ) ↦ ξ n + ν.withDensity (f n)
⊢ sum ξ + ν.withDensity (∑' (n : ℕ), f n) = sum fun (n : ℕ) ↦ ξ n + ν.withDensity (f n)
have rw₁ : Eq.{u_1 + 1} (α := Measure α) (sum fun (n : ℕ) ↦ ξ n + ν.withDensity (f n))
  (sum fun (n : ℕ) ↦ ξ n + ν.withDensity (f n))
Tactic: rw [withDensity_tsum hfm, Measure.sum_add_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
hξ : sum ξ ⟂ₘ ν
simp_rw :
  Eq.{u_1 + 1} (α := Measure α)
    (sum fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n)) + ν.withDensity (f n))
    (sum fun (n : ℕ) ↦ μ.restrict (s n))
simp_rw₁ :
  Eq.{u_1 + 1} (α := Measure α)
    (sum fun (n : ℕ) ↦
      (μ.restrict (s n)).singularPart (ν.restrict (s n)) +
        ν.withDensity ((s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))))
    (sum fun (n : ℕ) ↦ μ.restrict (s n))
⊢ Eq.{u_1 + 1} (α := Measure α) (sum fun (n : ℕ) ↦ ξ n + ν.withDensity (f n)) (sum fun (n : ℕ) ↦ μ.restrict (s n))
have simp_rw₂ : Eq.{u_1 + 1} (α := Measure α)
  (sum fun (n : ℕ) ↦
    (μ.restrict (s n)).singularPart (ν.restrict (s n)) +
      (ν.restrict (s n)).withDensity ((μ.restrict (s n)).rnDeriv (ν.restrict (s n))))
  (sum fun (n : ℕ) ↦ μ.restrict (s n))
Tactic: simp_rw [ξ, f, withDensity_indicator (hsm _), singularPart_add_rnDeriv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
hξ : sum ξ ⟂ₘ ν
⊢ μ.HaveLebesgueDecomposition ν
have hadd : sum ξ + ν.withDensity (∑' (n : ℕ), f n) = μ
Tactic: have hadd : .sum ξ + ν.withDensity (∑' n, f n) = μ := calc
    .sum ξ + ν.withDensity (∑' n, f n) = .sum fun n ↦ ξ n + ν.withDensity (f n) := by
      rw [withDensity_tsum hfm, Measure.sum_add_sum]
    _ = .sum fun n ↦ .restrict μ (s n) := by
      simp_rw [ξ, f, withDensity_indicator (hsm _), singularPart_add_rnDeriv]
    _ = μ := sum_restrict_disjointed_spanningSets ..
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
have rw : μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)
Tactic: rw [← withDensity_eq_iff_of_sigmaFinite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
rw : μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
have hf : AEMeasurable ((r • ν).rnDeriv μ) μ
Tactic: rw [← withDensity_eq_iff_of_sigmaFinite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
rw : μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)
hf : AEMeasurable ((r • ν).rnDeriv μ) μ
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
have hg : AEMeasurable (r • ν.rnDeriv μ) μ
Tactic: rw [← withDensity_eq_iff_of_sigmaFinite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
⊢ μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = μ.withDensity ((↑r : ℝ≥0∞) • ν.rnDeriv μ)
have rw : μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = (↑r : ℝ≥0∞) • μ.withDensity (ν.rnDeriv μ)
Tactic: rw [withDensity_smul _ (measurable_rnDeriv _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
this :
  (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
⊢ μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = (↑r : ℝ≥0∞) • μ.withDensity (ν.rnDeriv μ)
have rwa : ∀ (this : μ.withDensity ((r • ν).rnDeriv μ) = r • μ.withDensity (ν.rnDeriv μ)),
  μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = (↑r : ℝ≥0∞) • μ.withDensity (ν.rnDeriv μ)
Tactic: rwa [Measure.add_right_inj] at this
Cleared hypotheses: this