awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ HasFiniteIntegral f μ
have rw : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ∞
Tactic: rw [hasFiniteIntegral_iff_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
rw : HasFiniteIntegral bound μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
have rw₁ : 0 ≤ᶠ[ae μ] bound
Tactic: rw [← hasFiniteIntegral_iff_ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ∞
have lintegral_mono_ae : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
Tactic: calc
    (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) ≤ ∫⁻ a, ENNReal.ofReal (bound a) ∂μ :=
      lintegral_mono_ae <| ae_norm_ofReal_f_le_bound h_bound h_lim
    _ < ∞ := by
      rw [← hasFiniteIntegral_iff_ofReal]
      · exact bound_hasFiniteIntegral
      exact (h_bound 0).mono fun a h => le_trans (norm_nonneg _) h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
have f_measurable : AEStronglyMeasurable f μ
Tactic: have f_measurable : AEStronglyMeasurable f μ :=
    aestronglyMeasurable_of_tendsto_ae _ F_measurable h_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
have h : ∀ (a : α) (h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a))
  (h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)), ENNReal.ofReal ‖F n a - f a‖ ≤ b a
Tactic: filter_upwards [all_ae_norm_ofReal_F_le_bound h_bound n,
      ae_norm_ofReal_f_le_bound h_bound h_lim] with a h₁ h₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖
have rw : ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal (‖F n a‖ + ‖f a‖)
Tactic: rw [← ENNReal.ofReal_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
rw : ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal (‖F n a‖ + ‖f a‖)
⊢ ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖
have hp : 0 ≤ ‖F n a‖
Tactic: rw [← ENNReal.ofReal_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
rw : ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal (‖F n a‖ + ‖f a‖)
hp : 0 ≤ ‖F n a‖
⊢ ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖
have hq : 0 ≤ ‖f a‖
Tactic: rw [← ENNReal.ofReal_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal (‖F n a‖ + ‖f a‖)
have h : ‖F n a - f a‖ ≤ ‖F n a‖ + ‖f a‖
Tactic: apply ofReal_le_ofReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) = b a
have rw : 2 * ENNReal.ofReal (bound a) = b a
Tactic: rw [← two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal ‖F n a - f a‖ ≤ b a
have n₁ : ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖
Tactic: calc
      ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖ := by
        rw [← ENNReal.ofReal_add]
        · apply ofReal_le_ofReal
          apply norm_sub_le
        · exact norm_nonneg _
        · exact norm_nonneg _
      _ ≤ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) := add_le_add h₁ h₂
      _ = b a := by rw [← two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
n₁ : ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖
⊢ ENNReal.ofReal ‖F n a - f a‖ ≤ b a
have n₂ : ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) = b a
Tactic: calc
      ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖ := by
        rw [← ENNReal.ofReal_add]
        · apply ofReal_le_ofReal
          apply norm_sub_le
        · exact norm_nonneg _
        · exact norm_nonneg _
      _ ≤ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) := add_le_add h₁ h₂
      _ = b a := by rw [← two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
have hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
Tactic: have hb : ∀ n, ∀ᵐ a ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a := by
    intro n
    filter_upwards [all_ae_norm_ofReal_F_le_bound h_bound n,
      ae_norm_ofReal_f_le_bound h_bound h_lim] with a h₁ h₂
    calc
      ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖ := by
        rw [← ENNReal.ofReal_add]
        · apply ofReal_le_ofReal
          apply norm_sub_le
        · exact norm_nonneg _
        · exact norm_nonneg _
      _ ≤ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) := add_le_add h₁ h₂
      _ = b a := by rw [← two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
have rw : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 (ENNReal.ofReal 0))
Tactic: rw [← ENNReal.ofReal_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 (ENNReal.ofReal 0))
have refine : ∀ (a : α) (h : Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))),
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖F n a - f a‖) atTop (𝓝 0)
Tactic: refine h_lim.mono fun a h => (continuous_ofReal.tendsto _).comp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
have h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
Tactic: have h : ∀ᵐ a ∂μ, Tendsto (fun n => ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0) := by
    rw [← ENNReal.ofReal_zero]
    refine h_lim.mono fun a h => (continuous_ofReal.tendsto _).comp ?_
    rwa [← tendsto_iff_norm_sub_tendsto_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
this : Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ (x : α), 0 ∂μ))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
have rwa : ∀ (this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)),
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
Tactic: rwa [lintegral_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
have suffices : Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ (x : α), 0 ∂μ))
Tactic: suffices Tendsto (fun n => ∫⁻ a, ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ _ : α, 0 ∂μ)) by
    rwa [lintegral_zero] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ (x : α), 0 ∂μ))
have refine_1 : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal ‖F n a - f a‖) μ
Tactic: refine tendsto_lintegral_of_dominated_convergence' _ ?_ hb ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
refine_1 : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal ‖F n a - f a‖) μ
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 (∫⁻ (x : α), 0 ∂μ))
have refine_2 : ∫⁻ (a : α), b a ∂μ ≠ ∞
Tactic: refine tendsto_lintegral_of_dominated_convergence' _ ?_ hb ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∫⁻ (a : α), b a ∂μ ≠ ∞
have refine_2 : ∀ (bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞)
  (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
  (h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))) (f_measurable : AEStronglyMeasurable f μ),
  let b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a);
  ∀ (hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a)
    (h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)),
    ∫⁻ (a : α), b a ∂μ ≠ ∞
Tactic: rw [hasFiniteIntegral_iff_ofReal] at bound_hasFiniteIntegral
Cleared hypotheses: bound_hasFiniteIntegral, h_bound, h_lim, f_measurable, b, hb, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
refine_2 :
  ∀ (bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞)
    (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
    (h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))) (f_measurable : AEStronglyMeasurable f μ),
    let b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a);
    ∀ (hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a)
      (h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)),
      ∫⁻ (a : α), b a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), b a ∂μ ≠ ∞
have refine_2₁ : 0 ≤ᶠ[ae μ] bound
Tactic: rw [hasFiniteIntegral_iff_ofReal] at bound_hasFiniteIntegral
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∫⁻ (a : α), b a ∂μ = 2 * ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ
have hr : Ne (α := ℝ≥0∞) 2 ∞
Tactic: rw [lintegral_const_mul']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∫⁻ (a : α), b a ∂μ ≠ ∞
have b₁ : ∫⁻ (a : α), b a ∂μ = 2 * ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ
Tactic: calc
        ∫⁻ a, b a ∂μ = 2 * ∫⁻ a, ENNReal.ofReal (bound a) ∂μ := by
          rw [lintegral_const_mul']
          finiteness
        _ ≠ ∞ := mul_ne_top coe_ne_top bound_hasFiniteIntegral.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ 0 ≤ᶠ[ae μ] bound
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖F 0 a‖ ≤ bound a) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ bound x) x} x}
    a
Tactic: filter_upwards [h_bound 0] with _ h using le_trans (norm_nonneg _) h