curves and surfaces (differential geometry in R3)

Stream: PhysLean

[ZhiKai Pong]

the primary motivation for me is to do reflection and refraction at an boundary, but I imagine having these "elementary differential geometry" (things to do with parametrizations, normal vectors etc.) will be very useful for many other things. My impression is that mathlib has a lot on manifold theory, but not much on concrete curves and surfaces. I would just like to gauge how much of an effort will it require to build something up, ideally this will be connected to the manifold definitions but I'm not confident in those at the moment (it is something I want to learn eventually)

[Joseph Tooby-Smith]

I can't speak to how much work it would be, but the Mathematics directory of PhysLean is somewhat for this kind of thing - which doesn't fit completely in mathlib/ isn't in mathlib yet :).

[ZhiKai Pong]

I think I want the notions of a closed surface enclosing a volume - probably with docs#modelWithCornersEuclideanHalfSpace but I have to figure out how to state what I want.

I'll also need differentiability which relates to regular surface. https://math.stackexchange.com/a/2935902 seems to have what I want in terms of going from the manifold language to the parametrization picture, I'll try to work my way towards those

[Joseph Tooby-Smith]

With my physicist hat on, I would define a surface in space Space by the zero-set of a smooth map F : Space → ℝ, which has at least one non-zero partial derivative at every point in the zero-set.

These types of surfaces are called level surfaces, and MSE:2096790 hints at every surface been of this type (I say hints because as far as I can tell the 'answer' given doesn't exactly answer the specified question).

Thus I could imagine a theory like this:

import PhysLean.ClassicalMechanics.Space.Basic

namespace Space

structure LevelSurface (d : ℕ) where
  val : Space d → ℝ
  cond : ∀ x, val x = 0 → Space.grad val x ≠ 0

namespace LevelSurface

variable {d : ℕ} (S : LevelSurface d)

def surface : Set (Space d) := fun x => S.val x = 0

def interior : Set (Space d) := fun x => S.val x < 0

def exterior : Set (Space d) := fun x => 0 < S.val x

def DisjointPair (S1 S2 : LevelSurface d) : Prop :=
  Disjoint S1.surface S2.surface

def join (S1 S2 : LevelSurface d) (h : DisjointPair S1 S2)  : LevelSurface d where
  val := fun x => S1.val x * S2.val x
  cond := by sorry

end LevelSurface

end Space

(edit: fix condition on LevelSurface)

[Joseph Tooby-Smith]

(LevelSurface probably also need a smoothness condition. )

[ZhiKai Pong]

many thanks for this, I agree this is probably a good way of implementing this. using docs#modelWithCornersEuclideanHalfSpace (which does has notions of docs#ModelWithCorners.IsBoundaryPoint etc.) probably goes down a rabbit hole of homology/embedding etc. and is completely overkill for what I want to do for now, and your definition should be easier to do concrete calculations.

[Kevin Buzzard]

I think the Klein bottle is a surface which you can't realise as a subset of 3-space.

[Tomas Skrivan]

For a definition of a surface enclosing a volume I would look into Evans's book on PDEs. There you define a sane notion of a domain on which you can then solve PDEs. Boundary of such domain is a nice notion of a surface enclosing a volume. At some level or regularity this probably coincides with the level set definition.