feat: notation for vectors in Euclidean space (#17732)

This adds `!₂[1, 2, 3]` notation for `(WithLp.equiv 2 (∀ _ : Fin 3, _)).symm ![1, 2, 3]`, which is a term of type `EuclideanSpace 𝕜 (Fin 3)`; and more generally for other Lp norms, using the `subscript` parser.

This reduces the temptation to write the type-incorrect `![1, 2, 3]` that has the wrong norm.

The (parser for the) `subscript` parser relies on `initialize`rs running, and so a missing `Lean.enableInitializersExecution` has to be inserted in `checkYaml.lean`. It has already been inserted in the necessary places in upstream repos.

[Notation Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Notation.20for.20vectors.20in.20euclidean.20space/near/476796192).



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: eric-wieser

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -7,6 +7,7 @@ import Mathlib.Analysis.InnerProductSpace.Projection
 import Mathlib.Analysis.Normed.Lp.PiLp
 import Mathlib.LinearAlgebra.FiniteDimensional
 import Mathlib.LinearAlgebra.UnitaryGroup
+import Mathlib.Util.Superscript
 
 /-!
 # `L²` inner product space structure on finite products of inner product spaces
@@ -30,7 +31,8 @@ the last section, various properties of matrices are explored.
 
 - `EuclideanSpace 𝕜 n`: defined to be `PiLp 2 (n → 𝕜)` for any `Fintype n`, i.e., the space
   from functions to `n` to `𝕜` with the `L²` norm. We register several instances on it (notably
-  that it is a finite-dimensional inner product space).
+  that it is a finite-dimensional inner product space), and provide a `!ₚ[]` notation (for numeric
+  subscripts like `₂`) for the case when the indexing type is `Fin n`.
 
 - `OrthonormalBasis 𝕜 ι`: defined to be an isometry to Euclidean space from a given
   finite-dimensional inner product space, `E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι`.
@@ -95,10 +97,43 @@ theorem PiLp.inner_apply {ι : Type*} [Fintype ι] {f : ι → Type*} [∀ i, No
   rfl
 
 /-- The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
-space use `EuclideanSpace 𝕜 (Fin n)`. -/
+space use `EuclideanSpace 𝕜 (Fin n)`.
+
+For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
+analogous to `![x, y, ...]` notation. -/
 abbrev EuclideanSpace (𝕜 : Type*) (n : Type*) : Type _ :=
   PiLp 2 fun _ : n => 𝕜
 
+section Notation
+open Lean Meta Elab Term Macro TSyntax PrettyPrinter.Delaborator SubExpr
+
+/-- Notation for vectors in Lp space. `!₂[x, y, ...]` is a shorthand for
+`(WithLp.equiv 2 _ _).symm ![x, y, ...]`, of type `EuclideanSpace _ (Fin _)`.
+
+This also works for other subscripts. -/
+syntax (name := PiLp.vecNotation) "!" noWs subscript(term) noWs "[" term,* "]" : term
+macro_rules | `(!$p:subscript[$e:term,*]) => do
+  -- override the `Fin n.succ` to a literal
+  let n := e.getElems.size
+  `((WithLp.equiv $p <| ∀ _ : Fin $(quote n), _).symm ![$e,*])
+
+set_option trace.debug true in
+/-- Unexpander for the `!₂[x, y, ...]` notation. -/
+@[delab app.DFunLike.coe]
+def EuclideanSpace.delabVecNotation : Delab :=
+  whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 6 do
+    -- check that the `(WithLp.equiv _ _).symm` is present
+    let p : Term ← withAppFn <| withAppArg do
+      let_expr Equiv.symm _ _ e := ← getExpr | failure
+      let_expr WithLp.equiv _ _ := e | failure
+      withNaryArg 2 <| withNaryArg 0 <| delab
+    -- to be conservative, only allow subscripts which are numerals
+    guard <| p matches `($_:num)
+    let `(![$elems,*]) := ← withAppArg delab | failure
+    `(!$p[$elems,*])
+
+end Notation
+
 theorem EuclideanSpace.nnnorm_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n]
     (x : EuclideanSpace 𝕜 n) : ‖x‖₊ = NNReal.sqrt (∑ i, ‖x i‖₊ ^ 2) :=
   PiLp.nnnorm_eq_of_L2 x

Mathlib/Analysis/Quaternion.lean

@@ -165,7 +165,7 @@ theorem norm_piLp_equiv_symm_equivTuple (x : ℍ) :
 noncomputable def linearIsometryEquivTuple : ℍ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4) :=
   { (QuaternionAlgebra.linearEquivTuple (-1 : ℝ) (-1 : ℝ)).trans
       (WithLp.linearEquiv 2 ℝ (Fin 4 → ℝ)).symm with
-    toFun := fun a => (WithLp.equiv _ (Fin 4 → _)).symm ![a.1, a.2, a.3, a.4]
+    toFun := fun a => !₂[a.1, a.2, a.3, a.4]
     invFun := fun a => ⟨a 0, a 1, a 2, a 3⟩
     norm_map' := norm_piLp_equiv_symm_equivTuple }
 

MathlibTest/EuclideanSpace.lean

@@ -0,0 +1,33 @@
+import Mathlib.Analysis.InnerProductSpace.PiL2
+
+#guard_expr !₂[] = (WithLp.equiv 2 (∀ _ : Fin 0, _)).symm ![]
+#guard_expr !₂[1, 2, 3] = (WithLp.equiv 2 (∀ _ : Fin 3, ℕ)).symm ![1, 2, 3]
+#guard_expr !₁[1, 2, (3 : ℝ)] = (WithLp.equiv 1 (∀ _ : Fin 3, ℝ)).symm ![1, 2, 3]
+
+section delaborator
+
+/-- info: !₂[1, 2, 3] : WithLp 2 (Fin 3 → ℕ) -/
+#guard_msgs in
+#check !₂[1, 2, 3]
+
+set_option pp.mvars false in
+/-- info: !₀[] : WithLp 0 (Fin 0 → ?_) -/
+#guard_msgs in
+#check !₀[]
+
+section var
+variable {p : ENNReal}
+/-- info: (WithLp.equiv p (Fin 3 → ℕ)).symm ![1, 2, 3] : WithLp p (Fin 3 → ℕ) -/
+#guard_msgs in#check !ₚ[1, 2, 3]
+end var
+
+section tombstoned_var
+/- Here the `p` in the subscript is shadowed by a later p; so even if we do
+make the delaborator less conservative, it should not fire here since `✝` cannot
+be subscripted. -/
+variable {p : ENNReal} {x} (hx : x = !ₚ[1, 2, 3]) (p : True)
+/-- info: hx : x = (WithLp.equiv p✝ (Fin 3 → ℕ)).symm ![1, 2, 3] -/
+#guard_msgs in #check hx
+end tombstoned_var
+
+end delaborator

scripts/check-yaml.lean

@@ -40,6 +40,7 @@ def processDb (decls : ConstMap) : String → IO Bool
     return false
 
 unsafe def main : IO Unit := do
+  Lean.enableInitializersExecution
   CoreM.withImportModules #[`Mathlib, `Archive]
       (searchPath := compile_time_search_path%) (trustLevel := 1024) do
     let decls := (← getEnv).constants

scripts/noshake.json

@@ -424,6 +424,7 @@
   ["Mathlib.Tactic.CategoryTheory.Bicategory.Basic"],
   "Mathlib.Analysis.Normed.Operator.LinearIsometry":
   ["Mathlib.Algebra.Star.Basic"],
+  "Mathlib.Analysis.InnerProductSpace.PiL2": ["Mathlib.Util.Superscript"],
   "Mathlib.Analysis.InnerProductSpace.Basic":
   ["Mathlib.Algebra.Module.LinearMap.Basic"],
   "Mathlib.Analysis.Distribution.SchwartzSpace": ["Mathlib.Tactic.MoveAdd"],