awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ ∫⁻ (a : α), liminf (fun (x : ℕ) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p
have refine : liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop =
  HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p
Tactic: refine (lintegral_liminf_le' fun m => (hf m).enorm.pow_const _).trans_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop
have h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
Tactic: have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hp_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop
have h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
Tactic: have h_rpow_surj := (ENNReal.rpow_left_bijective hp_pos.ne.symm).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop
have refine_1 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ eLpNorm' (f n) p μ
Tactic: refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
refine_1 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ eLpNorm' (f n) p μ
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop
have refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ eLpNorm' (f n) p μ
Tactic: refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
refine_1 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ eLpNorm' (f n) p μ
refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ eLpNorm' (f n) p μ
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop
have refine_3 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x : ℕ) ↦
  (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
    (eLpNorm' (f x) p μ)
Tactic: refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
refine_1 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ eLpNorm' (f n) p μ
refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ eLpNorm' (f n) p μ
refine_3 :
  IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x : ℕ) ↦
    (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
      (eLpNorm' (f x) p μ)
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop
have refine_4 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x : ℕ) ↦
  (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
    (eLpNorm' (f x) p μ)
Tactic: refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p
have h_pow_liminf : HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
  liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop
Tactic: have h_pow_liminf :
    atTop.liminf (fun n ↦ eLpNorm' (f n) p μ) ^ p
      = atTop.liminf fun n ↦ eLpNorm' (f n) p μ ^ p := by
    have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hp_pos
    have h_rpow_surj := (ENNReal.rpow_left_bijective hp_pos.ne.symm).2
    refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
    all_goals isBoundedDefault
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
h_pow_liminf :
  HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop
⊢ liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p
have rw : Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
  (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop)
Tactic: rw [h_pow_liminf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
h_pow_liminf :
  HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop
⊢ Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
    (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop)
have simp_rw : Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
  (liminf (fun (n : ℕ) ↦ ((∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p) atTop)
Tactic: simp_rw [eLpNorm'_eq_lintegral_enorm, ← ENNReal.rpow_mul, one_div,
    inv_mul_cancel₀ hp_pos.ne.symm, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
h_pow_liminf :
  HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop
simp_rw :
  Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
    (liminf (fun (n : ℕ) ↦ ((∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p) atTop)
⊢ Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
    (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop)
have simp_rw₁ : Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
  (liminf (fun (n : ℕ) ↦ (∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) ^ (1 / p * p)) atTop)
Tactic: simp_rw [eLpNorm'_eq_lintegral_enorm, ← ENNReal.rpow_mul, one_div,
    inv_mul_cancel₀ hp_pos.ne.symm, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
h_pow_liminf :
  HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop
simp_rw :
  Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
    (liminf (fun (n : ℕ) ↦ ((∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p) atTop)
simp_rw₁ :
  Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
    (liminf (fun (n : ℕ) ↦ (∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) ^ (1 / p * p)) atTop)
⊢ Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
    (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop)
have simp_rw₂ : Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
  (liminf (fun (n : ℕ) ↦ (∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p)) atTop)
Tactic: simp_rw [eLpNorm'_eq_lintegral_enorm, ← ENNReal.rpow_mul, one_div,
    inv_mul_cancel₀ hp_pos.ne.symm, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
h_pow_liminf :
  HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop
simp_rw :
  Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
    (liminf (fun (n : ℕ) ↦ ((∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p) atTop)
simp_rw₁ :
  Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
    (liminf (fun (n : ℕ) ↦ (∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) ^ (1 / p * p)) atTop)
simp_rw₂ :
  Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
    (liminf (fun (n : ℕ) ↦ (∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p)) atTop)
⊢ Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
    (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop)
have simp_rw₃ : Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
  (liminf (fun (n : ℕ) ↦ HPow.hPow (β := ℝ) (∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) 1) atTop)
Tactic: simp_rw [eLpNorm'_eq_lintegral_enorm, ← ENNReal.rpow_mul, one_div,
    inv_mul_cancel₀ hp_pos.ne.symm, ENNReal.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
inst_1 : Nonempty ι
inst_2 : LinearOrder ι
f : ι → α → E
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f_lim x‖ₑ) μ) (essSup (fun (x : α) ↦ liminf (fun (m : ι) ↦ ‖f m x‖ₑ) atTop) μ)
have refine : ∀ (x : α) (hx : Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (f_lim x))),
  Eq (α := ℝ≥0∞) ((fun (x : α) ↦ ‖f_lim x‖ₑ) x) ((fun (x : α) ↦ (liminf (fun (m : ι) ↦ ‖f m x‖ₑ) atTop : ℝ≥0∞)) x)
Tactic: refine essSup_congr_ae (h_lim.mono fun x hx => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
inst_1 : Nonempty ι
inst_2 : LinearOrder ι
f : ι → α → E
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (f_lim x))
x : α
hx : Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ ‖f_lim x‖ₑ = liminf (fun (m : ι) ↦ ‖f m x‖ₑ) atTop
have apply : Tendsto (fun (m : ι) ↦ ‖f m x‖ₑ) atTop (𝓝 ‖f_lim x‖ₑ)
Tactic: apply (Tendsto.liminf_eq ..).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
inst_1 : Nonempty ι
inst_2 : Countable ι
inst_3 : LinearOrder ι
f : ι → α → E
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ eLpNorm f_lim ∞ μ ≤ liminf (fun (n : ι) ↦ eLpNorm (f n) ∞ μ) atTop
have rw : LE.le (α := ℝ≥0∞) (essSup (fun (x : α) ↦ liminf (fun (m : ι) ↦ ‖f m x‖ₑ) atTop) μ)
  (liminf (fun (n : ι) ↦ eLpNorm (f n) ∞ μ) atTop)
Tactic: rw [eLpNorm_exponent_top_lim_eq_essSup_liminf h_lim]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop
have inl : eLpNorm f_lim 0 μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) 0 μ) atTop
Tactic: obtain rfl | hp0 := eq_or_ne p 0
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
inl : eLpNorm f_lim 0 μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) 0 μ) atTop
⊢ eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop
have inr : ∀ (hp0 : p ≠ 0), eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop
Tactic: obtain rfl | hp0 := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
⊢ eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop
have pos : ∀ (hp_top : p = ∞), eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
pos : ∀ (hp_top : p = ∞), eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop
⊢ eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop
have neg : ∀ (hp_top : ¬p = ∞), eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : p = ∞
⊢ eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop
have pos : eLpNorm f_lim ∞ μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) ∞ μ) atTop
Tactic: simp_rw [hp_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : ¬p = ∞
⊢ eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop
have neg : eLpNorm' f_lim p.toReal μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p.toReal μ) atTop
Tactic: simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : ¬p = ∞
⊢ eLpNorm' f_lim p.toReal μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p.toReal μ) atTop
have hp_pos : 0 < p.toReal
Tactic: have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C : ℝ≥0∞
bound : ∀ᶠ (n : ι) in u, eLpNorm (f n) p μ ≤ C
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (x_1 : ι) ↦ f x_1 x) u (𝓝 (g x))
⊢ eLpNorm g p μ ≤ C
have obtain : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), eLpNorm g p μ ≤ C
Tactic: obtain ⟨v, hv⟩ := exists_seq_tendsto u
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C : ℝ≥0∞
bound : ∀ᶠ (n : ι) in u, eLpNorm (f n) p μ ≤ C
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (x_1 : ι) ↦ f x_1 x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f (v n) x) atTop (𝓝 (g x))
have h : ∀ (x : α) (hx : Tendsto (fun (x_1 : ι) ↦ f x_1 x) u (𝓝 (g x))), Tendsto (fun (n : ℕ) ↦ f (v n) x) atTop (𝓝 (g x))
Tactic: filter_upwards [h_tendsto] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C : ℝ≥0∞
bound : ∀ᶠ (n : ι) in u, eLpNorm (f n) p μ ≤ C
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (x_1 : ι) ↦ f x_1 x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
⊢ eLpNorm g p μ ≤ C
have this : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f (v n) x) atTop (𝓝 (g x))
Tactic: have : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f (v n) x) atTop (𝓝 (g x)) := by
    filter_upwards [h_tendsto] with x hx
    exact hx.comp hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C : ℝ≥0∞
bound : ∀ᶠ (n : ι) in u, eLpNorm (f n) p μ ≤ C
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (x_1 : ι) ↦ f x_1 x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
this : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f (v n) x) atTop (𝓝 (g x))
⊢ liminf (fun (n : ℕ) ↦ eLpNorm (f (v n)) p μ) atTop ≤ C
have refine : ∀ (b : ℝ≥0∞) (hb : ∀ᶠ (n : ℕ) in atTop, b ≤ eLpNorm (f (v n)) p μ), b ≤ C
Tactic: refine liminf_le_of_le (by isBoundedDefault) (fun b hb => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C : ℝ≥0∞
bound : ∀ᶠ (n : ι) in u, eLpNorm (f n) p μ ≤ C
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (x_1 : ι) ↦ f x_1 x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
this : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f (v n) x) atTop (𝓝 (g x))
b : ℝ≥0∞
hb : ∀ᶠ (n : ℕ) in atTop, b ≤ eLpNorm (f (v n)) p μ
⊢ b ≤ C
have obtain : ∀ (n : ℕ) (hn : b ≤ eLpNorm (f (v n)) p μ ∧ eLpNorm (f (v n)) p μ ≤ C), b ≤ C
Tactic: obtain ⟨n, hn⟩ := (hb.and (hv.eventually bound)).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C : ℝ≥0∞
bound : ∀ᶠ (n : ι) in u, eLpNorm (f n) p μ ≤ C
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (x_1 : ι) ↦ f x_1 x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
this : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f (v n) x) atTop (𝓝 (g x))
⊢ eLpNorm g p μ ≤ C
have _ : liminf (fun (n : ℕ) ↦ eLpNorm (f (v n)) p μ) atTop ≤ C
Tactic: calc
  _ ≤ atTop.liminf (fun (n : ℕ) => eLpNorm (f (v n)) p μ) :=
    Lp.eLpNorm_lim_le_liminf_eLpNorm (fun n => hf (v n)) g this
  _ ≤ C := by
    refine liminf_le_of_le (by isBoundedDefault) (fun b hb => ?_)
    obtain ⟨n, hn⟩ := (hb.and (hv.eventually bound)).exists
    exact hn.1.trans hn.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst_1 : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
⊢ Tendsto f fi (𝓝 f_lim) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ)
      fi (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (b : ι) ↦ dist (f b) f_lim) fi (𝓝 0) ↔
  Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ) fi
    (𝓝 0)
Tactic: rw [tendsto_iff_dist_tendsto_zero]