-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem eLpNorm'_lim_le_liminf_eLpNorm' {E} [NormedAddCommGroup 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))) :
    eLpNorm' f_lim p μ ≤ atTop.liminf fun n => eLpNorm' (f n) p μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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))
⊢ eLpNorm' f_lim p μ ≤ liminf (fun n => eLpNorm' (f n) p μ) atTop

Tactic:
rw [eLpNorm'_lim_eq_lintegral_liminf h_lim]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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 ∂μ) ^ (1 / p) ≤ liminf (fun n => eLpNorm' (f n) p μ) atTop

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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 ∂μ) ^ (1 / p) ≤ liminf (fun n => eLpNorm' (f n) p μ) atTop

Tactic:
rw [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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 ∂μ ≤ liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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 n => eLpNorm' (f n) p μ) atTop ^ p = liminf (fun n => eLpNorm' (f n) p μ ^ p) atTop

Tactic:
have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hp_pos

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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 fun x => x ^ p
⊢ liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p = liminf (fun n => eLpNorm' (f n) p μ ^ p) atTop

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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 ∂μ ≤ liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p

Tactic:
refine (lintegral_liminf_le' fun m => (hf m).enorm.pow_const _).trans_eq ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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 n => ∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) atTop = liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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 n => ∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) atTop = liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p

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

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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 : liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p = liminf (fun n => eLpNorm' (f n) p μ ^ p) atTop
⊢ liminf (fun n => ∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) atTop = liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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 : liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p = liminf (fun n => eLpNorm' (f n) p μ ^ p) atTop
⊢ liminf (fun n => ∫⁻ (a : α), ‖f n 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]

Result:
no goals