Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
| of a zero), a future refactor should give `Space d` only the instance of an `AddTorsor` | ||
| (an affine space) which does not require the choice of a zero. This has not been done | ||
| yet since `fderiv` requires a `Module` instance. | ||
|
|
There was a problem hiding this comment.
| Similarly, `Norm` `InnerProductSpace` instances should be replaced by the `MetricSpace` instance giving directly the Euclidean distance. |
if only "physical" quantities are allowed.
There was a problem hiding this comment.
NormedAddTorsor is probably the right thing to mention.
There was a problem hiding this comment.
I've updated this, would appreciate it if one of you could check what I have written.
jstoobysmith
added
the
awaiting-author
Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>
Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>
Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>
jstoobysmith
removed
the
awaiting-author
|
|
||
| There is a choice between defining `Space d` as an `abbrev` of `EuclideanSpace ℝ (Fin d)`, | ||
| as a `def` of a type with value `EuclideanSpace ℝ (Fin d)` or as a structure | ||
| with a field `val : Fin d → ℝ`. |
There was a problem hiding this comment.
Arguably val : EuclideanSpace ℝ (Fin d) is a nicer option here, which means you don't have to redefine all the structure.
There was a problem hiding this comment.
But I think it means you have to use WithLp.ofLp etc. everywhere. Could one not get the same benefit in terms of structure by defining an equivalence from Space d to EuclideanSpace ℝ (Fin d)?
There was a problem hiding this comment.
Can you give an example of where you'd need to write WithLp.ofLp? I think it's registered as a function coercion so that you don't have to write it.
There was a problem hiding this comment.
My bad, I meant WithLp.toLp, I agree that you shouldn't need WithLp.ofLp
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
zhikaip
left a comment
zhikaip
left a comment
There was a problem hiding this comment.
some minor suggestions otherwise looks good
zhikaip
added
the
awaiting-author
jstoobysmith
added
ready-to-merge
* feat: Improve docs on space * feat: Add add and zero paragraph * Update PhysLean/SpaceAndTime/Space/Basic.lean Co-authored-by: Eric Wieser <wieser.eric@gmail.com> * Update PhysLean/SpaceAndTime/Space/Basic.lean Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com> * Update PhysLean/SpaceAndTime/Space/Basic.lean Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com> * Update PhysLean/SpaceAndTime/Space/Basic.lean Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com> * refactor: Update docs * Update PhysLean/SpaceAndTime/Space/Basic.lean Co-authored-by: Eric Wieser <wieser.eric@gmail.com> * refactor: Review comments --------- Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>
4 participants
Improving the documentation on
Spacein accordance with the conversation here:https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Space.20vs.20EuclideanSpace/with/575332888