case pos
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : p = ⊤
⊢ TendstoInMeasure μ f l g

case neg
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : ¬p = ⊤
⊢ TendstoInMeasure μ f l g
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g
by_cases hp_ne_top : p = ∞
case pos
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hp_ne_zero : ⊤ ≠ 0
hfg : Tendsto (fun n => snorm (f n - g) ⊤ μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g
case pos
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : p = ⊤
⊢ TendstoInMeasure μ f l g
subst hp_ne_top
no goals
case pos
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hp_ne_zero : ⊤ ≠ 0
hfg : Tendsto (fun n => snorm (f n - g) ⊤ μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g
exact tendstoInMeasure_of_tendsto_snorm_top hfg
no goals
case neg
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => snorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : ¬p = ⊤
⊢ TendstoInMeasure μ f l g
exact tendstoInMeasure_of_tendsto_snorm_of_ne_top hp_ne_zero hp_ne_top hf hg hfg