Seasawher
commented
1 month ago 途中経過
良い感じに難しくてちょうどいいかもしれない
/- # Rayleigh の定理 -/
import Mathlib.Tactic
import Mathlib.Data.Real.Irrational
import Mathlib.Data.Set.Operations
set_option autoImplicit false
set_option relaxedAutoImplicit false
/-- 正の自然数全体 -/
def PosNat : Set ℕ := { n : ℕ | 0 < n }
/-- 実数 x の正の自然数倍を整数に丸めたものからなる部分集合 -/
def beatty (x : ℝ) : Set ℕ := { ⌊n * x⌋₊ | n ∈ PosNat}
/-- beatty が PosNat の分割を与えるという命題 -/
def beatty_partition (r s : ℝ) : Prop := beatty r ∪ beatty s = PosNat ∧ beatty r ∩ beatty s = ∅
variable (r s : ℝ) (rirr : Irrational r) (sirr : Irrational s) (rpos : r > 0) (spos : s > 0)
-- `variable` で宣言した変数を引数に加えるためのコマンド
include rirr sirr rpos spos
/-- レイリーの定理 -/
theorem rayleigh_mp (h : 1/r + 1/s = 1) : beatty_partition r s := by
dsimp [beatty_partition]
refine ⟨?cover, ?disjoint⟩
-- 重複がないことを示す
case disjoint =>
-- 両方の集合に属している要素があったと仮定して矛盾を示せばよい。
suffices ¬ (∃ x, x ∈ beatty r ∧ x ∈ beatty s) from by
aesop
-- `x` が両方の集合に属していると仮定する。
intro ⟨x, ⟨m, mpos, hr⟩, ⟨n, npos, hs⟩⟩
-- ヒント：この命題は使用しても良い
#check Nat.floor_eq_iff
-- 仮定から、ある自然数 `m > 0` が存在して
-- `x ≤ m * r < x + 1` が成り立つ。
replace ⟨mpos, «x≤mr», «mr<x+1»⟩ : 0 < m ∧ x ≤ m * r ∧ m * r < x + 1 := by
rw [Nat.floor_eq_iff (show 0 ≤ ↑m * r from by positivity)] at hr
simp_all [PosNat]
clear hr
-- 同様に、ある自然数 `n > 0` が存在して
-- `x ≤ n * s < x + 1` が成り立つ。
replace ⟨npos, «x≤ns», «ns<x+1»⟩ : 0 < n ∧ x ≤ n * s ∧ n * s < x + 1 := by
rw [Nat.floor_eq_iff (show 0 ≤ ↑n * s from by positivity)] at hs
simp_all [PosNat]
clear hs
-- ヒント：この命題は使用してOK
#check irrational_iff_ne_rational
-- `r` は無理数なので狭義の不等号が成り立つ
have «x<mr» : x < m * r := by
-- `x ≠ m * r` を示せば十分。
suffices ¬ (x = m * r) from by
exact lt_of_le_of_ne «x≤mr» this
-- `x = m * r` と仮定して矛盾を示そう。
intro hr
-- このとき `r = x / m` が成り立つので、
-- `r` は無理数ではないということになる。
have : ¬ Irrational r := by
replace hr : r = x / m := by field_simp [hr]
aesop
-- これは矛盾。
contradiction
-- `s` も無理数なので狭義の不等号が成り立つ
have «x<ns» : x < n * s := by
-- `x ≠ n * s` を示せば十分。
suffices ¬ (x = n * s) from by
exact lt_of_le_of_ne «x≤ns» this
-- `x = n * s` と仮定して矛盾を示そう。
intro hs
-- このとき `s = x / n` が成り立つので、
-- `s` は無理数ではないということになる。
have : ¬ Irrational s := by
replace hs : s = x / n := by field_simp [hs]
aesop
-- これは矛盾。
contradiction
-- したがって `x < m + n < x + 1` が成り立つことになる。
have ⟨left, right⟩ : (x : ℝ) < m + n ∧ m + n < (x + 1 : ℝ) := by
have left : (x : ℝ) < m + n := calc
x = x * (1/r + 1/s) := by rw [h]; simp
_ = x / r + x / s := by ring
_ < (m * r) / r + (n * s) / s := by gcongr
_ = m + n := by field_simp
have right : m + n < (x + 1 : ℝ) := calc
m + n = (m * r) / r + (n * s) / s := by field_simp
_ < (x + 1) / r + (x + 1) / s := by gcongr
_ = (x + 1) * (1 / r + 1 / s) := by ring
_ = x + 1 := by rw [h]; simp
simp_all
clear * - left right
-- `x` と `m + n` はともに自然数なので、これは矛盾である。
have : False := by
replace left : x + 1 ≤ m + n := by
norm_cast at left
replace right : m + n ≤ x := by
norm_cast at right
omega
omega
contradiction
-- どちらかの数列には必ず登場することを示す
case cover =>
sorry
無理数の定義からわりとすぐに従う上に、無理数を定義するのに必要な実数の闇にノータッチなまま話を進められそう。 しかも非自明。