α : Type u_3
E : Type u_2
F : Type ?u.8128143
G : Type ?u.8128146
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), Memℒp (f n) p
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
⊢ Tendsto (fun n => snorm (↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p)) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n => snorm (f n - f_lim) p μ) fi (𝓝 0)
α : Type u_3
E : Type u_2
F : Type ?u.8128143
G : Type ?u.8128146
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), Memℒp (f n) p
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
⊢ Tendsto (fun n => Memℒp.toLp (f n) (_ : Memℒp (f n) p)) fi (𝓝 (Memℒp.toLp f_lim f_lim_ℒp)) ↔
    Tendsto (fun n => snorm (f n - f_lim) p μ) fi (𝓝 0)
rw [Lp.tendsto_Lp_iff_tendsto_ℒp' (fun n => (f_ℒp n).toLp (f n)) (f_lim_ℒp.toLp f_lim)]
α : Type u_3
E : Type u_2
F : Type ?u.8128143
G : Type ?u.8128146
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), Memℒp (f n) p
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
n : ι
⊢ snorm (↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p)) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ = snorm (f n - f_lim) p μ
α : Type u_3
E : Type u_2
F : Type ?u.8128143
G : Type ?u.8128146
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), Memℒp (f n) p
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
⊢ Tendsto (fun n => snorm (↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p)) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n => snorm (f n - f_lim) p μ) fi (𝓝 0)
refine Filter.tendsto_congr fun n => ?_
case hfg
α : Type u_3
E : Type u_2
F : Type ?u.8128143
G : Type ?u.8128146
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), Memℒp (f n) p
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
n : ι
⊢ ↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p)) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp) =ᵐ[μ] f n - f_lim
α : Type u_3
E : Type u_2
F : Type ?u.8128143
G : Type ?u.8128146
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), Memℒp (f n) p
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
n : ι
⊢ snorm (↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p)) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) p μ = snorm (f n - f_lim) p μ
apply snorm_congr_ae
case h
α : Type u_3
E : Type u_2
F : Type ?u.8128143
G : Type ?u.8128146
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), Memℒp (f n) p
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
n : ι
a✝ : α
hx₁ : ↑↑(Memℒp.toLp (f n - f_lim) (_ : Memℒp (f n - f_lim) p)) a✝ = (f n - f_lim) a✝
hx₂ :
  ↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p) - Memℒp.toLp f_lim f_lim_ℒp) a✝ =
    (↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p)) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) a✝
⊢ (↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p)) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) a✝ = (f n - f_lim) a✝
case hfg
α : Type u_3
E : Type u_2
F : Type ?u.8128143
G : Type ?u.8128146
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), Memℒp (f n) p
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
n : ι
⊢ ↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p)) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp) =ᵐ[μ] f n - f_lim
filter_upwards [((f_ℒp n).sub f_lim_ℒp).coeFn_toLp,
  Lp.coeFn_sub ((f_ℒp n).toLp (f n)) (f_lim_ℒp.toLp f_lim)] with _ hx₁ hx₂
case h
α : Type u_3
E : Type u_2
F : Type ?u.8128143
G : Type ?u.8128146
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), Memℒp (f n) p
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
n : ι
a✝ : α
hx₁ : ↑↑(Memℒp.toLp (f n - f_lim) (_ : Memℒp (f n - f_lim) p)) a✝ = (f n - f_lim) a✝
hx₂ :
  ↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p) - Memℒp.toLp f_lim f_lim_ℒp) a✝ =
    (↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p)) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) a✝
⊢ ↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p) - Memℒp.toLp f_lim f_lim_ℒp) a✝ = (f n - f_lim) a✝
case h
α : Type u_3
E : Type u_2
F : Type ?u.8128143
G : Type ?u.8128146
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), Memℒp (f n) p
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
n : ι
a✝ : α
hx₁ : ↑↑(Memℒp.toLp (f n - f_lim) (_ : Memℒp (f n - f_lim) p)) a✝ = (f n - f_lim) a✝
hx₂ :
  ↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p) - Memℒp.toLp f_lim f_lim_ℒp) a✝ =
    (↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p)) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) a✝
⊢ (↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p)) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) a✝ = (f n - f_lim) a✝
rw [← hx₂]
no goals
case h
α : Type u_3
E : Type u_2
F : Type ?u.8128143
G : Type ?u.8128146
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
ι : Type u_1
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → α → E
f_ℒp : ∀ (n : ι), Memℒp (f n) p
f_lim : α → E
f_lim_ℒp : Memℒp f_lim p
n : ι
a✝ : α
hx₁ : ↑↑(Memℒp.toLp (f n - f_lim) (_ : Memℒp (f n - f_lim) p)) a✝ = (f n - f_lim) a✝
hx₂ :
  ↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p) - Memℒp.toLp f_lim f_lim_ℒp) a✝ =
    (↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p)) - ↑↑(Memℒp.toLp f_lim f_lim_ℒp)) a✝
⊢ ↑↑(Memℒp.toLp (f n) (_ : Memℒp (f n) p) - Memℒp.toLp f_lim f_lim_ℒp) a✝ = (f n - f_lim) a✝
exact hx₁