-- 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))
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

Tactic:
have h_rpow_surj := (ENNReal.rpow_left_bijective hp_pos.ne.symm).2

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
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p = liminf (fun n => eLpNorm' (f n) p μ ^ p) atTop

Proof state:
case refine_4
α : 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
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun x =>
    (StrictMono.orderIsoOfSurjective (fun x => x ^ p) h_rpow_mono h_rpow_surj) (eLpNorm' (f x) p μ)

Tactic:
isBoundedDefault

Result:
no goals

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))
⊢ 0 < p⁻¹

Tactic:
simp [hp_pos]

Result:
no goals

Proof state:
case refine_1
α : 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
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun n => eLpNorm' (f n) p μ

case refine_2
α : 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
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun n => eLpNorm' (f n) p μ

case refine_3
α : 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
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun x =>
    (StrictMono.orderIsoOfSurjective (fun x => x ^ p) h_rpow_mono h_rpow_surj) (eLpNorm' (f x) p μ)

case refine_4
α : 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
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun x =>
    (StrictMono.orderIsoOfSurjective (fun x => x ^ p) h_rpow_mono h_rpow_surj) (eLpNorm' (f x) p μ)

Tactic:
all_goals isBoundedDefault

Result:
no goals

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 μ) atTop ^ p

Tactic:
rw [h_pow_liminf]

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 μ ^ 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))
h_rpow_mono : StrictMono fun x => x ^ p
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ liminf (fun n => eLpNorm' (f n) p μ) atTop ^ p = liminf (fun n => eLpNorm' (f n) p μ ^ p) atTop

Tactic:
refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_

Result:
case refine_1
α : 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
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun n => eLpNorm' (f n) p μ

case refine_2
α : 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
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun n => eLpNorm' (f n) p μ

case refine_3
α : 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
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun x =>
    (StrictMono.orderIsoOfSurjective (fun x => x ^ p) h_rpow_mono h_rpow_surj) (eLpNorm' (f x) p μ)

case refine_4
α : 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
h_rpow_surj : Function.Surjective fun y => y ^ p
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun x =>
    (StrictMono.orderIsoOfSurjective (fun x => x ^ p) h_rpow_mono h_rpow_surj) (eLpNorm' (f x) p μ)