α : Type u_1
β : Type u_2
γ : Type ?u.1306428
δ : Type ?u.1306431
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ (∫⁻ (x : α), edist (↑↑(f - g) x) 0 ∂μ) = ∫⁻ (x : α), edist (↑↑f x - ↑↑g x) 0 ∂μ
α : Type u_1
β : Type u_2
γ : Type ?u.1306428
δ : Type ?u.1306431
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ ENNReal.ofReal ‖f - g‖ = ∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ
simp_rw [ofReal_norm_eq_lintegral, ← edist_eq_coe_nnnorm]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.1306428
δ : Type ?u.1306431
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ (fun a => edist (↑↑(f - g) a) 0) =ᵐ[μ] fun a => edist (↑↑f a - ↑↑g a) 0
α : Type u_1
β : Type u_2
γ : Type ?u.1306428
δ : Type ?u.1306431
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ (∫⁻ (x : α), edist (↑↑(f - g) x) 0 ∂μ) = ∫⁻ (x : α), edist (↑↑f x - ↑↑g x) 0 ∂μ
apply lintegral_congr_ae
case h
α : Type u_1
β : Type u_2
γ : Type ?u.1306428
δ : Type ?u.1306431
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
a✝ : α
ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝
⊢ edist (↑↑(f - g) a✝) 0 = edist (↑↑f a✝ - ↑↑g a✝) 0
case h
α : Type u_1
β : Type u_2
γ : Type ?u.1306428
δ : Type ?u.1306431
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ (fun a => edist (↑↑(f - g) a) 0) =ᵐ[μ] fun a => edist (↑↑f a - ↑↑g a) 0
filter_upwards [Lp.coeFn_sub f g] with _ ha
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.1306428
δ : Type ?u.1306431
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
a✝ : α
ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝
⊢ edist (↑↑(f - g) a✝) 0 = edist (↑↑f a✝ - ↑↑g a✝) 0
simp only [ha, Pi.sub_apply]