`BookProof.ScalaronDensitized.integral_norm_sq_eq_norm_sq` (mu : Measure X) (f : Lp ℂ 2 mu) : ∫ a, ‖(f : X → ℂ) a‖ ^ 2 ∂mu = ‖f‖ ^ 2

Initializing...

`BookProof.ScalaronDensitized.integral_norm_sq_eq_norm_sq` (mu : Measure X) (f : Lp ℂ 2 mu) : ∫ a, ‖(f : X → ℂ) a‖ ^ 2 ∂mu = ‖f‖ ^ 2 · Prove2Me