awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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
rw :
  Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
    (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

Tactic:
rw [h_pow_liminf]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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)
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)
⊢ Eq (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop)
    (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) 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]

Premises used: ENNReal.rpow_mul, ENNReal.rpow_one, Ne.symm, one_div, MeasureTheory.eLpNorm'_eq_lintegral_enorm, inv_mul_cancel₀, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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) μ)

Tactic:
essSup_congr_ae (h_lim.mono fun x hx => ?_)

Premises used: Filter.Eventually.mono, essSup_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
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)
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f_lim x‖ₑ) μ) (essSup (fun (x : α) ↦ liminf (fun (m : ι) ↦ ‖f m x‖ₑ) atTop) μ)

Tactic:
refine essSup_congr_ae (h_lim.mono fun x hx => ?_)

Premises used: Filter.Eventually.mono, essSup_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
apply : Tendsto (fun (m : ι) ↦ ‖f m x‖ₑ) atTop (𝓝 ‖f_lim x‖ₑ)
⊢ ‖f_lim x‖ₑ = liminf (fun (m : ι) ↦ ‖f m x‖ₑ) atTop

Tactic:
apply (Tendsto.liminf_eq ..).symm

Premises used: Filter.Tendsto.liminf_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
⊢ Tendsto (fun (m : ι) ↦ ‖f m x‖ₑ) atTop (𝓝 ‖f_lim x‖ₑ)

Tactic:
(continuous_enorm.tendsto (f_lim x)).comp hx

Premises used: continuous_enorm, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
⊢ Tendsto (fun (m : ι) ↦ ‖f m x‖ₑ) atTop (𝓝 ‖f_lim x‖ₑ)

Tactic:
exact (continuous_enorm.tendsto (f_lim x)).comp hx

Premises used: continuous_enorm, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
rw :
  LE.le (α := ℝ≥0∞) (essSup (fun (x : α) ↦ liminf (fun (m : ι) ↦ ‖f m x‖ₑ) atTop) μ)
    (liminf (fun (n : ι) ↦ eLpNorm (f n) ∞ μ) atTop)
⊢ eLpNorm f_lim ∞ μ ≤ liminf (fun (n : ι) ↦ eLpNorm (f n) ∞ μ) atTop

Tactic:
rw [eLpNorm_exponent_top_lim_eq_essSup_liminf h_lim]

Premises used: MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
⊢ LE.le (α := ℝ≥0∞) (essSup (fun (x : α) ↦ liminf (fun (m : ι) ↦ ‖f m x‖ₑ) atTop) μ)
    (liminf (fun (n : ι) ↦ essSup (fun (x : α) ↦ ‖f n x‖ₑ) μ) atTop)

Tactic:
ENNReal.essSup_liminf_le _

Premises used: ENNReal.essSup_liminf_le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
⊢ LE.le (α := ℝ≥0∞) (essSup (fun (x : α) ↦ liminf (fun (m : ι) ↦ ‖f m x‖ₑ) atTop) μ)
    (liminf (fun (n : ι) ↦ essSup (fun (x : α) ↦ ‖f n x‖ₑ) μ) atTop)

Tactic:
exact ENNReal.essSup_liminf_le _

Premises used: ENNReal.essSup_liminf_le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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
inr : ∀ (hp0 : p ≠ 0), eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop
⊢ eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop

Tactic:
obtain rfl | hp0 := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : 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 0 μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) 0 μ) atTop

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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
neg : ∀ (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

Tactic:
by_cases hp_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 = ∞
pos : eLpNorm f_lim ∞ μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) ∞ μ) atTop
⊢ eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop

Tactic:
simp_rw [hp_top]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 ∞ μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) ∞ μ) atTop

Tactic:
eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top h_lim

Premises used: MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 ∞ μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) ∞ μ) atTop

Tactic:
exact eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top h_lim

Premises used: MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 = ∞
neg : eLpNorm' f_lim p.toReal μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p.toReal μ) atTop
⊢ eLpNorm f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f n) p μ) atTop

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 = ∞
⊢ 0 < p.toReal

Tactic:
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 = ∞
hp_pos : 0 < p.toReal
⊢ eLpNorm' f_lim p.toReal μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p.toReal μ) atTop

Tactic:
eLpNorm'_lim_le_liminf_eLpNorm' hp_pos hf h_lim

Premises used: MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 = ∞
hp_pos : 0 < p.toReal
⊢ eLpNorm' f_lim p.toReal μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p.toReal μ) atTop

Tactic:
exact eLpNorm'_lim_le_liminf_eLpNorm' hp_pos hf h_lim

Premises used: MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
obtain : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), eLpNorm g p μ ≤ C
⊢ eLpNorm g p μ ≤ C

Tactic:
obtain ⟨v, hv⟩ := exists_seq_tendsto u

Premises used: Filter.exists_seq_tendsto
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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
h : ∀ (x : α) (hx : Tendsto (fun (x_1 : ι) ↦ f x_1 x) u (𝓝 (g x))), Tendsto (fun (n : ℕ) ↦ f (v n) x) atTop (𝓝 (g x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f (v n) x) atTop (𝓝 (g x))

Tactic:
filter_upwards [h_tendsto] with x hx
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 : α
hx : Tendsto (fun (x_1 : ι) ↦ f x_1 x) u (𝓝 (g x))
⊢ Tendsto (fun (n : ℕ) ↦ f (v n) x) atTop (𝓝 (g x))

Tactic:
hx.comp hv

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 : α
hx : Tendsto (fun (x_1 : ι) ↦ f x_1 x) u (𝓝 (g x))
⊢ Tendsto (fun (n : ℕ) ↦ f (v n) x) atTop (𝓝 (g x))

Tactic:
exact hx.comp hv

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))

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
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm (f (v n)) p μ) atTop

Tactic:
Lp.eLpNorm_lim_le_liminf_eLpNorm (fun n => hf (v n)) g this

Premises used: MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ eLpNorm (f (v n)) p μ

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
refine : ∀ (b : ℝ≥0∞) (hb : ∀ᶠ (n : ℕ) in atTop, b ≤ eLpNorm (f (v n)) p μ), b ≤ C
⊢ liminf (fun (n : ℕ) ↦ eLpNorm (f (v n)) p μ) atTop ≤ C

Tactic:
refine liminf_le_of_le (by isBoundedDefault) (fun b hb => ?_)

Premises used: Filter.liminf_le_of_le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 μ
obtain : ∀ (n : ℕ) (hn : b ≤ eLpNorm (f (v n)) p μ ∧ eLpNorm (f (v n)) p μ ≤ C), b ≤ C
⊢ b ≤ C

Tactic:
obtain ⟨n, hn⟩ := (hb.and (hv.eventually bound)).exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists, Filter.Tendsto.eventually
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 μ
n : ℕ
hn : b ≤ eLpNorm (f (v n)) p μ ∧ eLpNorm (f (v n)) p μ ≤ C
⊢ b ≤ C

Tactic:
hn.1.trans hn.2

Premises used: And.right, And.left, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 μ
n : ℕ
hn : b ≤ eLpNorm (f (v n)) p μ ∧ eLpNorm (f (v n)) p μ ≤ C
⊢ b ≤ C

Tactic:
exact hn.1.trans hn.2

Premises used: And.right, And.left, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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
⊢ eLpNorm g p μ ≤ 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

Premises used: Filter.liminf, MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm, Filter.atTop, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 μ)
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)
⊢ Tendsto f fi (𝓝 f_lim) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ)
      fi (𝓝 0)

Tactic:
rw [tendsto_iff_dist_tendsto_zero]

Premises used: tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 μ)
simp_rw :
  Tendsto (β := ℝ)
      (fun (b : ι) ↦ (eLpNorm ((↑(↑(f b) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ).toReal) fi
      (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ)
      fi (𝓝 0)
⊢ 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:
simp_rw [dist_def]

Premises used: MeasureTheory.Lp.dist_def
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 μ)
rw : ∀ (n : ι), eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ ≠ ∞
⊢ Tendsto (β := ℝ)
      (fun (b : ι) ↦ (eLpNorm ((↑(↑(f b) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ).toReal) fi
      (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ)
      fi (𝓝 0)

Tactic:
rw [← ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]

Premises used: ENNReal.zero_ne_top, ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 μ)
n : ι
rw : eLpNorm (↑(↑(f n - f_lim) : α →ₘ[μ] E) : α → E) p μ ≠ ∞
⊢ eLpNorm ((↑(↑(f n) : α →ₘ[μ] E) : α → E) - (↑(↑f_lim : α →ₘ[μ] E) : α → E)) p μ ≠ ∞

Tactic:
rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]

Premises used: MeasureTheory.Lp.coeFn_sub, MeasureTheory.eLpNorm_congr_ae, Filter.EventuallyEq.symm