Computation of ClassicalAlgorithm.p for recursive3ParamAlg.

This file will prove that the 3-parameter recursive cutoff algorithm from Distributed2Coloring/UpperBound/Recursive3Param.lean satisfies ClassicalAlgorithm.p recursive3ParamAlg < 24118/100000.

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.μ4 (i : Fin 4) : MeasureTheory.Measure Rand

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

Equations

• Distributed2Coloring.UpperBound.Recursive3Param.μ4 i = if i = i then MeasureTheory.volume else MeasureTheory.volume

@[reducible, inline]

abbrev Distributed2Coloring.UpperBound.Recursive3Param.E : Set (Samples 4)

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

Equations

• Distributed2Coloring.UpperBound.Recursive3Param.E = Distributed2Coloring.UpperBound.Recursive3Param.recursive3ParamAlg.pEvent

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.pInd : Samples 4 → ENNReal

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

Equations

• Distributed2Coloring.UpperBound.Recursive3Param.pInd = Distributed2Coloring.UpperBound.Recursive3Param.E.indicator fun (x : Distributed2Coloring.Samples 4) => 1

theorem Distributed2Coloring.UpperBound.Recursive3Param.measurable_pInd : Measurable pInd

theorem Distributed2Coloring.UpperBound.Recursive3Param.p_eq_lintegral_pInd : recursive3ParamAlg.p = ∫⁻ (x : Samples 4), pInd x

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.dSlice (x : Samples 4) : Set Rand

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

Equations

• Distributed2Coloring.UpperBound.Recursive3Param.dSlice x = {d : Distributed2Coloring.Rand | Function.update x 3 d ∈ Distributed2Coloring.UpperBound.Recursive3Param.E}

theorem Distributed2Coloring.UpperBound.Recursive3Param.measurableSet_dSlice (x : Samples 4) : MeasurableSet (dSlice x)

theorem Distributed2Coloring.UpperBound.Recursive3Param.dSlice_eq (x : Samples 4) : dSlice x = if x 2 < z0I (x 0) (x 1) then Set.Iio (z0I (x 1) (x 2)) else Set.Ici (z0I (x 1) (x 2))

theorem Distributed2Coloring.UpperBound.Recursive3Param.lmarginal_D (x : Samples 4) : (∫⋯∫⁻_{3}, pInd ∂μ4) x = if x 2 < z0I (x 0) (x 1) then ENNReal.ofReal ↑(z0I (x 1) (x 2)) else ENNReal.ofReal (1 - ↑(z0I (x 1) (x 2)))

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.aSlice (b c : Rand) : Set Rand

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

Equations

• Distributed2Coloring.UpperBound.Recursive3Param.aSlice b c = {a : Distributed2Coloring.Rand | c < Distributed2Coloring.UpperBound.Recursive3Param.z0I a b}

Explicit descriptions of aSlice

For our concrete dyadic parameters, aSlice b c = {a | c < z0(a,b)} is (away from boundary values) always an interval in a. The following lemmas give exact set descriptions under hypotheses on b.

theorem Distributed2Coloring.UpperBound.Recursive3Param.aSlice_eq_of_b_lt_t1 {b c : Rand} (hb : b < t1) : aSlice b c = if c < b then Set.Iio t else if c < t then Set.Iic b else ∅

theorem Distributed2Coloring.UpperBound.Recursive3Param.measurableSet_aSlice (b c : Rand) : MeasurableSet (aSlice b c)

theorem Distributed2Coloring.UpperBound.Recursive3Param.lintegral_ite_const {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) (a b : ENNReal) : ∫⁻ (x : α), if x ∈ s then a else b ∂μ = a * μ s + b * μ sᶜ

theorem Distributed2Coloring.UpperBound.Recursive3Param.lmarginal_AD (x : Samples 4) : (∫⋯∫⁻_{0, 3}, pInd ∂μ4) x = ENNReal.ofReal ↑(z0I (x 1) (x 2)) * MeasureTheory.volume (aSlice (x 1) (x 2)) + ENNReal.ofReal (1 - ↑(z0I (x 1) (x 2))) * MeasureTheory.volume (aSlice (x 1) (x 2))ᶜ

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.innerBC (b c : Rand) : ENNReal

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

Equations

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

theorem Distributed2Coloring.UpperBound.Recursive3Param.lmarginal_AD_eq_innerBC (x : Samples 4) : (∫⋯∫⁻_{0, 3}, pInd ∂μ4) x = innerBC (x 1) (x 2)

theorem Distributed2Coloring.UpperBound.Recursive3Param.p_eq_lintegral_innerBC : recursive3ParamAlg.p = ∫⁻ (b : Rand) (c : Rand), innerBC b c