LeanPool.TwoColoringOneRound.SimpleBounds

noncomputable def Distributed2Coloring.half : Rand

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.half = ⟨1 / 2, Distributed2Coloring.half._proof_2⟩

noncomputable def Distributed2Coloring.threshold (x : Rand) : Color

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.threshold x = if x < Distributed2Coloring.half then 0 else 1

theorem Distributed2Coloring.threshold_eq_zero_iff (x : Rand) : threshold x = 0 ↔ x < half

theorem Distributed2Coloring.threshold_eq_one_iff (x : Rand) : threshold x = 1 ↔ half ≤ x

theorem Distributed2Coloring.measurable_threshold : Measurable threshold

def Distributed2Coloring.g : Color → Color → Color → Color

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.g 0 0 0 = 1
• Distributed2Coloring.g 1 1 1 = 0
• Distributed2Coloring.g x✝² x✝¹ x✝ = x✝¹

theorem Distributed2Coloring.measurable_g : Measurable fun (t : Color × Color × Color) => g t.1 t.2.1 t.2.2

noncomputable def Distributed2Coloring.simpleUpperAlg : ClassicalAlgorithm

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

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

def Distributed2Coloring.side (b : Color) : Set Rand

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.side b = if b = 0 then Set.Iio Distributed2Coloring.half else Set.Ici Distributed2Coloring.half

theorem Distributed2Coloring.fin2_eq_one_of_ne_zero {b : Color} (hb : b ≠ 0) : b = 1

theorem Distributed2Coloring.side_measure (b : Color) : MeasureTheory.volume (side b) = 1 / 2

def Distributed2Coloring.cell (w : Fin 4 → Color) : Set (Samples 4)

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.cell w = Set.univ.pi fun (i : Fin 4) => Distributed2Coloring.side (w i)

theorem Distributed2Coloring.measurableSet_cell (w : Fin 4 → Color) : MeasurableSet (cell w)

theorem Distributed2Coloring.one_half_pow_four : (1 / 2) ^ 4 = 1 / 16

theorem Distributed2Coloring.cell_measure (w : Fin 4 → Color) : MeasureTheory.volume (cell w) = 1 / 16

def Distributed2Coloring.good (w : Fin 4 → Color) : Prop

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.good w = (Distributed2Coloring.g (w 0) (w 1) (w 2) = Distributed2Coloring.g (w 1) (w 2) (w 3))

theorem Distributed2Coloring.mem_cell_iff_threshold_eq (x : Samples 4) (w : Fin 4 → Color) : x ∈ cell w ↔ ∀ (i : Fin 4), threshold (x i) = w i

theorem Distributed2Coloring.pEvent_inter_cell_of_good {w : Fin 4 → Color} (hw : good w) : simpleUpperAlg.pEvent ∩ cell w = cell w

theorem Distributed2Coloring.pEvent_inter_cell_of_not_good {w : Fin 4 → Color} (hw : ¬good w) : simpleUpperAlg.pEvent ∩ cell w = ∅

theorem Distributed2Coloring.p_simpleUpperAlg : simpleUpperAlg.p = 1 / 4

theorem Distributed2Coloring.exists_algorithm_p_le_one_quarter : ∃ (alg : ClassicalAlgorithm), alg.p ≤ 1 / 4

theorem Distributed2Coloring.eq_of_ne_of_ne {x y z : Color} (hxy : x ≠ y) (hyz : y ≠ z) : z = x

theorem Distributed2Coloring.exists_monochromatic_edge (c : Fin 5 → Color) : ∃ (i : Fin 5), c i = c (i + 1)

noncomputable def Distributed2Coloring.nodeColor (alg : ClassicalAlgorithm) (x : Samples 5) (i : Fin 5) : Color

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.nodeColor alg x i = alg.f (x (i - 1), x i, x (i + 1))

def Distributed2Coloring.edgeEvent (alg : ClassicalAlgorithm) (i : Fin 5) : Set (Samples 5)

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

• Distributed2Coloring.edgeEvent alg i = {x : Distributed2Coloring.Samples 5 | Distributed2Coloring.nodeColor alg x i = Distributed2Coloring.nodeColor alg x (i + 1)}

theorem Distributed2Coloring.measurable_nodeColor (alg : ClassicalAlgorithm) (i : Fin 5) : Measurable fun (x : Samples 5) => nodeColor alg x i

theorem Distributed2Coloring.measurableSet_edgeEvent (alg : ClassicalAlgorithm) (i : Fin 5) : MeasurableSet (edgeEvent alg i)

theorem Distributed2Coloring.iUnion_edgeEvent_eq_univ (alg : ClassicalAlgorithm) : ⋃ (i : Fin 5), edgeEvent alg i = Set.univ

theorem Distributed2Coloring.edgeEvent_one_measure_eq_p (alg : ClassicalAlgorithm) : MeasureTheory.volume (edgeEvent alg 1) = alg.p

theorem Distributed2Coloring.edgeEvent_measure_eq_edgeEvent_one (alg : ClassicalAlgorithm) (i : Fin 5) : MeasureTheory.volume (edgeEvent alg i) = MeasureTheory.volume (edgeEvent alg 1)

theorem Distributed2Coloring.no_algorithm_p_lt_one_fifth : ¬∃ (alg : ClassicalAlgorithm), alg.p < 1 / 5