def IccT : Type

Here we define orbit, the Bad set, and the parametrized families rot and rot_iso (defined and developed in the module Rot.lean) and skew_rot Crucially we prove that there are only countably many "Bad" "rot"s and "skew_rot"s. We work with rot_iso whenever possible, and only convert to a statement about rot at the end (using the same_action lemma).

We also define as well as some geometric objects used by the main theorems like ball and cone, and the group G3 of isometries.

We also prove some "obvious" things like that SO(3) is contained in G3 (the group of isometries) and some lemmas about cardinality of sets.

Equations

• IccT = { x : ℝ // x ∈ Set.Icc 0 (Real.pi / 2) }

instance interval_uncountable : Uncountable IccT

noncomputable def to_s2_r3 : IccT → R3

Equations

• to_s2_r3 θ = to_R3 ![Real.cos ↑θ, Real.sin ↑θ, 0]

def is_s2 (θ : IccT) : to_s2_r3 θ ∈ S2

Equations

• ⋯ = ⋯

noncomputable def to_s2 : IccT → ↑S2

Equations

• to_s2 θ = ⟨to_s2_r3 θ, ⋯⟩

theorem ih : Function.Injective to_s2

theorem s2_uncountable : Uncountable ↑S2

theorem lb_card_s2 : Cardinal.aleph0 < Cardinal.mk ↑S2

@[reducible, inline]

abbrev MAT1 : Type

Equations

• MAT1 = Matrix (Fin 3) (Fin 1) ℝ

def v2m (v : R3_raw) : MAT1

Equations

• v2m v = !![v 0; v 1; v 2]

theorem dot_as_matmul (u v : R3_raw) : u ⬝ᵥ v = (Matrix.transpose (v2m u) * v2m v) 0 0

theorem v2m_equiv (M : MAT) (v : R3_raw) : v2m (Matrix.mulVec M v) = M * v2m v

theorem dp_nonneg (v : R3_raw) : v ⬝ᵥ v ≥ 0

theorem so3_cancel_lem {g : ↥SO3} : (↑g).transpose * ↑g = 1

theorem so3_fixes_norm (g : ↥SO3) (x : R3) : ‖g • x‖ = ‖x‖

theorem so3_fixes_s2 (g : ↥SO3) : f g '' S2 ⊆ S2

theorem triv_so3 : f 1 = fun (x : R3) => x

def orbit {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (g : G) (S : Set X) : Set X

Equations

• orbit g S = ⋃ (i : ℕ), (f g)^[i] '' S

theorem rot_containment_S2 {axis : ↑S2} {θ : ℝ} : f (rot axis θ) '' S2 ⊆ S2

theorem rot_containment_general {S : Set R3} (axis : ↑S2) (subset_of_s2 : S ⊆ S2) (r : ℝ) : orbit (rot axis r) S ⊆ S2

def BadEl {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (g : G) (S : Set X) : Prop

Equations

• BadEl g S = ∃ n > 0, ∃ s ∈ S, (f g)^[n] s ∈ S

def Bad {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (F : ℝ → G) (S : Set X) : Set ℝ

Equations

• Bad F S = {θ : ℝ | BadEl (F θ) S}

theorem collapse_iter {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (g h : G) (n : ℕ) : (f (h * g * h⁻¹))^[n] = f h ∘ (f g)^[n] ∘ f h⁻¹

theorem conj_bad_el {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (g h : G) (S : Set X) : BadEl g S ↔ BadEl (h * g * h⁻¹) (f h '' S)

def BadAtN {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (F : ℝ → G) (S : Set X) (s t : ↑S) (n : ℕ) : Set ℝ

Equations

• BadAtN F S s t n = {θ : ℝ | (f (F θ))^[n + 1] ↑s = ↑t}

def BadAtN_rot (ax : ↑S2) (S : Set R3) (s t : ↑S) (n : ℕ) : Set ℝ

Equations

• BadAtN_rot ax S s t n = {θ : ℝ | (f (rot ax θ))^[n + 1] ↑s = ↑t}

def BadAtN_rot_iso (ax : ↑S2) (S : Set R3) (s t : ↑S) (n : ℕ) : Set ℝ

Equations

• BadAtN_rot_iso ax S s t n = {θ : ℝ | (⇑(rot_iso ax θ))^[n + 1] ↑s = ↑t}

theorem rot_iso_comp_add (ax : ↑S2) (t1 t2 : ℝ) : ⇑(rot_iso ax t1) ∘ ⇑(rot_iso ax t2) = ⇑(rot_iso ax (t1 + t2))

theorem rot_iso_power_lemma (axis : ↑S2) (r : ℝ) (n : ℕ) : (⇑(rot_iso axis r))^[n] = ⇑(rot_iso axis (↑n * r))

theorem rot_iso_fixed_gen {t : ℝ} (axis : ↑S2) (v w : R3) : operp axis v ≠ 0 ∧ (rot_iso axis t) v = w → ∃ (k : ℤ), t = (ang_diff axis v w).toReal + ↑k * 2 * Real.pi

theorem rot_iso_fixed {t : ℝ} (axis : ↑S2) (v : R3) : operp axis v ≠ 0 ∧ (rot_iso axis t) v = v → ∃ (k : ℤ), t = ↑k * 2 * Real.pi

theorem BadAtN_rot_iso_equiv (axis : ↑S2) (S : Set R3) (s t : ↑S) (n : ℕ) : S ⊆ S2 → operp axis ↑s ≠ 0 → BadAtN_rot_iso axis S s t n ⊆ {θ : ℝ | ∃ (k : ℤ), (↑n + 1) * θ = ↑k * (2 * Real.pi) + (ang_diff axis ↑s ↑t).toReal}

theorem same_bad (ax : ↑S2) (S : Set R3) (s t : ↑S) (n : ℕ) : BadAtN_rot ax S s t n = BadAtN_rot_iso ax S s t n

def BadAt {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (F : ℝ → G) (S : Set X) (s t : ↑S) : Set ℝ

Equations

• BadAt F S s t = ⋃ (n : ℕ), BadAtN F S s t n

theorem bad_as_union {X : Type u_1} {G : Type u_2} [Group G] [MulAction G X] (F : ℝ → G) (S : Set X) : Bad F S = ⋃ (s : ↑S), ⋃ (t : ↑S), BadAt F S s t

theorem bad_as_union_rot (axis : ↑S2) (S : Set R3) : S ⊆ S2 → Bad (rot axis) S = ⋃ (s : ↑S), ⋃ (t : ↑S), ⋃ (n : ℕ), BadAtN (rot axis) S s t n

theorem BadAtN_rot_iso_countable {n : ℕ} (axis : ↑S2) (S : Set R3) (s t : ↑S) : S ⊆ S2 ∧ ↑axis ∉ S ∧ -↑axis ∉ S → (BadAtN_rot_iso axis S s t n).Countable

theorem countable_bad_rots (S : Set R3) (axis : ↑S2) : S ⊆ S2 ∧ Countable ↑S ∧ ↑axis ∉ S ∧ -↑axis ∉ S → Countable ↑(Bad (rot axis) S)

def ToEquivSO3 (g : ↥SO3) : R3 ≃ R3

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev G3 : Type

Equations

• G3 = (R3 ≃ᵢ R3)

theorem so3_diff_lin (g : ↥SO3) (x y : R3) : g • x - g • y = g • (x - y)

theorem isometry_of_so3 (g : ↥SO3) : Isometry (f g)

def SO3_into_G3 : ↥SO3 → G3

Equations

• SO3_into_G3 g = { toEquiv := ToEquivSO3 g, isometry_toFun := ⋯ }

def SO3_in_G3 : Subgroup G3

Equations

• SO3_in_G3 = { carrier := SO3_into_G3 '' Set.univ, mul_mem' := @SO3_in_G3._proof_1, one_mem' := SO3_in_G3._proof_2, inv_mem' := @SO3_in_G3._proof_3 }

def hmo : ↥SO3 →* ↥SO3_in_G3

Equations

• hmo = { toFun := fun (g : ↥SO3) => ⟨SO3_into_G3 g, ⋯⟩, map_one' := hmo._proof_3, map_mul' := hmo._proof_5 }

theorem hmo_is_injective : Function.Injective ⇑hmo

theorem hmo_is_surjective : Function.Surjective ⇑hmo

theorem hmo_is_bijective : Function.Bijective ⇑hmo

noncomputable def SO3_to_G3_iso_forward_equiv : ↥SO3 ≃ ↥SO3_in_G3

Equations

• SO3_to_G3_iso_forward_equiv = Equiv.ofBijective (⇑hmo) hmo_is_bijective

noncomputable def SO3_embed_G3 : ↥SO3 ≃* ↥SO3_in_G3

Equations

• SO3_embed_G3 = MulEquiv.mk' SO3_to_G3_iso_forward_equiv SO3_embed_G3._proof_1

instance instMulActionG3R3 : MulAction G3 R3

Equations

• instMulActionG3R3 = { smul := fun (g : G3) (v : R3) => g v, mul_smul := instMulActionG3R3._proof_1, one_smul := instMulActionG3R3._proof_2 }

theorem SO3_G3_action_equiv (x : R3) (g : ↥SO3) : SO3_into_G3 g • x = g • x

def B3 : Set R3

Equations

• B3 = Metric.closedBall 0 1

def B3min : Set R3

Equations

• B3min = B3 \ {0}

def S2_sub : Type

Equations

• S2_sub = { S : Set R3 // S ⊆ S2 }

def cone (S : S2_sub) : Set R3

Equations

• cone S = {x : R3 | ∃ (s : ℝ) (v : R3), x = s • v ∧ v ∈ ↑S ∧ 0 < s}

def trunc_cone (S : S2_sub) : Set R3

Equations

• trunc_cone S = cone S ∩ B3

theorem b3min_is_trunc_cone_s2 : B3min = trunc_cone ⟨S2, ⋯⟩

theorem trunc_cone_sub_ball (S : S2_sub) : trunc_cone S ⊆ B3min

theorem cone_lemma (S : S2_sub) (x : R3) : x ∈ cone S ↔ normed x ∈ ↑S

theorem trunc_cone_lemma (S : S2_sub) (x : R3) : x ∈ trunc_cone S → normed x ∈ ↑S

theorem disj_lemma (n : ℕ) (fam : Fin n → S2_sub) (disj : ∀ (i j : Fin n), i ≠ j → Disjoint ↑(fam i) ↑(fam j)) (i j : Fin n) : i ≠ j → Disjoint (trunc_cone (fam i)) (trunc_cone (fam j))

theorem cover_lemma (n : ℕ) (fam : Fin n → S2_sub) (T : S2_sub) (cover : ⋃ (i : Fin n), ↑(fam i) = ↑T) : ⋃ (i : Fin n), trunc_cone (fam i) = trunc_cone T

instance instSMulCommClassRealSubtypeMatrixFinOfNatNatMemSubmonoidSO3R3 : SMulCommClass ℝ (↥SO3) R3

theorem map_lemma (n : ℕ) (map : Fin n → ↥SO3) (famA famB : Fin n → S2_sub) (map_prop : ∀ (i : Fin n), f (map i) '' ↑(famA i) = ↑(famB i)) (i : Fin n) : f (map i) '' trunc_cone (famA i) = trunc_cone (famB i)

def x_axis_vec : R3

Equations

• x_axis_vec = to_R3 ![1, 0, 0]

theorem x_axis_on_sphere : x_axis_vec ∈ S2

def x_axis : ↑S2

Equations

• x_axis = ⟨x_axis_vec, x_axis_on_sphere⟩

noncomputable def skew_rot (θ : ℝ) : G3

Equations

• One or more equations did not get rendered due to their size.

theorem f_triv_g3 {r : ℝ} : f (skew_rot r) = ⇑(skew_rot r)

theorem skew_rot_comp_add (t1 t2 : ℝ) : ⇑(skew_rot t1) ∘ ⇑(skew_rot t2) = ⇑(skew_rot (t1 + t2))

theorem skew_rot_power_lemma {n : ℕ} (r : ℝ) : (⇑(skew_rot r))^[n] = ⇑(skew_rot (↑n * r))

theorem origin_cont (T : ℝ) : ‖(skew_rot T) origin‖ ≤ 1

theorem srot_containment (r : ℝ) : orbit (skew_rot r) {origin} ⊆ B3

def origin_in_s : ↑{origin}

Equations

• origin_in_s = ⟨origin, origin_in_s._proof_1⟩

theorem BadAtN_skew_rot {n : ℕ} : BadAtN skew_rot {origin} origin_in_s origin_in_s n = {θ : ℝ | ∃ (k : ℤ), (↑n + 1) * θ / (2 * Real.pi) = ↑k}

theorem BadAtN_skew_rot_countable {n : ℕ} : (BadAtN skew_rot {origin} origin_in_s origin_in_s n).Countable

theorem bad_as_union_skew_rot : Bad skew_rot {origin} = ⋃ (n : ℕ), BadAtN skew_rot {origin} origin_in_s origin_in_s n

theorem countable_bad_skew_rot : Countable ↑(Bad skew_rot {origin})