α : Type u_1
β : Type ?u.1108791
ι : Type ?u.1108794
E : Type ?u.1108797
F : Type u_2
𝕜 : Type ?u.1108803
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ✝ : Measure α
p✝ : ℝ≥0∞
p : ℝ
f : α →ₛ F
μ : Measure α
h_map : (fun a => ↑‖↑f a‖₊ ^ p) = ↑(map (fun a => ↑‖a‖₊ ^ p) f)
⊢ snorm' (↑f) p μ = (∑ y in SimpleFunc.range f, ↑‖y‖₊ ^ p * ↑↑μ (↑f ⁻¹' {y})) ^ (1 / p)
α : Type u_1
β : Type ?u.1108791
ι : Type ?u.1108794
E : Type ?u.1108797
F : Type u_2
𝕜 : Type ?u.1108803
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ✝ : Measure α
p✝ : ℝ≥0∞
p : ℝ
f : α →ₛ F
μ : Measure α
⊢ snorm' (↑f) p μ = (∑ y in SimpleFunc.range f, ↑‖y‖₊ ^ p * ↑↑μ (↑f ⁻¹' {y})) ^ (1 / p)
have h_map : (fun a => (‖f a‖₊ : ℝ≥0∞) ^ p) = f.map fun a : F => (‖a‖₊ : ℝ≥0∞) ^ p := by
  simp; rfl
no goals
α : Type u_1
β : Type ?u.1108791
ι : Type ?u.1108794
E : Type ?u.1108797
F : Type u_2
𝕜 : Type ?u.1108803
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ✝ : Measure α
p✝ : ℝ≥0∞
p : ℝ
f : α →ₛ F
μ : Measure α
h_map : (fun a => ↑‖↑f a‖₊ ^ p) = ↑(map (fun a => ↑‖a‖₊ ^ p) f)
⊢ snorm' (↑f) p μ = (∑ y in SimpleFunc.range f, ↑‖y‖₊ ^ p * ↑↑μ (↑f ⁻¹' {y})) ^ (1 / p)
rw [snorm', h_map, lintegral_eq_lintegral, map_lintegral]
α : Type u_1
β : Type ?u.1108791
ι : Type ?u.1108794
E : Type ?u.1108797
F : Type u_2
𝕜 : Type ?u.1108803
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ✝ : Measure α
p✝ : ℝ≥0∞
p : ℝ
f : α →ₛ F
μ : Measure α
⊢ (fun a => ↑‖↑f a‖₊ ^ p) = (fun a => ↑‖a‖₊ ^ p) ∘ ↑f
α : Type u_1
β : Type ?u.1108791
ι : Type ?u.1108794
E : Type ?u.1108797
F : Type u_2
𝕜 : Type ?u.1108803
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ✝ : Measure α
p✝ : ℝ≥0∞
p : ℝ
f : α →ₛ F
μ : Measure α
⊢ (fun a => ↑‖↑f a‖₊ ^ p) = ↑(map (fun a => ↑‖a‖₊ ^ p) f)
simp
no goals
α : Type u_1
β : Type ?u.1108791
ι : Type ?u.1108794
E : Type ?u.1108797
F : Type u_2
𝕜 : Type ?u.1108803
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ✝ : Measure α
p✝ : ℝ≥0∞
p : ℝ
f : α →ₛ F
μ : Measure α
⊢ (fun a => ↑‖↑f a‖₊ ^ p) = (fun a => ↑‖a‖₊ ^ p) ∘ ↑f
rfl