Connected set in R3 and divergence theorem at boundary

Stream: new members

[ZhiKai Pong]

I'm currently looking at trying to formalize the boundary conditions of Maxwell's equations for PhysLean (along the lines of https://physics.stackexchange.com/a/407129). The standard argument for this involves creating a "Gaussian pillbox" across an interface, apply the divergence theorem then taking the limit of its height to zero (similarly create a rectangle and apply stokes theorem for the curl equations). I tried to look through Mathlib and I believe in principle the ingredients are there for this to be stated and proved, but I'm not familiar with this part of Mathlib at all, so I'll probably ask lots of questions in this thread as I work towards this goal.

[ZhiKai Pong]

First question: I want to have a notion of a "domain" to be a connected set in R3.

import Mathlib

example : IsConnected {(0 < x 3) | x : EuclideanSpace ℝ (Fin 3)} := by
  sorry

My first attempt to state "the half space z > 0 is connected", is this the correct way to state this? I also have no idea how to prove this. The theorems I'm looking at around docs#IsConnected is all quite abstract and I would like some pointers as to how to state/prove things in R3.

[Bjørn Kjos-Hanssen]

You can use

import Mathlib

example : IsConnected {x : EuclideanSpace ℝ (Fin 3) | 0 < x 2 } := by
  sorry

(What you wrote is a set of propositions!)

[Bjørn Kjos-Hanssen]

Also I think the coordinates of x are x 0, x 1, x 2.

[ZhiKai Pong]

Bjørn Kjos-Hanssen said:

Also I think the coordinates of x are x 0, x 1, x 2.

I was too tired to think properly, that was obvious!

[ZhiKai Pong]

I found docs#EuclideanHalfSpace.pathConnectedSpace, I'll see what I can learn from there...

[ZhiKai Pong]

I managed to prove the following but please let me know if there are more direct ways of proving this using tools from the library:

import Mathlib

example : IsConnected {x : EuclideanSpace ℝ (Fin 3) | 0 < x 2} := by
  apply Convex.isConnected
  · rw [Convex]
    intro x hx y hy a b ha hb hab
    simp
    have hab : a = 1 - b := by linarith
    rw [hab]
    by_cases h : b = 0
    · rw [h]
      simp
      exact hx
    · have hb : 0 < b := by
        apply lt_of_le_of_ne hb
        symm
        exact h
      apply add_pos_of_nonneg_of_pos
      · rw [← hab]
        exact mul_nonneg ha (le_of_lt hx)
      · exact mul_pos hb hy
  · use !₂[1, 1, 1]
    simp

example : IsOpen {x : EuclideanSpace ℝ (Fin 3) | 0 < x 2} := by
  refine isOpen_lt ?_ ?_
  · fun_prop
  · fun_prop

[ZhiKai Pong]

My next question is whether there is a notion of boundary for an open set s that I can use directly or I should just use closure s \ s?

for the concrete example I'll try to prove

example : closure {x : EuclideanSpace ℝ (Fin 3) | 0 < x 2}
    =
    {x : EuclideanSpace ℝ (Fin 3) | 0 ≤ x 2} := by
  rw [closure]
  sorry

[ZhiKai Pong]

docs#closure_Ioi is really close but not quite since x is in R3. Is there a way to convert this?

nevermind exact closure_open_halfSpace 2 0 2 works!

[ZhiKai Pong]

For the boundary I'm not sure if docs#exterior or docs#frontier might be more useful, I'll need to learn what existing theorems are helpful and I'm not familiar with filters at all.

I believe what I need next is to prove that the boundary of a connected open set in R3 is a surface (then I need its tangent plane and normal vector).

very crude attempt of stating what I want:

lemma closure_of_connected_open_set_is_surface (S : Set (EuclideanSpace ℝ (Fin 3)))
    (hc : IsConnected S) (ho : IsOpen S) (D : Set (ℝ × ℝ)) (u v: ℝ) (huv : (u, v) ∈ D):
    ∃ (f : ℝ → ℝ → (EuclideanSpace ℝ (Fin 3))), frontier S = {f u v}:= by
  sorry

I don't think this is defined in mathlib (please let me know if there's something that helps!)

There is docs#TangentSpace and I'll try to start from there after I've proven the above, but any suggestions and advice is much appreciated!

[Bjørn Kjos-Hanssen]

Note that {f u v} has just one element; instead you can write it like this:

import Mathlib

lemma closure_of_connected_open_set_is_surface (S : Set (EuclideanSpace ℝ (Fin 3)))
    (hc : IsConnected S) (ho : IsOpen S) (D : Set (EuclideanSpace ℝ (Fin 2))) :
    ∃ (f : EuclideanSpace ℝ (Fin 2) → (EuclideanSpace ℝ (Fin 3))), frontier S = f '' D := by
  sorry

[ZhiKai Pong]

I realized I should probably use docs#modelWithCornersEuclideanHalfSpace, and then formalize the notion of regular surface etc.

At the moment there doesn't seem to be much on surfaces and curves in Mathlib, and I don't feel confident enough to work with the abstract manifold setting just yet. maybe I'll try to look at some classical differential geometry textbooks (e.g. do Carmo) and see how far I can go with those in lean. If anyone has any suggestions please let me know!