awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
M : ℕ
⊢ AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
have apply : MeasurableSet.{u_1} (α := α) {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)}
Tactic: apply hf.1.indicator
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
⊢ ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
have hmeas₁ : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
Tactic: have hmeas : ∀ M : ℕ, AEStronglyMeasurable ({ x | (M : ℝ) ≤ ‖f x‖₊ }.indicator f) μ := by
    intro M
    apply hf.1.indicator
    apply StronglyMeasurable.measurableSet_le stronglyMeasurable_const
      hmeas.nnnorm.measurable.coe_nnreal_real.stronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
have rw : ∀ (hf : Integrable f μ) (hmeas : StronglyMeasurable f) {ε : ℝ} (hε : 0 < ε)
  (htendsto :
    ∀ᵐ (x : α) ∂μ,
      Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0))
  (hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ),
  HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
Tactic: rw [memLp_one_iff_integrable] at hf
Cleared hypotheses: hf, hmeas_1, ε, hε, htendsto, hmeas
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
⊢ ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
have hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
Tactic: have hbound : HasFiniteIntegral (fun x => ‖f x‖) μ := by
    rw [memLp_one_iff_integrable] at hf
    exact hf.norm.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ) atTop (𝓝 0)
have refine : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖
Tactic: refine tendsto_lintegral_norm_of_dominated_convergence hmeas hbound ?_ htendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖
have refine : ∀ (n : ℕ) (x : α),
  Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x} x
Tactic: refine fun n => univ_mem' (id fun x => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
n : ℕ
x : α
⊢ Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x} x
have pos : ∀ (hx : (↑n : ℝ) ≤ ‖f x‖),
  Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x} x
Tactic: by_cases hx : (n : ℝ) ≤ ‖f x‖
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
n : ℕ
x : α
pos :
  ∀ (hx : (↑n : ℝ) ≤ ‖f x‖),
    Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x} x
have neg : ∀ (hx : ¬(↑n : ℝ) ≤ ‖f x‖),
  Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x} x
Tactic: by_cases hx : (n : ℝ) ≤ ‖f x‖
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
n : ℕ
x : α
hx : (↑n : ℝ) ≤ ‖f x‖
⊢ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f x‖ ≤ ‖f x‖
have pos : ‖f x‖ ≤ ‖f x‖
Tactic: rwa [Set.indicator_of_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
n : ℕ
x : α
hx : (↑n : ℝ) ≤ ‖f x‖
pos : ‖f x‖ ≤ ‖f x‖
⊢ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f x‖ ≤ ‖f x‖
have pos₁ : Membership.mem (γ := Set α) {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} x
Tactic: rwa [Set.indicator_of_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
n : ℕ
x : α
hx : ¬(↑n : ℝ) ≤ ‖f x‖
⊢ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f x‖ ≤ ‖f x‖
have neg : 0 ≤ ‖f x‖
Tactic: rw [Set.indicator_of_notMem, norm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
n : ℕ
x : α
hx : ¬(↑n : ℝ) ≤ ‖f x‖
neg : 0 ≤ ‖f x‖
⊢ ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f x‖ ≤ ‖f x‖
have neg₁ : x ∉ {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊}
Tactic: rw [Set.indicator_of_notMem, norm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
⊢ ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
have this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ)
  atTop (𝓝 0)
Tactic: have : Tendsto (fun n : ℕ ↦ ∫⁻ a, ENNReal.ofReal ‖{ x | n ≤ ‖f x‖₊ }.indicator f a - 0‖ ∂μ)
      atTop (𝓝 0) := by
    refine tendsto_lintegral_norm_of_dominated_convergence hmeas hbound ?_ htendsto
    refine fun n => univ_mem' (id fun x => ?_)
    by_cases hx : (n : ℝ) ≤ ‖f x‖
    · dsimp
      rwa [Set.indicator_of_mem]
    · dsimp
      rw [Set.indicator_of_notMem, norm_zero]
      · exact norm_nonneg _
      · assumption
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
this :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ) atTop (𝓝 0)
⊢ ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
have this₁ : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
Tactic: rw [ENNReal.tendsto_atTop_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
⊢ ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
have obtain : ∀ (M : ℕ)
  (hM :
    ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ENNReal.ofReal ε),
  ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨M, hM⟩ := this (ENNReal.ofReal ε) (ENNReal.ofReal_pos.2 hε)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
have hM₁ : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ∂μ ≤ ENNReal.ofReal ε
Tactic: simp only [sub_zero] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ∂μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
have refine : ∫⁻ (x : α), (↑‖Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
Tactic: refine ⟨M, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ∂μ ≤ ENNReal.ofReal ε
⊢ ∫⁻ (x : α), (↑‖Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
have h : ∀ (x : α),
  (↑‖Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) =
    ENNReal.ofReal ‖Set.indicator {x : α | (↑M : ℝ≥0) ≤ ‖f x‖₊} f x‖
Tactic: convert! hM M le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas_1 : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto :
  ∀ᵐ (x : α) ∂μ,
    Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f) μ
hbound : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ‖f x‖) μ
this :
  ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x : α | (↑n : ℝ≥0) ≤ ‖f x‖₊} f a‖ ∂μ ≤ ENNReal.ofReal ε
x : α
⊢ (↑‖Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) =
    ENNReal.ofReal ‖Set.indicator {x : α | (↑M : ℝ≥0) ≤ ‖f x‖₊} f x‖
have h : (↑‖Set.indicator {x : α | (↑M : ℝ) ≤ ‖f x‖} f x‖₊ : ℝ≥0∞) =
  (↑(NNReal.mk ‖Set.indicator {x : α | (↑M : ℝ≥0) ≤ ‖f x‖₊} f x‖ sorry) : ℝ≥0∞)
Tactic: simp only [coe_nnnorm, ENNReal.ofReal_eq_coe_nnreal (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
⊢ ∃ (M : ℝ), 0 ≤ M ∧ ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ ≤ ENNReal.ofReal ε
have hf_mk : MemLp (AEStronglyMeasurable.mk f sorry) 1 μ
Tactic: have hf_mk : MemLp (hf.1.mk f) 1 μ := (memLp_congr_ae hf.1.ae_eq_mk).mp hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
hf_mk : MemLp (AEStronglyMeasurable.mk f ⋯) 1 μ
⊢ ∃ (M : ℝ), 0 ≤ M ∧ ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ ≤ ENNReal.ofReal ε
have obtain : ∀ (M : ℝ) (hM_pos : 0 ≤ M)
  (hfM :
    ∫⁻ (x : α),
        ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f sorry x‖₊ : ℝ)} (AEStronglyMeasurable.mk f sorry) x‖ₑ ∂μ ≤
      ENNReal.ofReal ε),
  ∃ (M : ℝ), 0 ≤ M ∧ ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨M, hM_pos, hfM⟩ :=
    hf_mk.integral_indicator_norm_ge_nonneg_le_of_meas hf.1.stronglyMeasurable_mk hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
hf_mk : MemLp (AEStronglyMeasurable.mk f ⋯) 1 μ
M : ℝ
hM_pos : 0 ≤ M
hfM :
  ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ ≤
    ENNReal.ofReal ε
⊢ ∃ (M : ℝ), 0 ≤ M ∧ ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ ≤ ENNReal.ofReal ε
have refine : ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ =
  ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f sorry x‖₊ : ℝ)} (AEStronglyMeasurable.mk f sorry) x‖ₑ ∂μ
Tactic: refine ⟨M, hM_pos, (le_of_eq ?_).trans hfM⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
hf_mk : MemLp (AEStronglyMeasurable.mk f ⋯) 1 μ
M : ℝ
hM_pos : 0 ≤ M
hfM :
  ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ ≤
    ENNReal.ofReal ε
⊢ ∫⁻ (x : α), ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ∂μ =
    ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ
have refine : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ) fun (x : α) ↦
  ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f sorry x‖₊ : ℝ)} (AEStronglyMeasurable.mk f sorry) x‖ₑ
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
ε : ℝ
hε : 0 < ε
hf_mk : MemLp (AEStronglyMeasurable.mk f ⋯) 1 μ
M : ℝ
hM_pos : 0 ≤ M
hfM :
  ∫⁻ (x : α),
      ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ ∂μ ≤
    ENNReal.ofReal ε
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ) fun (x : α) ↦
    ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f ⋯ x‖₊ : ℝ)} (AEStronglyMeasurable.mk f ⋯) x‖ₑ
have h : ∀ (x : α) (hx : f x = AEStronglyMeasurable.mk f sorry x),
  ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ =
    ‖Set.indicator {x : α | M ≤ (↑‖AEStronglyMeasurable.mk f sorry x‖₊ : ℝ)} (AEStronglyMeasurable.mk f sorry) x‖ₑ
Tactic: filter_upwards [hf.1.ae_eq_mk] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
⊢ ∃ (M : ℝ), eLpNormEssSup (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) μ = 0
have hbdd : eLpNormEssSup f μ < ∞
Tactic: have hbdd : eLpNormEssSup f μ < ∞ := hf.eLpNorm_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
⊢ ∃ (M : ℝ), eLpNormEssSup (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) μ = 0
have refine : eLpNormEssSup (Set.indicator {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)} f) μ = 0
Tactic: refine ⟨(eLpNorm f ∞ μ + 1).toReal, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
⊢ eLpNormEssSup (Set.indicator {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)} f) μ = 0
have rw : eLpNormEssSup f (μ.restrict {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)}) = 0
Tactic: rw [eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
rw : eLpNormEssSup f (μ.restrict {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)}) = 0
⊢ eLpNormEssSup (Set.indicator {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)} f) μ = 0
have rw₁ : MeasurableSet.{u_1} (α := α) {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)}
Tactic: rw [eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
⊢ μ.restrict {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)} = 0
have simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [coe_nnnorm, eLpNorm_exponent_top, Measure.restrict_eq_zero]