From 1a533c87a09b3d72aded1d981cec8be02c2f15c0 Mon Sep 17 00:00:00 2001 From: Nicola Bernini Date: Sun, 7 Jun 2026 18:01:12 +0200 Subject: [PATCH 1/2] feat: Adding Space Module Docs Improvement --- Physlib/SpaceAndTime/Space/Module.lean | 41 ++++++++++++++++++++++---- 1 file changed, 36 insertions(+), 5 deletions(-) diff --git a/Physlib/SpaceAndTime/Space/Module.lean b/Physlib/SpaceAndTime/Space/Module.lean index 065160daa..7f7c70c40 100644 --- a/Physlib/SpaceAndTime/Space/Module.lean +++ b/Physlib/SpaceAndTime/Space/Module.lean @@ -290,8 +290,27 @@ noncomputable instance {d : ℕ} : MeasurableSpace (Space d) := borel (Space d) instance {d : ℕ} : BorelSpace (Space d) where measurable_eq := by rfl -TODO "In the above documentation describe what an instance is, and why - it is useful to have instances for `Space d`." +/-! + +In Lean, an `instance` supplies a typeclass automatically. When a definition or +theorem needs a structure such as `AddCommGroup (Space d)`, `Module ℝ (Space d)`, +`NormedAddCommGroup (Space d)`, `InnerProductSpace ℝ (Space d)`, or +`MeasurableSpace (Space d)`, typeclass inference searches for the corresponding +instance and inserts it without the user passing it explicitly. + +These instances make `Space d` usable with standard mathematical notation and +with the Mathlib API. For example, they allow expressions such as `p + q`, +`c • p`, `‖p‖`, `inner ℝ p q`, and measurable-set arguments involving the Borel +structure. They also make general theorems about modules, normed groups, inner +product spaces, and measurable spaces apply directly to `Space d`. + +For `Space d`, these instances are intentional choices rather than inherited +facts: the type was defined as a structure instead of an abbreviation for +`EuclideanSpace ℝ (Fin d)`. In particular, the additive and module structures +choose an origin, while the norm, inner product, and Borel structure choose the +standard Euclidean coordinate geometry on `Fin d`. + +-/ /-! @@ -327,10 +346,22 @@ lemma sum_apply {ι : Type} [Fintype ι] (f : ι → Space d) (i : Fin d) : ## Basis --/ +A basis in Lean is typically represented by `Module.Basis ι R M`: an indexed +family of vectors in an `R`-module `M` such that every element of `M` has a +unique finite linear expansion in those vectors. The index type `ι` names the +basis vectors, and the map `basis.repr` gives the coordinate representation of a +vector with respect to that basis. + +For inner product spaces, Lean also has `OrthonormalBasis ι R M`. This is a +basis whose vectors are orthonormal, packaged together with a linear isometric +equivalence between `M` and its coordinate space. It can be coerced to the +underlying `Module.Basis` using `basis.toBasis` when only the linear-algebraic +basis structure is needed. -TODO "In the above documentation describe the notion of a basis - in Lean." +The standard basis below is indexed by `Fin d`, so the basis vector `basis i` +is the unit vector in the `i`th coordinate direction of `Space d`. + +-/ /-- The standard basis of Space based on `Fin d`. -/ noncomputable def basis {d} : OrthonormalBasis (Fin d) ℝ (Space d) where From 4e641c1c19e8166c0d42aa6e14c60a29a7f86ce5 Mon Sep 17 00:00:00 2001 From: Nicola Bernini Date: Wed, 10 Jun 2026 18:57:40 +0200 Subject: [PATCH 2/2] docs: move Space instance explanation --- Physlib/SpaceAndTime/Space/Module.lean | 40 ++++++++++++-------------- 1 file changed, 18 insertions(+), 22 deletions(-) diff --git a/Physlib/SpaceAndTime/Space/Module.lean b/Physlib/SpaceAndTime/Space/Module.lean index 7f7c70c40..ebb1b98f6 100644 --- a/Physlib/SpaceAndTime/Space/Module.lean +++ b/Physlib/SpaceAndTime/Space/Module.lean @@ -21,6 +21,24 @@ The scope of this module is to define on `Space d` the structure of a `Module` These instances require certain non-canonical choices to be made, for example the choice of a zero and for a basis, a choice of orientation. +In Lean, an `instance` supplies a typeclass automatically. When a definition or +theorem needs a structure such as `AddCommGroup (Space d)`, `Module ℝ (Space d)`, +`NormedAddCommGroup (Space d)`, `InnerProductSpace ℝ (Space d)`, or +`MeasurableSpace (Space d)`, typeclass inference searches for the corresponding +instance and inserts it without the user passing it explicitly. + +These instances make `Space d` usable with standard mathematical notation and +with the Mathlib API. For example, they allow expressions such as `p + q`, +`c • p`, `‖p‖`, `inner ℝ p q`, and measurable-set arguments involving the Borel +structure. They also make general theorems about modules, normed groups, inner +product spaces, and measurable spaces apply directly to `Space d`. + +For `Space d`, these instances are intentional choices rather than inherited +facts: the type was defined as a structure instead of an abbreviation for +Euclidean space. In particular, the additive and module structures choose an +origin, while the norm, inner product, and Borel structure choose the standard +Euclidean coordinate geometry. + -/ @[expose] public section @@ -292,28 +310,6 @@ instance {d : ℕ} : BorelSpace (Space d) where /-! -In Lean, an `instance` supplies a typeclass automatically. When a definition or -theorem needs a structure such as `AddCommGroup (Space d)`, `Module ℝ (Space d)`, -`NormedAddCommGroup (Space d)`, `InnerProductSpace ℝ (Space d)`, or -`MeasurableSpace (Space d)`, typeclass inference searches for the corresponding -instance and inserts it without the user passing it explicitly. - -These instances make `Space d` usable with standard mathematical notation and -with the Mathlib API. For example, they allow expressions such as `p + q`, -`c • p`, `‖p‖`, `inner ℝ p q`, and measurable-set arguments involving the Borel -structure. They also make general theorems about modules, normed groups, inner -product spaces, and measurable spaces apply directly to `Space d`. - -For `Space d`, these instances are intentional choices rather than inherited -facts: the type was defined as a structure instead of an abbreviation for -`EuclideanSpace ℝ (Fin d)`. In particular, the additive and module structures -choose an origin, while the norm, inner product, and Borel structure choose the -standard Euclidean coordinate geometry on `Fin d`. - --/ - -/-! - ## The norm on `Space` -/