Jordan curve theorem statement etc... (first steps)

Stream: new members

[Ilmārs Cīrulis]

Is this okay for a definition of the Jordan curve (simple closed curve)?
I looking right now at this pdf.

Someone, I believe, is already doing work on Jordan curve theorem... This is kinda duplication then, but I'm still interested in formalizing of this specific proof (for the two dimensional case) as learning experience.

import Mathlib

structure jordan_curve where
  parametrization: unitInterval → ℝ × ℝ
  property1: Continuous parametrization
  property2: Function.Injective parametrization

[Ilmārs Cīrulis]

Yes, there's something happening already here

[Kevin Buzzard]

Your definition seems to disagree with Hales; he has a function from the circle, not the unit interval.

[Ilmārs Cīrulis]

Thank you! I'm learning the specific math too and I see that I misunderstand that R\Z notation, it seems.

[Ilmārs Cīrulis]

Does adding property that parametrization 0 = parametrization 1 fixes that?

[Kevin Buzzard]

No because then it will never be injective!

[Ilmārs Cīrulis]

I believe I have found the correct definition/thing using Moogle. This should be UnitAddCircle, right?

import Mathlib

structure Jordan_curve where
  parametrization: UnitAddCircle → ℝ × ℝ
  property1: Continuous parametrization
  property2: Function.Injective parametrization

[Ilmārs Cīrulis]

And together with the (possible) formalization of Jordan curve theorem's statement:

import Mathlib

structure Jordan_curve where
  parametrization: UnitAddCircle → ℝ × ℝ
  property1: Continuous parametrization
  property2: Function.Injective parametrization

theorem Jordan_curve_theorem (jc: Jordan_curve):
  ∃ A B, (jc.parametrization '' Set.univ)ᶜ = A.union B ∧
  A.Nonempty ∧ B.Nonempty ∧ Disjoint A B ∧
  IsConnected A ∧ IsConnected B ∧ IsOpen A ∧ IsOpen B := sorry

[Kevin Buzzard]

Instead of f '' Set.univ you should use docs#Set.range but other than that this looks good to me.

[Eric Wieser]

You should use the union notation too, to avoid having to work with docs#Set.union which is an implementation detail

[Vincent Beffara]

Maybe using Path x x with appropriate definition of injectivity would make sense (or GenLoop (Fin 1) x ?)

[Ilmārs Cīrulis]

I believe UnitAddCircle is the best option. Others could work too, of course.

[Ilmārs Cīrulis]

Here's the statement of first lemma. How does that looks to you? Is this a good enough way to define lines and polygons?

-- https://mizar.uwb.edu.pl/trybulec65/4.pdf
import Mathlib

structure Jordan_curve where
  parametrization: UnitAddCircle → ℝ × ℝ
  parametrization_continuous: Continuous parametrization
  parametrization_injective: Function.Injective parametrization

structure line_coefs where
  a: ℝ
  b: ℝ
  c: ℝ
  nonzero_normal_vector: a ≠ 0 ∨ b ≠ 0

def line (lc: line_coefs): Set (ℝ × ℝ) := λ ⟨x, y⟩ => lc.a * x + lc.b * y + lc.c = 0

def union_of_list {A}: List (Set A) → Set A := List.foldr (λ x1 x2 => x1 ∪ x2) ∅

def union_of_finite_number_of_lines (L: List line_coefs): Set (ℝ × ℝ) := union_of_list (L.map line)

def is_polygonal {A} (f: A → ℝ × ℝ): Prop :=
  ∃ (L: List line_coefs), Set.range f ⊆ union_of_finite_number_of_lines L

def is_polygon (jc: Jordan_curve): Prop := is_polygonal jc.parametrization

def parity_function_for_polygon (jc: Jordan_curve) (H: is_polygon jc):
    ↑(Set.range jc.parametrization)ᶜ → Bool := sorry

lemma parity_function_for_polygon_is_locally_constant (jc: Jordan_curve) (H: is_polygon jc):
  IsLocallyConstant (parity_function_for_polygon _ H) := sorry

[Luigi Massacci]

This is more a question of style/readability, but I would suggest naming property1, property2, Hab with proper english names

[Ilmārs Cīrulis]

Renamed them, yes. Thank you!

[Ilmārs Cīrulis]

Rewrote the statement of first lemma and some stuff necessary for it, a bit.

-- https://mizar.uwb.edu.pl/trybulec65/4.pdf
import Mathlib

structure Jordan_curve where
  parametrization: UnitAddCircle → ℝ × ℝ
  parametrization_continuous: Continuous parametrization
  parametrization_injective: Function.Injective parametrization

structure line_coefs where
  a: ℝ
  b: ℝ
  c: ℝ
  nonzero_normal_vector: a ≠ 0 ∨ b ≠ 0

def line (lc: line_coefs): Set (ℝ × ℝ) := λ ⟨x, y⟩ => lc.a * x + lc.b * y + lc.c = 0

def union_of_list {A}: List (Set A) → Set A := List.foldr Set.union ∅

def range_is_subset_of_lines {A} (f: A → ℝ × ℝ) (L: List line_coefs): Prop :=
  Set.range f ⊆ union_of_list (L.map line)

structure polygon where
  curve: Jordan_curve
  lines: List line_coefs
  curve_is_polygon: range_is_subset_of_lines curve.parametrization lines

def parity_function_for_polygon (p: polygon):
  ↑(Set.range p.curve.parametrization)ᶜ → Bool := sorry

lemma parity_function_for_polygon_is_locally_constant (p: polygon):
  IsLocallyConstant (parity_function_for_polygon p) := sorry

[Ilmārs Cīrulis]

It seems I will have to do some computational geometry or smth for this parity_function_for_polygon. Okay, challenge accepted.

[Ilmārs Cīrulis]

Maybe weird question... can I use Prop as Bool, even if the Prop is without decision procedure?

[Ilmārs Cīrulis]

That introduces uncomputable stuff into proof, of course

[Ilmārs Cīrulis]

Oh, there's noncomputable instance Real.decidableEq (and also decidableLT and decidableLE). That should be enough.

[Ilmārs Cīrulis]

How would you prove this, which is basically the solution of 2x2 linear equation system?
Thank you!

import Mathlib

structure line_coefs where
  a: ℝ
  b: ℝ
  c: ℝ
  nonzero_normal_vector: a ≠ 0 ∨ b ≠ 0

def line (lc: line_coefs): Set (ℝ × ℝ) := λ ⟨x, y⟩ => lc.a * x + lc.b * y + lc.c = 0

def parallel_lines (lc1 lc2: line_coefs): Prop := lc1.a * lc2.b - lc2.a * lc1.b = 0

theorem intersection_of_two_lines {lc1 lc2: line_coefs} (H: ¬ parallel_lines lc1 lc2):
    ∃ (p: ℝ × ℝ), line lc1 ∩ line lc2 = { p } := by
  cases lc1 with | mk a1 b1 c1 nonzero_normal_vector_1 =>
  cases lc2 with | mk a2 b2 c2 nonzero_normal_vector_2 =>
  unfold parallel_lines line at *
  simp at *
  exists (b1 * c2 - c1 * b2) / (a1 * b2 - a2 * b1), (c1 * a2 - a1 * c2) / (a1 * b2 - a2 * b1)
  ext ⟨x, y⟩
  simp
  simp [Set.mem_def, ne_eq] at *
  constructor <;> simp
  . intros eq1 eq2
    rw [<- neg_eq_of_add_eq_zero_right eq1]
    rw [<- neg_eq_of_add_eq_zero_right eq2]
    field_simp
    constructor <;> ring
  . intros eq1 eq2
    constructor <;> (subst x y; field_simp; ring)

[Ilmārs Cīrulis]

Okay, done. (Edited previous comment.)

[Ilmārs Cīrulis]

Okay, steps will be, probably:

1. get all intersection points of the lines
2. filter out those who belong to the (polygonal) Jordan curve
3. sort those by the corresponding time parameters
4. accordingly get all segments (probably in the corresponding order)
5. define the parity function (by getting the downwards ray's intersections with the segments, sorting them and then changing parity after each of them, starting with false at the start point)
6. prove that the parity function is locally constant (somehow --- I have postponed thinking about this part for now)

[Vincent Beffara]

A question: why do you want a statement that the image of a curve is contained in a union of lines, rather than directly stating that it is piecewise affine? That would make points 1-4 part of the definition of a polygonal curve.

[Ilmārs Cīrulis]

Oh, I didn't know that's possible. Also, probably following the definitions of the informal proof in the pdf too much.

[Ilmārs Cīrulis]

May I ask for a hint how to state that it is piecewise affine? :sweat_smile:

[Ilmārs Cīrulis]

I mean, is there something in Mathlib? Or should I write my own definition?

[Vincent Beffara]

Piecewise things are always painful... Something like this maybe

-- https://mizar.uwb.edu.pl/trybulec65/4.pdf
import Mathlib

open Set unitInterval

structure Jordan_curve where
  parametrization: I → ℝ × ℝ
  parametrization_continuous: Continuous parametrization
  parametrization_injective: Function.Injective parametrization

instance : CoeFun Jordan_curve (fun _ => I → ℝ × ℝ) := ⟨Jordan_curve.parametrization⟩

structure Polygonification (γ : Jordan_curve) where
  t : ℕ → I
  ht : Monotone t

  n : ℕ
  ht0 : t 0 = 0
  ht1 : ∀ i ≥ n, t i = 1

  a : ℕ → ℝ × ℝ
  b : ℕ → ℝ × ℝ

  aff : ∀ n, ∀ u ∈ Icc (t n) (t (n + 1)), γ u = a n + (u * (b n).1, u * (b n).2)

def parity_function_for_polygon {γ : Jordan_curve} (p: Polygonification γ) :
  ↑(Set.range γ)ᶜ → Bool := sorry

[Vincent Beffara]

But then you have to show that the parity does not depend on the choice of the polygonification