-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem eLpNorm'_lim_eq_lintegral_liminf {ι} [Nonempty ι] [LinearOrder ι] {f : ι → α → G} {p : ℝ}
    {f_lim : α → G} (h_lim : ∀ᵐ x : α ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))) :
    eLpNorm' f_lim p μ = (∫⁻ a, atTop.liminf (‖f · a‖ₑ ^ p) ∂μ) ^ (1 / p)

Proof state:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
a : α
ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))
⊢ Tendsto (fun m => ‖f m a‖ₑ) atTop (𝓝 ↑‖f_lim a‖₊)

Tactic:
exact (continuous_enorm.tendsto (f_lim a)).comp ha

Result:
no goals

Proof state:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
a : α
ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))
⊢ Tendsto (fun m => ‖f m a‖ₑ ^ p) atTop (𝓝 (‖f_lim a‖ₑ ^ p))

Tactic:
refine (ENNReal.continuous_rpow_const.tendsto ‖f_lim a‖₊).comp ?_

Result:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
a : α
ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))
⊢ Tendsto (fun m => ‖f m a‖ₑ) atTop (𝓝 ↑‖f_lim a‖₊)

Proof state:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ ∫⁻ (a : α), ‖f_lim a‖ₑ ^ p ∂μ = ∫⁻ (a : α), liminf (fun m => ‖f m a‖ₑ ^ p) atTop ∂μ

Tactic:
refine lintegral_congr_ae (h_lim.mono fun a ha => ?_)

Result:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
a : α
ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))
⊢ (fun a => ‖f_lim a‖ₑ ^ p) a = (fun a => liminf (fun m => ‖f m a‖ₑ ^ p) atTop) a

Proof state:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
a : α
ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))
⊢ (fun a => ‖f_lim a‖ₑ ^ p) a = (fun a => liminf (fun m => ‖f m a‖ₑ ^ p) atTop) a

Tactic:
dsimp only

Result:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
a : α
ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))
⊢ ‖f_lim a‖ₑ ^ p = liminf (fun m => ‖f m a‖ₑ ^ p) atTop

Proof state:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
a : α
ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))
⊢ ‖f_lim a‖ₑ ^ p = liminf (fun m => ‖f m a‖ₑ ^ p) atTop

Tactic:
rw [Tendsto.liminf_eq]

Result:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
a : α
ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))
⊢ Tendsto (fun m => ‖f m a‖ₑ ^ p) atTop (𝓝 (‖f_lim a‖ₑ ^ p))

Proof state:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
h_no_pow : ∫⁻ (a : α), ‖f_lim a‖ₑ ^ p ∂μ = ∫⁻ (a : α), liminf (fun m => ‖f m a‖ₑ ^ p) atTop ∂μ
⊢ eLpNorm' f_lim p μ = (∫⁻ (a : α), liminf (fun x => ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p)

Tactic:
rw [eLpNorm'_eq_lintegral_enorm, h_no_pow]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ eLpNorm' f_lim p μ = (∫⁻ (a : α), liminf (fun x => ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p)

Tactic:
suffices h_no_pow : (∫⁻ a, ‖f_lim a‖ₑ ^ p ∂μ) = ∫⁻ a, atTop.liminf fun m => ‖f m a‖ₑ ^ p ∂μ by
  rw [eLpNorm'_eq_lintegral_enorm, h_no_pow]

Result:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ ∫⁻ (a : α), ‖f_lim a‖ₑ ^ p ∂μ = ∫⁻ (a : α), liminf (fun m => ‖f m a‖ₑ ^ p) atTop ∂μ