LeanPool.Monsky.SegmentCounting

Imported Lean Pool material for LeanPool.Monsky.SegmentCounting.

noncomputable def LeanPool.Monsky.segmentSet (X : Finset (EuclideanSpace ℝ (Fin 2))) : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

The set of nondegenerate segments with both endpoints in X.

Equations

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

noncomputable def LeanPool.Monsky.avoidingSegmentSet (X : Finset (EuclideanSpace ℝ (Fin 2))) (A : Set (EuclideanSpace ℝ (Fin 2))) : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

The segments of segmentSet X whose open hull avoids the set A.

Equations

• LeanPool.Monsky.avoidingSegmentSet X A = {L ∈ LeanPool.Monsky.segmentSet X | Disjoint (LeanPool.Monsky.closedHull L) A}

noncomputable def LeanPool.Monsky.basicAvoidingSegmentSet (X : Finset (EuclideanSpace ℝ (Fin 2))) (A : Set (EuclideanSpace ℝ (Fin 2))) : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

The avoiding segments of X that are basic, i.e. contain no point of X in their interior.

Equations

• LeanPool.Monsky.basicAvoidingSegmentSet X A = {L ∈ LeanPool.Monsky.avoidingSegmentSet X A | ∀ x ∈ X, x ∉ LeanPool.Monsky.openHull L}

inductive LeanPool.Monsky.Chain : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → Type

An inductively defined chain of collinear segments between two points.

• basic {u v : EuclideanSpace ℝ (Fin 2)} : Chain u v
• join {u v w : EuclideanSpace ℝ (Fin 2)} (hCollineair : colin u v w) (C : Chain v w) : Chain u w

noncomputable def LeanPool.Monsky.toBasicSegments {u v : EuclideanSpace ℝ (Fin 2)} : Chain u v → Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

The finite set of basic segments making up a chain.

Equations

• LeanPool.Monsky.toBasicSegments LeanPool.Monsky.Chain.basic = {LeanPool.Monsky.toSegment u v}
• LeanPool.Monsky.toBasicSegments (LeanPool.Monsky.Chain.join hCollineair C) = LeanPool.Monsky.toBasicSegments C ∪ {LeanPool.Monsky.toSegment u w}

noncomputable def LeanPool.Monsky.glueChains {u v w : EuclideanSpace ℝ (Fin 2)} (hCollinear : colin u v w) : Chain u v → Chain v w → Chain u w

Concatenates two chains sharing an endpoint into a single chain.

Equations

• LeanPool.Monsky.glueChains hCollinear LeanPool.Monsky.Chain.basic x✝ = LeanPool.Monsky.Chain.join hCollinear x✝
• LeanPool.Monsky.glueChains hCollinear (LeanPool.Monsky.Chain.join h C') x✝ = LeanPool.Monsky.Chain.join ⋯ (LeanPool.Monsky.glueChains ⋯ C' x✝)

noncomputable def LeanPool.Monsky.reverseChain {u v : EuclideanSpace ℝ (Fin 2)} : Chain u v → Chain v u

Reverses the direction of a chain.

Equations

• LeanPool.Monsky.reverseChain LeanPool.Monsky.Chain.basic = LeanPool.Monsky.Chain.basic
• LeanPool.Monsky.reverseChain (LeanPool.Monsky.Chain.join hCollineair C) = LeanPool.Monsky.glueChains ⋯ (LeanPool.Monsky.reverseChain C) LeanPool.Monsky.Chain.basic

noncomputable def LeanPool.Monsky.chainToBigSegment {u v : EuclideanSpace ℝ (Fin 2)} (C : Chain u v) : Fin 2 → EuclideanSpace ℝ (Fin 2)

The single segment from the start to the end of a chain.

Equations

• LeanPool.Monsky.chainToBigSegment C = LeanPool.Monsky.toSegment u v

theorem LeanPool.Monsky.chainToBigSegment_join {u v w : EuclideanSpace ℝ (Fin 2)} (h : colin u v w) (C : Chain v w) : chainToBigSegment (Chain.join h C) = toSegment u w

theorem LeanPool.Monsky.chainToBigSegment_glue {u v w : EuclideanSpace ℝ (Fin 2)} (h : colin u v w) (CL : Chain u v) (CR : Chain v w) : chainToBigSegment (glueChains h CL CR) = toSegment u w

theorem LeanPool.Monsky.glueChains_assoc {u v w x : EuclideanSpace ℝ (Fin 2)} (C₁ : Chain u v) (C₂ : Chain v w) (C₃ : Chain w x) (h₁ : colin u v w) (h₂ : colin v w x) : glueChains ⋯ (glueChains h₁ C₁ C₂) C₃ = glueChains ⋯ C₁ (glueChains h₂ C₂ C₃)

theorem LeanPool.Monsky.reverseChain_glue {u v w : EuclideanSpace ℝ (Fin 2)} (h : colin u v w) (CL : Chain u v) (CR : Chain v w) : reverseChain (glueChains h CL CR) = glueChains ⋯ (reverseChain CR) (reverseChain CL)

theorem LeanPool.Monsky.basic_segments_glue {u v w : EuclideanSpace ℝ (Fin 2)} (h : colin u v w) (CL : Chain u v) (CR : Chain v w) : toBasicSegments (glueChains h CL CR) = toBasicSegments CL ∪ toBasicSegments CR

theorem LeanPool.Monsky.basic_segment_in_openHull {u v : EuclideanSpace ℝ (Fin 2)} (C : Chain u v) {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ toBasicSegments C) : openHull S ⊆ openHull (toSegment u v)

theorem LeanPool.Monsky.basic_segments_colin_disjoint {u v w : EuclideanSpace ℝ (Fin 2)} {C : Chain v w} (h : colin u v w) : toSegment u v ∉ toBasicSegments C

theorem LeanPool.Monsky.basic_segments_colin_disjoint2 {u v w : EuclideanSpace ℝ (Fin 2)} {C : Chain v w} (h : colin u v w) : toSegment v u ∉ toBasicSegments C

theorem LeanPool.Monsky.basic_segments_colin_disjoint_reverse {u v w : EuclideanSpace ℝ (Fin 2)} {C : Chain v w} (h : colin u v w) : toSegment u v ∉ toBasicSegments (reverseChain C)

theorem LeanPool.Monsky.reverseChain_basic_segments {u v : EuclideanSpace ℝ (Fin 2)} (C : Chain u v) : toBasicSegments (reverseChain C) = Finset.image (fun (S : Fin 2 → EuclideanSpace ℝ (Fin 2)) => reverseSegment S) (toBasicSegments C)

theorem LeanPool.Monsky.reverseChain_basic_segments_disjoint {u v : EuclideanSpace ℝ (Fin 2)} (C : Chain u v) (huv : u ≠ v) : Disjoint (toBasicSegments C) (toBasicSegments (reverseChain C))

theorem LeanPool.Monsky.segmentSet_vertex {X : Finset (EuclideanSpace ℝ (Fin 2))} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ segmentSet X) (i : Fin 2) : S i ∈ X

theorem LeanPool.Monsky.avoidingSegmentSet_sub {X : Finset (EuclideanSpace ℝ (Fin 2))} {A : Set (EuclideanSpace ℝ (Fin 2))} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ avoidingSegmentSet X A) : S ∈ segmentSet X

theorem LeanPool.Monsky.basicAvoidingSegmentSet_sub {X : Finset (EuclideanSpace ℝ (Fin 2))} {A : Set (EuclideanSpace ℝ (Fin 2))} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ basicAvoidingSegmentSet X A) : S ∈ segmentSet X

theorem LeanPool.Monsky.segmentSet_vertex_distinct {X : Finset (EuclideanSpace ℝ (Fin 2))} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ segmentSet X) : S 0 ≠ S 1

theorem LeanPool.Monsky.segmentSet_boundary {X : Finset (EuclideanSpace ℝ (Fin 2))} {x : EuclideanSpace ℝ (Fin 2)} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ segmentSet X) (hx : x ∈ boundary S) : x ∈ X

theorem LeanPool.Monsky.segmentSet_reverse {X : Finset (EuclideanSpace ℝ (Fin 2))} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ segmentSet X) : reverseSegment S ∈ segmentSet X

theorem LeanPool.Monsky.avoidingSegmentSet_reverse {X : Finset (EuclideanSpace ℝ (Fin 2))} {A : Set (EuclideanSpace ℝ (Fin 2))} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ avoidingSegmentSet X A) : reverseSegment S ∈ avoidingSegmentSet X A

theorem LeanPool.Monsky.basicAvoidingSegmentSet_reverse {X : Finset (EuclideanSpace ℝ (Fin 2))} {A : Set (EuclideanSpace ℝ (Fin 2))} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ basicAvoidingSegmentSet X A) : reverseSegment S ∈ basicAvoidingSegmentSet X A

theorem LeanPool.Monsky.avoidingSegmentSet_sub_left {X : Finset (EuclideanSpace ℝ (Fin 2))} {A : Set (EuclideanSpace ℝ (Fin 2))} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ avoidingSegmentSet X A) {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ X) (hxS : x ∈ openHull S) : toSegment (S 0) x ∈ avoidingSegmentSet X A

theorem LeanPool.Monsky.avoidingSegmentSet_sub_right {X : Finset (EuclideanSpace ℝ (Fin 2))} {A : Set (EuclideanSpace ℝ (Fin 2))} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ avoidingSegmentSet X A) {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ X) (hxS : x ∈ openHull S) : toSegment x (S 1) ∈ avoidingSegmentSet X A

theorem LeanPool.Monsky.segment_decomposition {A : Set (EuclideanSpace ℝ (Fin 2))} {X : Finset (EuclideanSpace ℝ (Fin 2))} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ avoidingSegmentSet X A) : ∃ (C : Chain (S 0) (S 1)), S = chainToBigSegment C ∧ {s ∈ basicAvoidingSegmentSet X A | closedHull s ⊆ closedHull S} = toBasicSegments C ∪ toBasicSegments (reverseChain C)

def LeanPool.Monsky.twoModFunction (f : (Fin 2 → EuclideanSpace ℝ (Fin 2)) → ℕ) : Prop

A function on segments that is additive modulo 2 along collinear splits.

Equations

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

def LeanPool.Monsky.symmFun (f : (Fin 2 → EuclideanSpace ℝ (Fin 2)) → ℕ) : Prop

A function on segments invariant under reversing the segment.

Equations

• LeanPool.Monsky.symmFun f = ∀ (S : Fin 2 → EuclideanSpace ℝ (Fin 2)), f (LeanPool.Monsky.reverseSegment S) = f S

theorem LeanPool.Monsky.twoModFunction_chains {f : (Fin 2 → EuclideanSpace ℝ (Fin 2)) → ℕ} (hf : twoModFunction f) {u v : EuclideanSpace ℝ (Fin 2)} (C : Chain u v) : (∑ S ∈ toBasicSegments C, f S) % 2 = f (toSegment u v) % 2

theorem LeanPool.Monsky.symmFunction_reverse_sum {f : (Fin 2 → EuclideanSpace ℝ (Fin 2)) → ℕ} (hf : symmFun f) {u v : EuclideanSpace ℝ (Fin 2)} (C : Chain u v) : ∑ S ∈ toBasicSegments (reverseChain C), f S = ∑ S ∈ toBasicSegments C, f S

theorem LeanPool.Monsky.mod_two_mul {a b : ℕ} (h : a % 2 = b % 2) : 2 * a % 4 = 2 * b % 4

theorem LeanPool.Monsky.sum_two_mod_fun_seg {A : Set (EuclideanSpace ℝ (Fin 2))} {X : Finset (EuclideanSpace ℝ (Fin 2))} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : S ∈ avoidingSegmentSet X A) {f : (Fin 2 → EuclideanSpace ℝ (Fin 2)) → ℕ} (hf₁ : twoModFunction f) (hf₂ : symmFun f) : (∑ T ∈ basicAvoidingSegmentSet X A with closedHull T ⊆ closedHull S, f T) % 4 = 2 * f S % 4

noncomputable def LeanPool.Monsky.isPurple {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) : (Fin 2 → EuclideanSpace ℝ (Fin 2)) → ℕ

Indicator (0 or 1) of whether a segment is purple, i.e. red-blue colored.

Equations

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

noncomputable def LeanPool.Monsky.isRainbow {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) : (Fin 3 → EuclideanSpace ℝ (Fin 2)) → ℕ

Indicator (0 or 1) of whether a triangle is rainbow.

Equations

• LeanPool.Monsky.isRainbow v T = if Function.Surjective (LeanPool.Monsky.coloring v ∘ T) then 1 else 0

theorem LeanPool.Monsky.isPurple_twoModFunction {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) : twoModFunction (isPurple v)

theorem LeanPool.Monsky.isPurple_symmFunction {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) : symmFun (isPurple v)

noncomputable def LeanPool.Monsky.triangulationPoints (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : Finset (EuclideanSpace ℝ (Fin 2))

The finite set of all vertices appearing in a triangulation.

Equations

• LeanPool.Monsky.triangulationPoints Δ = Δ.biUnion fun (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) => {T 0, T 1, T 2}

noncomputable def LeanPool.Monsky.triangulationPoints₂ (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : Finset (EuclideanSpace ℝ (Fin 2))

The set of triangulation vertices, viewed as a set of points of the plane.

Equations

• LeanPool.Monsky.triangulationPoints₂ Δ = Δ.biUnion fun (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) => Finset.image (fun (i : Fin 3) => T i) Finset.univ

theorem LeanPool.Monsky.triangulationPoints_mem {Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))} {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hT : T ∈ Δ) (i : Fin 3) : T i ∈ triangulationPoints Δ

noncomputable def LeanPool.Monsky.triangulationAvoidingSet (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : Set (EuclideanSpace ℝ (Fin 2))

The union of triangle interiors that basic segments of the triangulation must avoid.

Equations

• LeanPool.Monsky.triangulationAvoidingSet Δ = ⋃ T ∈ Δ, LeanPool.Monsky.openHull T

noncomputable def LeanPool.Monsky.triangulationBasicSegments (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

The basic avoiding segments of a triangulation.

Equations

• LeanPool.Monsky.triangulationBasicSegments Δ = LeanPool.Monsky.basicAvoidingSegmentSet (LeanPool.Monsky.triangulationPoints Δ) (LeanPool.Monsky.triangulationAvoidingSet Δ)

noncomputable def LeanPool.Monsky.triangulationBoundaryBasicSegments (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

The basic segments lying on the boundary of the unit square.

Equations

• LeanPool.Monsky.triangulationBoundaryBasicSegments Δ = {S ∈ LeanPool.Monsky.triangulationBasicSegments Δ | LeanPool.Monsky.openHull S ⊆ LeanPool.Monsky.boundary LeanPool.Monsky.unitSquare}

noncomputable def LeanPool.Monsky.triangulationInteriorBasicSegments (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

The basic segments lying in the interior of the unit square.

Equations

• LeanPool.Monsky.triangulationInteriorBasicSegments Δ = {S ∈ LeanPool.Monsky.triangulationBasicSegments Δ | LeanPool.Monsky.openHull S ⊆ LeanPool.Monsky.openHull LeanPool.Monsky.unitSquare}

noncomputable def LeanPool.Monsky.isTriangulation (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : Prop

isTriangulation Δ states that Δ is a disjoint cover of the unit square by triangles.

Equations

• LeanPool.Monsky.isTriangulation Δ = LeanPool.Monsky.isCover (LeanPool.Monsky.closedHull LeanPool.Monsky.unitSquare) ↑Δ

theorem LeanPool.Monsky.triangulationPoints_subset_unitSquare {Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))} (hCover : isTriangulation Δ) : ↑(triangulationPoints Δ) ⊆ closedHull unitSquare

Every vertex of a triangulation lies in the closed unit square.

theorem LeanPool.Monsky.segment_in_interior_aux {Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))} (hCover : isTriangulation Δ) (non_degen : ∀ P ∈ Δ, det P ≠ 0) {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hL : L ∈ triangulationBasicSegments Δ) : ∃ T ∈ Δ, closedHull L ⊆ closedHull T

theorem LeanPool.Monsky.segment_in_interior_or_boundary {Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))} (hCover : isTriangulation Δ) (non_degen : ∀ P ∈ Δ, det P ≠ 0) {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hL : L ∈ triangulationBasicSegments Δ) : openHull L ⊆ boundary unitSquare ∨ openHull L ⊆ openHull unitSquare

theorem LeanPool.Monsky.triangulation_boundary_union (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (hCover : isTriangulation Δ) (non_degen : ∀ P ∈ Δ, det P ≠ 0) : triangulationBasicSegments Δ = triangulationBoundaryBasicSegments Δ ∪ triangulationInteriorBasicSegments Δ

theorem LeanPool.Monsky.triangulation_boundary_intersection (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : triangulationBoundaryBasicSegments Δ ∩ triangulationInteriorBasicSegments Δ = ∅

noncomputable def LeanPool.Monsky.triangulationAllSegments (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

All basic segments of a triangulation, both boundary and interior.

Equations

• LeanPool.Monsky.triangulationAllSegments Δ = LeanPool.Monsky.avoidingSegmentSet (LeanPool.Monsky.triangulationPoints Δ) (LeanPool.Monsky.triangulationAvoidingSet Δ)

noncomputable def LeanPool.Monsky.purpleSum {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : ℕ

The total number of purple segments in a triangulation.

Equations

• LeanPool.Monsky.purpleSum v Δ = ∑ S ∈ LeanPool.Monsky.triangulationBoundaryBasicSegments Δ, LeanPool.Monsky.isPurple v S

noncomputable def LeanPool.Monsky.rainbowSum {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : ℕ

The total number of rainbow triangles in a triangulation.

Equations

• LeanPool.Monsky.rainbowSum v Δ = ∑ T ∈ Δ, LeanPool.Monsky.isRainbow v T

noncomputable def LeanPool.Monsky.rainbowTriangles {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))

The finite set of rainbow triangles of a triangulation.

Equations

• LeanPool.Monsky.rainbowTriangles v Δ = {T ∈ Δ | LeanPool.Monsky.isRainbow v T = 1}

noncomputable def LeanPool.Monsky.basicSegmentSegments (X : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))) (S : Fin 2 → EuclideanSpace ℝ (Fin 2)) : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

The basic segments of a segment family contained in a given side.

Equations

• LeanPool.Monsky.basicSegmentSegments X S = {L ∈ X | LeanPool.Monsky.openHull L ⊆ LeanPool.Monsky.openHull S}

theorem LeanPool.Monsky.segment_sum_splitting (A : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))) (AVOID : Set (EuclideanSpace ℝ (Fin 2))) (X : Finset (EuclideanSpace ℝ (Fin 2))) (hA : A ⊆ avoidingSegmentSet X AVOID) (hDisj : ∀ (S T : Fin 2 → EuclideanSpace ℝ (Fin 2)), S ∈ A → T ∈ A → S ≠ T → openHull S ∩ openHull T = ∅) (f : (Fin 2 → EuclideanSpace ℝ (Fin 2)) → ℕ) (hfTwoMod : twoModFunction f) (hSymm : symmFun f) : (∑ S ∈ basicAvoidingSegmentSet X AVOID with closedHull S ⊆ ⋃ T ∈ A, closedHull T, f S) % 4 = (2 * ∑ T ∈ A, f T) % 4

noncomputable def LeanPool.Monsky.p (x y : ℝ) : EuclideanSpace ℝ (Fin 2)

Auxiliary index function used in the square boundary decomposition.

Equations

• LeanPool.Monsky.p x y = !₂[x, y]

noncomputable def LeanPool.Monsky.squareBoundaryBasic (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : Fin 4 → Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

The basic boundary segments of the unit square lying on side i.

Equations

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

theorem LeanPool.Monsky.unitSquare_boundary_decomposition (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (hCovering : isTriangulation Δ) : triangulationBoundaryBasicSegments Δ = ⊤.biUnion (squareBoundaryBasic Δ)

theorem LeanPool.Monsky.unitSquare_cover_segmentSet {S : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))} (hCover : isCover (closedHull unitSquare) ↑S) {i : Fin 4} : squareBoundaryBig i ∈ segmentSet (triangulationPoints S)

theorem LeanPool.Monsky.unitSquare_boundary_intersections (i j : Fin 4) (h_neq : i ≠ j) : openHull (squareBoundaryBig i) ∩ openHull (squareBoundaryBig j) = ∅

theorem LeanPool.Monsky.purple_computation0 {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (i : Fin 4) : i ≠ 0 → isPurple v (squareBoundaryBig i) = 0

theorem LeanPool.Monsky.purple_computation1 {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) : isPurple v (squareBoundaryBig 0) = 1

theorem LeanPool.Monsky.open_triangle_in_open_square {Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))} {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hT : T ∈ Δ) (non_degen : det T ≠ 0) (hCovering : isTriangulation Δ) : openHull T ⊆ openHull unitSquare

theorem LeanPool.Monsky.segment_sum_odd {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (hCovering : isTriangulation Δ) (non_degen : ∀ P ∈ Δ, det P ≠ 0) : purpleSum v Δ % 4 = 2

theorem LeanPool.Monsky.segment_sum_rainbowTriangle {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : rainbowSum v Δ = (rainbowTriangles v Δ).card

noncomputable def LeanPool.Monsky.triangleBasicBoundary (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

The basic segments of a triangulation lying on the boundary of triangle T.

Equations

• LeanPool.Monsky.triangleBasicBoundary Δ T = {S ∈ LeanPool.Monsky.triangulationBasicSegments Δ | LeanPool.Monsky.closedHull S ⊆ LeanPool.Monsky.boundary T}

theorem LeanPool.Monsky.triangle_edges_disjoint (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (i j : Fin 3) (h : i ≠ j) (hdet : det T ≠ 0) : Disjoint (openHull (Tside T i)) (openHull (Tside T j))

theorem LeanPool.Monsky.triangleBoundary_decomposition {Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))} {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) (h : T ∈ Δ) : triangleBasicBoundary Δ T = ⊤.biUnion fun (i : Fin 3) => basicSegmentSegments (triangleBasicBoundary Δ T) (Tside T i)

noncomputable def LeanPool.Monsky.triangleBoundary (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

The three sides of a triangle T, as a set of segments.

Equations

• LeanPool.Monsky.triangleBoundary T = ⊤.biUnion fun (i : Fin 3) => {LeanPool.Monsky.Tside T i}

theorem LeanPool.Monsky.color_trichotomy (c : Color) : c = Color.Red ∨ c = Color.Blue ∨ c = Color.Green

theorem LeanPool.Monsky.different_points (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (h_det : det T ≠ 0) (i j : Fin 3) (hneq : i ≠ j) : T i ≠ T j

def LeanPool.Monsky.purpleB (a b : Color) : ℕ

The number (0, 1 or 2) of purple edges among the edges with two given colors.

Equations

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

def LeanPool.Monsky.rainbowB (a b c : Color) : ℕ

Indicator of whether the three given colors form a rainbow triangle.

Equations

• LeanPool.Monsky.rainbowB a b c = if (a == b || b == c || a == c) = true then 0 else 1

theorem LeanPool.Monsky.surj_iff_distinct (c0 c1 c2 : Color) : Function.Surjective ![c0, c1, c2] ↔ c0 ≠ c1 ∧ c1 ≠ c2 ∧ c0 ≠ c2

theorem LeanPool.Monsky.isPurple_eq_colors {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (S : Fin 2 → EuclideanSpace ℝ (Fin 2)) : isPurple v S = purpleB (coloring v (S 0)) (coloring v (S 1))

theorem LeanPool.Monsky.isRainbow_eq_colors {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : isRainbow v T = rainbowB (coloring v (T 0)) (coloring v (T 1)) (coloring v (T 2))

theorem LeanPool.Monsky.rainbow_purple_color_identity (c0 c1 c2 : Color) : 2 * rainbowB c0 c1 c2 % 4 = 2 * (purpleB c1 c2 + purpleB c2 c0 + purpleB c0 c1) % 4

theorem LeanPool.Monsky.rainbowTriangle_purpleSum {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) {Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))} (non_degen : ∀ P ∈ Δ, det P ≠ 0) (hDisjointCover : isDisjointCover (closedHull unitSquare) ↑Δ) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : T ∈ Δ → 2 * isRainbow v T % 4 = (∑ S ∈ triangleBasicBoundary Δ T, isPurple v S) % 4

theorem LeanPool.Monsky.boundary_filter_union (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : T ∈ Δ → {S ∈ triangulationBoundaryBasicSegments Δ ∪ triangulationInteriorBasicSegments Δ | closedHull S ⊆ boundary T} = {S ∈ triangulationBoundaryBasicSegments Δ | closedHull S ⊆ boundary T} ∪ {S ∈ triangulationInteriorBasicSegments Δ | closedHull S ⊆ boundary T}

theorem LeanPool.Monsky.boundary_filter_intersection (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (T : ↥Δ) : {S ∈ triangulationBoundaryBasicSegments Δ | closedHull S ⊆ boundary ↑T} ∩ {S ∈ triangulationInteriorBasicSegments Δ | closedHull S ⊆ boundary ↑T} = ∅

def LeanPool.Monsky.triangulationInteriorBasicSegmentsHulls (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : Set (Set (EuclideanSpace ℝ (Fin 2)))

The open hulls of the interior basic segments of a triangulation.

Equations

• LeanPool.Monsky.triangulationInteriorBasicSegmentsHulls Δ = {x : Set (EuclideanSpace ℝ (Fin 2)) | ∃ S ∈ LeanPool.Monsky.triangulationInteriorBasicSegments Δ, LeanPool.Monsky.openHull S = x}

theorem LeanPool.Monsky.basic_seg_non_degenerate {Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (h : S ∈ triangulationBasicSegments Δ) : S 0 ≠ S 1

theorem LeanPool.Monsky.interior_purpleSum {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : (∑ S ∈ triangulationInteriorBasicSegments Δ, isPurple v S) % 2 = 0 % 2

noncomputable def LeanPool.Monsky.boundaryIndicator (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (S : Fin 2 → EuclideanSpace ℝ (Fin 2)) : ℕ

Indicator of whether a segment lies on the boundary of the unit square.

Equations

• LeanPool.Monsky.boundaryIndicator T S = if LeanPool.Monsky.closedHull S ⊆ LeanPool.Monsky.boundary T then 1 else 0

theorem LeanPool.Monsky.triangleBasicBoundary_indicator_rw {Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))} (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) {f : (Fin 2 → EuclideanSpace ℝ (Fin 2)) → ℕ} : ∑ S ∈ triangleBasicBoundary Δ T, f S = ∑ S ∈ triangulationBasicSegments Δ, f S * boundaryIndicator T S

theorem LeanPool.Monsky.open_triangle_segment (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (S : Fin 2 → EuclideanSpace ℝ (Fin 2)) (hS : S ∈ triangulationBasicSegments Δ) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : T ∈ Δ → openHull T ∩ closedHull S = ∅

theorem LeanPool.Monsky.split_segment_sum (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (hDisjointCover : isDisjointCover (closedHull unitSquare) ↑Δ) (f : (Fin 2 → EuclideanSpace ℝ (Fin 2)) → ℕ) (non_degen : ∀ P ∈ Δ, det P ≠ 0) : ∑ T ∈ Δ, ∑ S ∈ triangleBasicBoundary Δ T, f S = ∑ S ∈ triangulationBoundaryBasicSegments Δ, f S + 2 * ∑ S ∈ triangulationInteriorBasicSegments Δ, f S

theorem LeanPool.Monsky.rainbowSum_is_purpleSum {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (hDisjointCover : isDisjointCover (closedHull unitSquare) ↑Δ) (non_degen : ∀ P ∈ Δ, det P ≠ 0) : 2 * rainbowSum v Δ % 4 = purpleSum v Δ % 4

theorem LeanPool.Monsky.monsky_rainbow {Γ₀ : Type} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation ℝ Γ₀) (Δ : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (hDisjointCover : isDisjointCover (closedHull unitSquare) ↑Δ) (non_degen : ∀ P ∈ Δ, det P ≠ 0) : ∃ T ∈ Δ, rainbowTriangle v T