α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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 ∂μ
⊢ snorm' f_lim p μ = (∫⁻ (a : α), liminf (fun m => ↑‖f m a‖₊ ^ p) atTop ∂μ) ^ (1 / p)

case h_no_pow
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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 ∂μ
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ p
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ snorm' f_lim p μ = (∫⁻ (a : α), liminf (fun m => ↑‖f m a‖₊ ^ p) atTop ∂μ) ^ (1 / p)
suffices h_no_pow :
  (∫⁻ a, (‖f_lim a‖₊ : ℝ≥0∞) ^ p ∂μ) = ∫⁻ a, atTop.liminf fun m => (‖f m a‖₊ : ℝ≥0∞) ^ p ∂μ
case h_no_pow
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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
case h_no_pow
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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 ∂μ
refine' lintegral_congr_ae (h_lim.mono fun a ha => _)
case h_no_pow
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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
case h_no_pow
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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
dsimp only
case h_no_pow
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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))
case h_no_pow
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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
rw [Tendsto.liminf_eq]
case h_no_pow
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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 a_1 => ‖f a_1 a‖₊ ^ p) atTop (𝓝 (‖f_lim a‖₊ ^ p))
case h_no_pow
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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))
simp_rw [ENNReal.coe_rpow_of_nonneg _ hp_nonneg, ENNReal.tendsto_coe]
case h_no_pow
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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 a_1 => ‖f a_1 a‖₊) atTop (𝓝 ‖f_lim a‖₊)
case h_no_pow
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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 a_1 => ‖f a_1 a‖₊ ^ p) atTop (𝓝 (‖f_lim a‖₊ ^ p))
refine' ((NNReal.continuous_rpow_const hp_nonneg).tendsto ‖f_lim a‖₊).comp _
no goals
case h_no_pow
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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 a_1 => ‖f a_1 a‖₊) atTop (𝓝 ‖f_lim a‖₊)
exact (continuous_nnnorm.tendsto (f_lim a)).comp ha
no goals
α : Type u_2
E : Type ?u.8103735
F : Type ?u.8103738
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
p : ℝ
hp_nonneg : 0 ≤ 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 ∂μ
⊢ snorm' f_lim p μ = (∫⁻ (a : α), liminf (fun m => ↑‖f m a‖₊ ^ p) atTop ∂μ) ^ (1 / p)
rw [snorm', h_no_pow]