Mathemagics

[Ideas] 1. 동전 던지기

동전 던지기에 대한 한 유튜브 게시물을 보고, 오랜만에 공학수학을 배웠던 기억을 되살려 몇 줄 적어 보았다.문제 본문은 다음과 같다.앞면과 뒷면이 각각 \(\frac{1}{2}\)의 확률로 나오는 공정한 동전을 던지는 시행을 반복할 때, 앞면, 뒷면, 앞면, 뒷면이 순서대로 등장하는 것과 뒷면, 앞면, 뒷면, 뒷면이 순서대로 등장하는 것 중 어느 것이 먼저 나올 확률이 높은가? 나는 이 문제를 마르코프 체인(Markov Chain)을 이용하여 접근했다.앞면을 H, 뒷면을 T라 할 때, 지금까지 던진 동전들의 결과 중 유의미한 결과만 고려하면, 아래 9개의 상태를 얻을 수 있다.아직 아무것도 던지지 않은 상태HHTHTHHTHTTTHTHTTHTT여기에서 '유의미한'의 의미는 다음 내용을 참고하는 것이 도움이..

Multiplication World에서는 Addition World에서 증명했던 Theorem들과, 곱셈에 관한 기본 Theorem들을 사용하여 곱셈의 교환법칙, 결합법칙, 그리고 분배법칙을 증명하고자 한다.Multiplication World Level 1Theorem mul_one: For any natural number \(m\), we have \(m \times 1=m\).theorem mul_one (m : ℕ) : m * 1 = m := byrw [one_eq_succ_zero]rw [mul_succ m 0]rw [mul_zero, zero_add]rflMultiplication World Level 2Theorem zero_mul: For all natural numbers \(m\),..

Lean과 Natural Number Game에 대한 간략한 소개는 이전 글에서 확인할 수 있다.Addition World에서는 덧셈의 교환법칙(add_comm)과 결합법칙(add_assoc)을 증명하는 것을 목표로 한다.지금까지의 과정에서 사용할 수 있는 Theorem은 add_zero, add_succ, succ_eq_add_one과, \(1=\text{succ} \ 0\), \(2=\text{succ} \ 1\)등의 자명한 equation이다.Addition World Level 1Theorem zero_add: For all natural numbers \(n\), we have \(0+n=n\).theorem zero_add (n : ℕ) : 0 + n = n := byinduction n w..

Lean은 프로그래밍 언어이자 증명보조기로 사용되는 도구이다.Natural Number Game을 통해, 인터랙티브 Lean을 사용하여 Lean의 문법을 간략히 학습할 수 있었다. 또한, 0을 포함한 (페아노 공리계를 따라 정의된) 자연수에서의 여러 Theorem을 순차적으로 증명하는 방법을 알 수 있었다. 다만, 인터랙티브인 만큼 증명이 긴 Theorem의 경우 가독성이 좋지 않기 때문에, indentation을 비롯한 추가적인 문법에 대해서는 추가로 알아둘 필요가 있을 것 같다.Tutorial World Level 1If \(x\) and \(q\) are arbitrary natural numbers, then \(37x+q=37x+q\).example (x q : ℕ) : 37 * x + q = ..

[5.3 Definition] 군의 위수(order) 군 \(G\)에 대하여, \(G\)의 위수 \(\vert G \vert \)(order \( \vert G \vert \) of \(G\))는 \(G\)의 원소의 수이다. [5.4 Definition] 부분군(subgroup) 군 \(G\)의 부분집합 \(H\)가 \(G\)의 이항연산에 대하여 닫혀 있으며, 집합 \(H\)와, \(G\)로부터 유도된 이항연산이 그 자체로도 군을 이룰 때, \(H\)는 \(G\)의 부분군(subgroup)이라 하고, \(H \leq G\) 또는 \(G \geq H\)라 한다. \(H \neq G\)인 경우 \(HH\)라 한다. 부분군의 예시 군 \(G\)에 대하여, 항등원이 \(e\)일 때, \(G\)와 \(\{e\}..

9. \(\langle U, \cdot \rangle\)은, \(\langle \mathbb{R}, + \rangle\)과 \(\langle \mathbb{R}^\ast, \cdot\rangle\) 둘 다와 동형이 아님을 보여라. \(\langle U, \cdot \rangle\)의 항등원은 \(1\), \(\langle \mathbb{R}, + \rangle\)의 항등원은 \(0\), \(\langle \mathbb{R}^\ast, \cdot\rangle\)의 항등원은 \(1\)이다. 이제 같은 원소를 3번 연산하여 항등원이 되는 원소, 즉 이항 구조 \(\langle S, \ast\rangle\)에 대하여 \(x \ast x \ast x =e\)의 해 \(x \in S\)의 개수를 구하자. 이때, 세..

[4.1 Definition] 군(group) 군(group)은 다음 조건을 만족하는 이항 구조 \(\langle G, \ast \rangle\)이다.\(\mathscr{G}_1\): 임의의 \(a, b, c \in G\)에 대하여, 결합 법칙 \[(a \ast b) \ast c = a \ast (b \ast c)\]이 성립한다. (associativity of \(\ast\))\(\mathscr{G}_2\): 임의의 \(x \in G\)에 대하여 \[e \ast x = x \ast e = x\]을 만족하는 항등원 \(e \in G\)가 존재한다. (identity element \(e\) for \(\ast\))\(\mathscr{G}_3\): 임의의 \(a \in G\) 각각에 대하여 \[a \ast..

이항 대수 구조(binary algebraic structure) 이항 대수 구조(binary algebraic structure) 은 집합 \(S\)와 그 위의 이항 연산 \(\ast\)을 통틀어 나타내며 \(\langle S, \ast \rangle\) 로 표기한다. 편의상 이항 구조(binary structure)로 쓰는 경우가 많다. [3.7 Definition] 동형사상(isomorphism)이항 대수 구조 \(\langle S, \ast \rangle\), \(\langle S', \ast' \rangle\)에 대하여, \(S\)와 \(S'\)의 동형사상(isomorphism)은 다음 조건(homomorphism property, 준동형 성질)을 만족하는 \(S\)에서 \(S'\)로의 일대일 ..

[2.1 Definition] 이항 연산(binary operation) 집합 \(S\) 위의 이항 연산(binary operation) \(\ast\)은 \(S \times S\)에서 \(S\)로의 함수이다. \((a, b) \in S \times S\)에 대하여, \(\ast((a, b)) \in S\)를 간단히 \(a \ast b\) 로 나타낸다.[2.3 Example] 집합 \(S\) 위의 이항 연산은 \(S \times S\)의 임의의 원소에 대하여 \(S\)의 한 원소를 매핑해야 한다. 따라서 실수 값을 갖는 행렬들의 집합 \(M(\mathbb{R})\) 위의 덧셈 \(+\)은 서로 다른 크기의 두 행렬 사이에서는 정의되지 않으므로 이항 연산이 아니다. [2.4 Definition] 닫혀 있음..

1. 서론 Spotify Web API는 Spotify에서 제공하는 콘텐츠에 대한 메타데이터를 추출할 수 있도록 도와주는 API입니다. Spotify Premium 사용자는 자신의 Dashboard에서 애플리케이션을 만들 수 있습니다. 이후 OAuth 2.0 방식을 사용하여 사용할 권한을 설정하고 권한 부여(authorization)를 하면, refresh token과 access token을 발급받을 수 있습니다. access token은 1시간(3,600초) 동안 유효한데, 이 access token이 만료된 경우 재발급에 refresh token을 사용합니다. access token은 앞으로 API를 활용한 호출(call)을 할 때마다 권한 확인을 위하여 header 부분에 들어가게 됩니다.2. 트..