def matrix_a : Matrix (Fin 3) (Fin 3) ℝ

Equations

• matrix_a = Matrix.of ![![1, 0, 0], ![0, 1 / 3, -2 / 3 * Real.sqrt 2], ![0, 2 / 3 * Real.sqrt 2, 1 / 3]]

def matrix_a' : Matrix (Fin 3) (Fin 3) ℝ

Equations

• matrix_a' = Matrix.of ![![1, 0, 0], ![0, 1 / 3, 2 / 3 * Real.sqrt 2], ![0, -2 / 3 * Real.sqrt 2, 1 / 3]]

def matrix_b : Matrix (Fin 3) (Fin 3) ℝ

Equations

• matrix_b = Matrix.of ![![1 / 3, -2 / 3 * Real.sqrt 2, 0], ![2 / 3 * Real.sqrt 2, 1 / 3, 0], ![0, 0, 1]]

def matrix_b' : Matrix (Fin 3) (Fin 3) ℝ

Equations

• matrix_b' = Matrix.of ![![1 / 3, 2 / 3 * Real.sqrt 2, 0], ![-2 / 3 * Real.sqrt 2, 1 / 3, 0], ![0, 0, 1]]

def matrix_one : Matrix (Fin 3) (Fin 3) ℝ

Equations

• matrix_one = 1

theorem matrix_a_det_neq_zero : Matrix.det matrix_a ≠ 0

theorem matrix_a'_det_neq_zero : Matrix.det matrix_a' ≠ 0

theorem matrix_b_det_neq_zero : Matrix.det matrix_b ≠ 0

theorem matrix_b'_det_neq_zero : Matrix.det matrix_b' ≠ 0

theorem matrix_one_det_neq_zero : Matrix.det matrix_one ≠ 0

def gl_a : GL (Fin 3) ℝ

Equations

• gl_a = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_a matrix_a_det_neq_zero

def gl_a' : GL (Fin 3) ℝ

Equations

• gl_a' = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_a' matrix_a'_det_neq_zero

def gl_b : GL (Fin 3) ℝ

Equations

• gl_b = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_b matrix_b_det_neq_zero

def gl_b' : GL (Fin 3) ℝ

Equations

• gl_b' = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_b' matrix_b'_det_neq_zero

def gl_one : GL (Fin 3) ℝ

Equations

• gl_one = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_one matrix_one_det_neq_zero

def erzeuger : Set (GL (Fin 3) ℝ)

Equations

• erzeuger = {gl_a, gl_b}

def G : Subgroup (GL (Fin 3) ℝ)

Equations

• G = Subgroup.closure erzeuger

@[inline, reducible]

abbrev r_3 : Type

Equations

• r_3 = (Fin 3 → ℝ)

@[inline, reducible]

abbrev r_2 : Type

Equations

• r_2 = (Fin 2 → ℝ)

def zero_one_zero : r_3

Equations

• zero_one_zero = ![0, 1, 0]

def rotate (p : GL (Fin 3) ℝ) (vec : r_3) : r_3

Equations

• rotate p vec = Matrix.vecMul vec ↑p

def rotate_set (x : Set r_3) (p : GL (Fin 3) ℝ) : Set r_3

Equations

• rotate_set x p = {w : r_3 | ∃ v ∈ x, rotate p v = w}

def rotate_n_times (n : ℕ) (p : GL (Fin 3) ℝ) (vec : r_3) : r_3

Equations

• rotate_n_times 0 p vec = vec
• rotate_n_times (Nat.succ m) p vec = rotate_n_times m p (rotate p vec)

def translate (p : r_3) (vec : r_3) : r_3

Equations

• translate p vec = p + vec

def L : Set r_3

Equations

• L = {w : r_3 | Real.sqrt (Real.sqrt (w 0 ^ 2 + w 1 ^ 2)) + w 2 ^ 2 ≤ 1}

def origin : r_3

Equations

• origin = ![0, 0, 0]

def L' : Set r_3

Equations

• L' = L \ {origin}

def fixpunkt (y : r_3) (p : GL (Fin 3) ℝ) : Prop

Equations

• fixpunkt y p = (rotate p y = y)

def D : Set ↑L'

Equations

• D = {w : ↑L' | ∀ (p : ↥G), fixpunkt ↑w ↑p}

def rotationsAchse (p : GL (Fin 3) ℝ) : Set r_3

Equations

• rotationsAchse p = {w : r_3 | fixpunkt w p}

inductive erzeuger_t : Type

• gl_a: erzeuger_t
• gl_b: erzeuger_t

instance instDecidableEqErzeuger_t : DecidableEq erzeuger_t

Equations

• instDecidableEqErzeuger_t x y = if h : erzeuger_t.toCtorIdx x = erzeuger_t.toCtorIdx y then isTrue ⋯ else isFalse ⋯

@[inline, reducible]

abbrev G_list : Type

Equations

• G_list = { w : List (erzeuger_t × Bool) // w = FreeGroup.reduce w }

def S_A : Set G_list

Equations

• S_A = {w : G_list | List.head? ↑w = some (erzeuger_t.gl_a, true)}

def S_A' : Set G_list

Equations

• S_A' = {w : G_list | List.head? ↑w = some (erzeuger_t.gl_a, false)}

def S_B : Set G_list

Equations

• S_B = {w : G_list | List.head? ↑w = some (erzeuger_t.gl_b, true)}

def S_B' : Set G_list

Equations

• S_B' = {w : G_list | List.head? ↑w = some (erzeuger_t.gl_b, false)}

def item_to_matrix (i : erzeuger_t × Bool) : GL (Fin 3) ℝ

Equations

• item_to_matrix i = match i with | (erzeuger_t.gl_a, true) => gl_a | (erzeuger_t.gl_a, false) => gl_a' | (erzeuger_t.gl_b, true) => gl_b | (erzeuger_t.gl_b, false) => gl_b'

def list_to_matrix (w : List (erzeuger_t × Bool)) : GL (Fin 3) ℝ

Equations

• list_to_matrix [] = gl_one
• list_to_matrix (head :: rest) = list_to_matrix rest * item_to_matrix head

def rotate_set_around_set (x : Set r_3) (p : Set G_list) : Set r_3

Equations

• rotate_set_around_set x p = {w : r_3 | ∃ pp ∈ p, ∃ ww ∈ x, rotate (list_to_matrix ↑pp) ww = w}