awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
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
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
have hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
Tactic: have hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ a, ξ a ∂ν := by
      have := @lintegral_tendsto_of_tendsto_of_monotone _ _ ν (fun n ↦ ⨆ (k) (_ : k ≤ n), f k)
          (⨆ (n) (k) (_ : k ≤ n), f k) ?_ ?_ ?_
      · refine tendsto_nhds_unique ?_ this
        refine tendsto_of_tendsto_of_tendsto_of_le_of_le hg₂ tendsto_const_nhds (fun n ↦ ?_)
          fun n ↦ ?_
        · rw [← hf₂ n]
          apply lintegral_mono
          convert! iSup_le_le f n n le_rfl
          simp only [iSup_apply]
        · exact le_sSup ⟨⨆ (k : ℕ) (_ : k ≤ n), f k, iSup_mem_measurableLE' _ hf₁ _, rfl⟩
      · intro n
        refine Measurable.aemeasurable ?_
        convert! (iSup_mem_measurableLE _ hf₁ n).1
        simp
      · refine Filter.Eventually.of_forall fun a ↦ ?_
        simp [iSup_monotone' f _]
      · refine Filter.Eventually.of_forall fun a ↦ ?_
        simp [tendsto_atTop_iSup (iSup_monotone' f 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 ∂ν
⊢ Measurable ξ
have h : ∀ (x : α), ξ x = ⨆ (i : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ i), f k x
Tactic: convert! Measurable.iSup fun n ↦ (iSup_mem_measurableLE _ hf₁ n).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
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 ∂ν
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
have hξm : Measurable ξ
Tactic: have hξm : Measurable ξ := by
      convert! Measurable.iSup fun n ↦ (iSup_mem_measurableLE _ hf₁ n).1
      simp [hξ]
-- 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 ξ
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (a : α) in A, (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
have simp_rw : ∫⁻ (a : α) in A, ⨆ (i : ℕ), ⨆ (i_1 : ℕ), ⨆ (_ : i_1 ≤ i), f i_1 a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
Tactic: simp_rw [iSup_apply]
-- 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 ξ
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (a : α) in A, ⨆ (i : ℕ), ⨆ (i_1 : ℕ), ⨆ (_ : i_1 ≤ i), f i_1 a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
have rw : LE.le (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α) in A, ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k a ∂ν : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [lintegral_iSup (fun n ↦ (iSup_mem_measurableLE _ hf₁ n).1) (iSup_monotone _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
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 ξ
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
have hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
Tactic: have hξle A (hA : MeasurableSet A) : ∫⁻ a in A, ξ a ∂ν ≤ μ A := by
        rw [hξ]
        simp_rw [iSup_apply]
        rw [lintegral_iSup (fun n ↦ (iSup_mem_measurableLE _ hf₁ n).1) (iSup_monotone _)]
        exact iSup_le fun n ↦ (iSup_mem_measurableLE _ hf₁ n).2 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
⊢ ν.withDensity ξ ≤ μ
have refine : ∀ (B : Set α) (hB : MeasurableSet B),
  B.Nonempty → LE.le (α := ℝ≥0∞) ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞)
Tactic: refine le_intro fun B hB _ ↦ ?_
-- 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
B : Set α
hB : MeasurableSet B
h_1 : B.Nonempty
⊢ LE.le (α := ℝ≥0∞) ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞)
have rw : ∫⁻ (a : α) in B, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) B
Tactic: rw [withDensity_apply _ hB]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
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
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
have hle : ν.withDensity ξ ≤ μ
Tactic: have hle : ν.withDensity ξ ≤ μ := by
      refine le_intro fun B hB _ ↦ ?_
      rw [withDensity_apply _ hB]
      exact hξle B hB
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
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 ξ ≤ μ
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
have this : IsFiniteMeasure (ν.withDensity ξ)
Tactic: have : IsFiniteMeasure (ν.withDensity ξ) := isFiniteMeasure_of_le _ hle
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
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 ξ)
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
have hμ₁ : let μ₁ := μ - ν.withDensity ξ;
μ₁ = μ - ν.withDensity ξ
Tactic: set μ₁ := μ - ν.withDensity ξ with hμ₁
-- 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 ξ
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
have refine_1 : (μ₁, ξ).1 ⟂ₘ ν
Tactic: refine ⟨⟨μ₁, ξ⟩, hξm, ?_, ?_⟩
-- 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 ξ
refine_1 : (μ₁, ξ).1 ⟂ₘ ν
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
have refine_2 : μ = (μ₁, ξ).1 + ν.withDensity (μ₁, ξ).2
Tactic: refine ⟨⟨μ₁, ξ⟩, hξm, ?_, ?_⟩
-- 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 ξ
⊢ (μ₁, ξ).1 ⟂ₘ ν
have refine_1 : ∀ (h : ¬(μ₁, ξ).1 ⟂ₘ ν), False
Tactic: by_contra h
-- 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_1 : 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 ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
⊢ False
have refine_1 : ∀ (ε : ℝ≥0) (hε₁ : 0 < ε) (E : Set α) (hE₁ : MeasurableSet E)
  (hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞))
  (hE₃ :
    ∀ (A : Set α),
      MeasurableSet A →
        HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
          (μ₁ : (a : Set α) → ℝ≥0∞) (A ∩ E)),
  False
Tactic: obtain ⟨ε, hε₁, E, hE₁, hE₂, hE₃⟩ := exists_positive_of_not_mutuallySingular μ₁ ν h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h_1 : 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 ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
have hE₄ : HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
  (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
Tactic: specialize hE₃ A hA
Cleared hypotheses: hE₃
-- 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_1 : 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 ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hE₃ :
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
    (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
⊢ ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
have rw : HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) + ∫⁻ (a : α) in A ∩ E, ξ a ∂ν ≤
  (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
Tactic: rw [lintegral_add_left measurable_const, lintegral_const, restrict_apply_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h_1 : 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 ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hE₃ :
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
    (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) + ∫⁻ (a : α) in A ∩ E, ξ a ∂ν ≤
    (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
have hE₄ : HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
  HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) (∫⁻ (a : α) in A ∩ E, ξ a ∂ν)
Tactic: rw [Measure.sub_apply (hA.inter hE₁) hle, withDensity_apply _ (hA.inter hE₁)] at hE₃
Cleared hypotheses: hE₃
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h_1 : 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 ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
⊢ False
have hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
Tactic: have hε₂ (A : Set α) (hA : MeasurableSet A) : ∫⁻ a in A ∩ E, ε + ξ a ∂ν ≤ μ (A ∩ E) := by
        specialize hE₃ A hA
        rw [lintegral_add_left measurable_const, lintegral_const, restrict_apply_univ]
        rw [Measure.sub_apply (hA.inter hE₁) hle, withDensity_apply _ (hA.inter hE₁)] at hE₃
        refine add_le_of_le_tsub_right_of_le (hξle _ (hA.inter hE₁)) hE₃
-- 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_1 : 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 ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
⊢ (ξ + E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) ∈ measurableLE ν μ
have refine : ∀ (A : Set α) (hA : MeasurableSet A),
  ∫⁻ (x : α) in A, HAdd.hAdd (β := (x : α) → ℝ≥0∞) ξ (E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) x ∂ν ≤
    (μ : (a : Set α) → ℝ≥0∞) A
Tactic: refine ⟨hξm.add (measurable_const.indicator hE₁), fun A hA ↦ ?_⟩