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

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Tactic:
obtain rfl|hp0 := eq_or_ne p 0

Result:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

case inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Proof state:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Result:
no goals

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Result:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Tactic:
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top

Result:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Result:
no goals

Proof state:
case inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Tactic:
by_cases hp_top : p = ∞

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Tactic:
simp_rw [hp_top]

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup 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

Result:
no goals