LeanPool.Monsky.RainbowTriangles

Imported Lean Pool material for LeanPool.Monsky.RainbowTriangles.

One square and an odd number of triangles

inductive LeanPool.Monsky.Color : Type

The three colors used in Monsky's coloring of the plane: red, green and blue.

• Red : Color
• Green : Color
• Blue : Color

@[implicit_reducible]

instance LeanPool.Monsky.instDecidableEqColor : DecidableEq Color

Equations

• LeanPool.Monsky.instDecidableEqColor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance LeanPool.Monsky.instFintypeColor : Fintype Color

Equations

• LeanPool.Monsky.instFintypeColor = { elems := { val := ↑LeanPool.Monsky.Color.enumList, nodup := LeanPool.Monsky.Color.enumList_nodup }, complete := LeanPool.Monsky.instFintypeColor._proof_1 }

def LeanPool.Monsky.coloring {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (X : EuclideanSpace ℝ (Fin 2)) : Color

Monsky's three-coloring of a point of the plane induced by a valuation v.

Equations

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

theorem LeanPool.Monsky.green_region {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (X : EuclideanSpace ℝ (Fin 2)) : coloring v X = Color.Green → v (X.ofLp 0) < v (X.ofLp 1) ∧ v (X.ofLp 1) ≥ v 1

theorem LeanPool.Monsky.red_region {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (X : EuclideanSpace ℝ (Fin 2)) : coloring v X = Color.Red → v (X.ofLp 0) < v 1 ∧ v (X.ofLp 1) < v 1

theorem LeanPool.Monsky.blue_region {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (X : EuclideanSpace ℝ (Fin 2)) : coloring v X = Color.Blue → v (X.ofLp 0) ≥ v 1 ∧ v (X.ofLp 0) ≥ v (X.ofLp 1)

def LeanPool.Monsky.rainbowTriangle {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : Prop

A triangle is rainbow if its three vertices receive all three colors.

Equations

• LeanPool.Monsky.rainbowTriangle v T = Function.Surjective (LeanPool.Monsky.coloring v ∘ T)

theorem LeanPool.Monsky.valuation_bounds {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (X Y Z : EuclideanSpace ℝ (Fin 2)) (hb : coloring v X = Color.Blue) (hg : coloring v Y = Color.Green) (hr : coloring v Z = Color.Red) : v (X.ofLp 0 * Y.ofLp 1) ≥ 1 ∧ v (X.ofLp 1 * Z.ofLp 0) < v (X.ofLp 0 * Y.ofLp 1) ∧ v (Y.ofLp 0 * Z.ofLp 1) < v (X.ofLp 0 * Y.ofLp 1) ∧ v (X.ofLp 0 * Y.ofLp 1) > v (-(Y.ofLp 1 * Z.ofLp 0)) ∧ v (X.ofLp 0 * Y.ofLp 1) > v (-(X.ofLp 1 * Y.ofLp 0)) ∧ v (X.ofLp 0 * Y.ofLp 1) > v (-(X.ofLp 0 * Z.ofLp 1))

theorem LeanPool.Monsky.valuation_max {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) {A a₁ a₂ a₃ a₄ a₅ : ℝ} (h1 : v A > v a₁) (h2 : v A > v a₂) (h3 : v A > v a₃) (h4 : v A > v a₄) (h5 : v A > v a₅) : v (A + a₁ + a₂ + a₃ + a₄ + a₅) = v A

theorem LeanPool.Monsky.bounded_det {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (X Y Z : EuclideanSpace ℝ (Fin 2)) (hb : coloring v X = Color.Blue) (hg : coloring v Y = Color.Green) (hr : coloring v Z = Color.Red) : v (X.ofLp 0 * Y.ofLp 1 + X.ofLp 1 * Z.ofLp 0 + Y.ofLp 0 * Z.ofLp 1 - Y.ofLp 1 * Z.ofLp 0 - X.ofLp 1 * Y.ofLp 0 - X.ofLp 0 * Z.ofLp 1) ≥ 1

theorem LeanPool.Monsky.det_triv_triangle (X Y : EuclideanSpace ℝ (Fin 2)) : (det fun (x : Fin 3) => match x with | 0 => X | 1 => X | 2 => Y) = 0

theorem LeanPool.Monsky.Lhull_equals_Thull (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : closedHull L = closedHull fun (x : Fin 3) => match x with | 0 => L 0 | 1 => L 0 | 2 => L 1

def LeanPool.Monsky.σ : Fin 6 → Fin 3 → Fin 3

The six permutations of Fin 3, indexed by Fin 6.

Equations

• LeanPool.Monsky.σ 0 = fun (x : Fin 3) => match x with | 0 => 0 | 1 => 1 | 2 => 2
• LeanPool.Monsky.σ 1 = fun (x : Fin 3) => match x with | 0 => 0 | 1 => 2 | 2 => 1
• LeanPool.Monsky.σ 2 = fun (x : Fin 3) => match x with | 0 => 1 | 1 => 0 | 2 => 2
• LeanPool.Monsky.σ 3 = fun (x : Fin 3) => match x with | 0 => 1 | 1 => 2 | 2 => 0
• LeanPool.Monsky.σ 4 = fun (x : Fin 3) => match x with | 0 => 2 | 1 => 0 | 2 => 1
• LeanPool.Monsky.σ 5 = fun (x : Fin 3) => match x with | 0 => 2 | 1 => 1 | 2 => 0

def LeanPool.Monsky.bSign : Fin 6 → ℝ

The sign of the permutation σ b, as a value in ℝ.

Equations

• LeanPool.Monsky.bSign 0 = 1
• LeanPool.Monsky.bSign 1 = -1
• LeanPool.Monsky.bSign 2 = -1
• LeanPool.Monsky.bSign 3 = 1
• LeanPool.Monsky.bSign 4 = 1
• LeanPool.Monsky.bSign 5 = -1

theorem LeanPool.Monsky.sign_non_zero (b : Fin 6) : bSign b ≠ 0

theorem LeanPool.Monsky.fun_in_bijections {i j k : Fin 3} : i ≠ j → i ≠ k → j ≠ k → ∃ (b : Fin 6), σ b = fun (x : Fin 3) => match x with | 0 => i | 1 => j | 2 => k

theorem LeanPool.Monsky.det_perm {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (b : Fin 6) : det T = bSign b * det (T ∘ σ b)

theorem LeanPool.Monsky.det_zero_perm {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hT : det T = 0) (i j k : Fin 3) : (det fun (x : Fin 3) => match x with | 0 => T i | 1 => T j | 2 => T k) = 0

theorem LeanPool.Monsky.linearCombinationDetMiddle {n : ℕ} {x z : EuclideanSpace ℝ (Fin 2)} {P : Fin n → EuclideanSpace ℝ (Fin 2)} {α : Fin n → ℝ} (hα : ∑ i : Fin n, α i = 1) : (det fun (x_1 : Fin 3) => match x_1 with | 0 => x | 1 => ∑ i : Fin n, α i • P i | 2 => z) = ∑ i : Fin n, α i * det fun (x_1 : Fin 3) => match x_1 with | 0 => x | 1 => P i | 2 => z

theorem LeanPool.Monsky.linearCombinationDetFirst {n : ℕ} {y z : EuclideanSpace ℝ (Fin 2)} {P : Fin n → EuclideanSpace ℝ (Fin 2)} {α : Fin n → ℝ} (hα : ∑ i : Fin n, α i = 1) : (det fun (x : Fin 3) => match x with | 0 => ∑ i : Fin n, α i • P i | 1 => y | 2 => z) = ∑ i : Fin n, α i * det fun (x : Fin 3) => match x with | 0 => P i | 1 => y | 2 => z

theorem LeanPool.Monsky.linearCombinationDetLast' {n : ℕ} {x y : EuclideanSpace ℝ (Fin 2)} {P : Fin n → EuclideanSpace ℝ (Fin 2)} {α : Fin n → ℝ} (hα : ∑ i : Fin n, α i = 1) : (det fun (x_1 : Fin 3) => match x_1 with | 0 => x | 1 => y | 2 => ∑ i : Fin n, α i • P i) = ∑ i : Fin n, α i * det fun (x_1 : Fin 3) => match x_1 with | 0 => x | 1 => y | 2 => P i

theorem LeanPool.Monsky.det_0_triangle_imp_triv {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hT : det T = 0) (x y z : EuclideanSpace ℝ (Fin 2)) : x ∈ closedHull T → y ∈ closedHull T → z ∈ closedHull T → (det fun (x_1 : Fin 3) => match x_1 with | 0 => x | 1 => y | 2 => z) = 0

theorem LeanPool.Monsky.no_Color_lines (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) {Γ₀ : Type} [locg : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) : ∃ (c : Color), ∀ P ∈ closedHull L, coloring v P ≠ c

theorem LeanPool.Monsky.red00 {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) : coloring v !₂[0, 0] = Color.Red

theorem LeanPool.Monsky.green01 {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) : coloring v !₂[0, 1] = Color.Green

theorem LeanPool.Monsky.blue10 {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) : coloring v !₂[1, 0] = Color.Blue

theorem LeanPool.Monsky.blue11 {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) : coloring v !₂[1, 1] = Color.Blue

theorem LeanPool.Monsky.get_color_of_rainbowTriangle {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (rt : rainbowTriangle v T) (c : Color) : ∃ (i : Fin 3), coloring v (T i) = c

theorem LeanPool.Monsky.bounded_det_coord_free {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (rt : rainbowTriangle v T) : v (det T) ≥ 1

theorem LeanPool.Monsky.no_odd_rainbowTriangle {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (rt : rainbowTriangle v T) (vhalf : v (1 / 2) > 1) : ¬∃ (n : ℕ) (_ : Odd n), |det T| / 2 = 1 / ↑n