banach_tarski.Definitions

source

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]]

source

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]]

source

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]]

source

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]]

source

def matrix_one :

Matrix (Fin 3) (Fin 3) ℝ

Equations

matrix_one = 1

source

theorem matrix_a_det_neq_zero :

Matrix.det matrix_a ≠ 0

source

theorem matrix_a'_det_neq_zero :

Matrix.det matrix_a' ≠ 0

source

theorem matrix_b_det_neq_zero :

Matrix.det matrix_b ≠ 0

source

theorem matrix_b'_det_neq_zero :

Matrix.det matrix_b' ≠ 0

source

theorem matrix_one_det_neq_zero :

Matrix.det matrix_one ≠ 0

source

def gl_a :

GL (Fin 3) ℝ

Equations

gl_a = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_a matrix_a_det_neq_zero

source

def gl_a' :

GL (Fin 3) ℝ

Equations

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

source

def gl_b :

GL (Fin 3) ℝ

Equations

gl_b = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_b matrix_b_det_neq_zero

source

def gl_b' :

GL (Fin 3) ℝ

Equations

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

source

def gl_one :

GL (Fin 3) ℝ

Equations

gl_one = Matrix.GeneralLinearGroup.mkOfDetNeZero matrix_one matrix_one_det_neq_zero

source

def erzeuger :

Set (GL (Fin 3) ℝ)

Equations

erzeuger = {gl_a, gl_b}

source

def G :

Subgroup (GL (Fin 3) ℝ)

Equations

G = Subgroup.closure erzeuger

source

@[inline, reducible]

abbrev r_3 :

Type

Equations

r_3 = (Fin 3 → ℝ)

source

@[inline, reducible]

abbrev r_2 :

Type

Equations

r_2 = (Fin 2 → ℝ)

source

def zero_one_zero :

r_3

Equations

zero_one_zero = ![0, 1, 0]

source

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

r_3

Equations

rotate p vec = Matrix.vecMul vec ↑p

source

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}

source

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)

source

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

r_3

Equations

translate p vec = p + vec

source

def L :

Set r_3

Equations

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

source

def origin :

r_3

Equations

origin = ![0, 0, 0]

source

def L' :

Set r_3

Equations

L' = L \ {origin}

source

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

Prop

Equations

fixpunkt y p = (rotate p y = y)

source

def D :

Set ↑L'

Equations

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

source

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

Set r_3

Equations

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

source

inductive erzeuger_t :

Type

gl_a: erzeuger_t
gl_b: erzeuger_t

source

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 ⋯

source

@[inline, reducible]

abbrev G_list :

Type

Equations

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

source

def S_A :

Set G_list

Equations

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

source

def S_A' :

Set G_list

Equations

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

source

def S_B :

Set G_list

Equations

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

source

def S_B' :

Set G_list

Equations

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

source

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'

source

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

source

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}