α : Type u_1
β : Type u_2
γ : Type ?u.1303508
δ : Type ?u.1303511
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑(f - g) a‖₊ ∂μ) = ENNReal.toReal (∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ)
α : Type u_1
β : Type u_2
γ : Type ?u.1303508
δ : Type ?u.1303511
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ ‖f - g‖ = ENNReal.toReal (∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ)
rw [norm_def]
case e_a
α : Type u_1
β : Type u_2
γ : Type ?u.1303508
δ : Type ?u.1303511
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ (∫⁻ (a : α), ↑‖↑↑(f - g) a‖₊ ∂μ) = ∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ
α : Type u_1
β : Type u_2
γ : Type ?u.1303508
δ : Type ?u.1303511
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑(f - g) a‖₊ ∂μ) = ENNReal.toReal (∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ)
congr 1
case e_a
α : Type u_1
β : Type u_2
γ : Type ?u.1303508
δ : Type ?u.1303511
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ (fun a => ↑‖↑↑(f - g) a‖₊) =ᵐ[μ] fun a => ↑‖↑↑f a - ↑↑g a‖₊
case e_a
α : Type u_1
β : Type u_2
γ : Type ?u.1303508
δ : Type ?u.1303511
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ (∫⁻ (a : α), ↑‖↑↑(f - g) a‖₊ ∂μ) = ∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ
rw [lintegral_congr_ae]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.1303508
δ : Type ?u.1303511
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
a✝ : α
ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝
⊢ ↑‖↑↑(f - g) a✝‖₊ = ↑‖↑↑f a✝ - ↑↑g a✝‖₊
case e_a
α : Type u_1
β : Type u_2
γ : Type ?u.1303508
δ : Type ?u.1303511
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
⊢ (fun a => ↑‖↑↑(f - g) a‖₊) =ᵐ[μ] fun a => ↑‖↑↑f a - ↑↑g a‖₊
filter_upwards [Lp.coeFn_sub f g] with _ ha
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.1303508
δ : Type ?u.1303511
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f g : { x // x ∈ Lp β 1 }
a✝ : α
ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝
⊢ ↑‖↑↑(f - g) a✝‖₊ = ↑‖↑↑f a✝ - ↑↑g a✝‖₊
simp only [ha, Pi.sub_apply]