pub fn square_function_ty() -> Expr
SquareFunction : (n : Nat) → LpSpace p n → Real
The Littlewood-Paley square function: S(f)(x) = (Σⱼ |Δⱼf(x)|²)^{1/2}.