α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ snorm f p μ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹)
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
⊢ snorm f p μ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹)
have A : (∫⁻ a : α, ENNReal.ofReal (‖f a‖ ^  p.toReal) ∂μ) = ∫⁻ a : α, ‖f a‖₊ ^ p.toReal ∂μ := by
  apply lintegral_congr
  intro x
  rw [← ofReal_rpow_of_nonneg (norm_nonneg _) toReal_nonneg, ofReal_norm_eq_coe_nnnorm,
    ← ENNReal.coe_rpow_of_nonneg _ toReal_nonneg]
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹ =
    ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹)
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ snorm f p μ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹)
simp only [snorm_eq_lintegral_rpow_nnnorm hp1 hp2, one_div]
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹ =
    ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) ^ (ENNReal.toReal p)⁻¹)

case hf
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ 0 ≤ᵐ[μ] fun a => ‖f a‖ ^ ENNReal.toReal p

case hfm
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ AEStronglyMeasurable (fun a => ‖f a‖ ^ ENNReal.toReal p) μ
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹ =
    ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹)
rw [integral_eq_lintegral_of_nonneg_ae]
case hf
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ 0 ≤ᵐ[μ] fun a => ‖f a‖ ^ ENNReal.toReal p

case hfm
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ AEStronglyMeasurable (fun a => ‖f a‖ ^ ENNReal.toReal p) μ

α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹ =
    ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) ^ (ENNReal.toReal p)⁻¹)
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹ =
    ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) ^ (ENNReal.toReal p)⁻¹)

case hf
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ 0 ≤ᵐ[μ] fun a => ‖f a‖ ^ ENNReal.toReal p

case hfm
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ AEStronglyMeasurable (fun a => ‖f a‖ ^ ENNReal.toReal p) μ
rotate_left
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹ =
    (∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ) ^ (ENNReal.toReal p)⁻¹

α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ (∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ) ≠ ⊤
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹ =
    ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) ^ (ENNReal.toReal p)⁻¹)
rw [A, ← ofReal_rpow_of_nonneg toReal_nonneg (inv_nonneg.2 toReal_nonneg), ofReal_toReal]
case h
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
⊢ ∀ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) = ↑(‖f a‖₊ ^ ENNReal.toReal p)
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
apply lintegral_congr
case h
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
x : α
⊢ ENNReal.ofReal (‖f x‖ ^ ENNReal.toReal p) = ↑(‖f x‖₊ ^ ENNReal.toReal p)
case h
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
⊢ ∀ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) = ↑(‖f a‖₊ ^ ENNReal.toReal p)
intro x
no goals
case h
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
x : α
⊢ ENNReal.ofReal (‖f x‖ ^ ENNReal.toReal p) = ↑(‖f x‖₊ ^ ENNReal.toReal p)
rw [← ofReal_rpow_of_nonneg (norm_nonneg _) toReal_nonneg, ofReal_norm_eq_coe_nnnorm,
  ← ENNReal.coe_rpow_of_nonneg _ toReal_nonneg]
no goals
case hf
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ 0 ≤ᵐ[μ] fun a => ‖f a‖ ^ ENNReal.toReal p
exact eventually_of_forall fun x => Real.rpow_nonneg_of_nonneg (norm_nonneg _) _
no goals
case hfm
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ AEStronglyMeasurable (fun a => ‖f a‖ ^ ENNReal.toReal p) μ
exact (hf.aestronglyMeasurable.norm.aemeasurable.pow_const _).aestronglyMeasurable
no goals
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹ =
    (∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ) ^ (ENNReal.toReal p)⁻¹
simp_rw [← ENNReal.coe_rpow_of_nonneg _ toReal_nonneg]
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ (∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ) ≠ ⊤
simp_rw [← ENNReal.coe_rpow_of_nonneg _ toReal_nonneg]
no goals
α : Type u_2
E : Type ?u.1137869
F : Type ?u.1137872
𝕜 : Type ?u.1137875
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1140566
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
H : Type u_1
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ⊤
hf : Memℒp f p
A : (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ ENNReal.toReal p) ∂μ) = ∫⁻ (a : α), ↑(‖f a‖₊ ^ ENNReal.toReal p) ∂μ
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
exact (lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top hp1 hp2 hf.2).ne