α : Type u_1
E : Type ?u.1276212
F : Type u_2
G : Type ?u.1276218
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → F
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
this : (fun x => ↑‖f x‖₊ ^ q) =ᵐ[μ] fun x => ↑‖g x‖₊ ^ q
⊢ snorm' f q μ = snorm' g q μ
α : Type u_1
E : Type ?u.1276212
F : Type u_2
G : Type ?u.1276218
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → F
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
⊢ snorm' f q μ = snorm' g q μ
have : (fun x => (‖f x‖₊ : ℝ≥0∞) ^ q) =ᵐ[μ] fun x => (‖g x‖₊ : ℝ≥0∞) ^ q :=
  hfg.mono fun x hx => by simp_rw [hx]
no goals
α : Type u_1
E : Type ?u.1276212
F : Type u_2
G : Type ?u.1276218
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → F
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
this : (fun x => ↑‖f x‖₊ ^ q) =ᵐ[μ] fun x => ↑‖g x‖₊ ^ q
⊢ snorm' f q μ = snorm' g q μ
simp only [snorm', lintegral_congr_ae this]
no goals
α : Type u_1
E : Type ?u.1276212
F : Type u_2
G : Type ?u.1276218
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : α → F
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
x : α
hx : ‖f x‖₊ = ‖g x‖₊
⊢ (fun x => ↑‖f x‖₊ ^ q) x = (fun x => ↑‖g x‖₊ ^ q) x
simp_rw [hx]