Final bound for the 3-parameter recursive algorithm

This file completes the computation of ClassicalAlgorithm.p recursive3ParamAlg and derives the numerical upper bound p < 24118/100000.

@[reducible, inline]

noncomputable abbrev Distributed2Coloring.UpperBound.Recursive3Param.μ : MeasureTheory.Measure Rand

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

Equations

• Distributed2Coloring.UpperBound.Recursive3Param.μ = MeasureTheory.volume

theorem Distributed2Coloring.UpperBound.Recursive3Param.Iio_one_ae_eq_univ : Set.Iio 1 =ᵐ[μ] Set.univ

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.constAboveT : ENNReal

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

Equations

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

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.gCt (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.

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.constT1T : ENNReal

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

Equations

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

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.constT2T2 : ENNReal

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

Equations

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

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.gCt2 (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.

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.gTB (b : 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.

noncomputable def Distributed2Coloring.UpperBound.Recursive3Param.gT2B (b : 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.gCt_eq_linear (c : Rand) : gCt c = ENNReal.ofReal ((2 * ↑t - 1) * ↑c) + ENNReal.ofReal (1 - ↑t)

theorem Distributed2Coloring.UpperBound.Recursive3Param.gCt2_eq_linear (c : Rand) : gCt2 c = ENNReal.ofReal ((2 * ↑t2 - 1) * ↑c) + ENNReal.ofReal (1 - ↑t2)

theorem Distributed2Coloring.UpperBound.Recursive3Param.gTB_eq_linear (b : Rand) : gTB b = ENNReal.ofReal ((2 * ↑t - 1) * ↑b) + ENNReal.ofReal (1 - ↑t)

theorem Distributed2Coloring.UpperBound.Recursive3Param.gT2B_eq_linear (b : Rand) : gT2B b = ENNReal.ofReal ((2 * ↑t2 - 1) * ↑b) + ENNReal.ofReal (1 - ↑t2)

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_constAboveT_of_t_lt_b {b c : Rand} (hb : t < b) (htc : t ≤ c) (hc1 : c ∈ Set.Iio 1) : innerBC b c = constAboveT

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_zero_of_t_lt_b_of_c_lt_t {b c : Rand} (hb : t < b) (hc : c < t) : innerBC b c = 0

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_gCt_of_t2_le_b_lt_t_of_c_lt_t1 {b c : Rand} (hb1 : t2 ≤ b) (hb2 : b < t) (hc : c < t1) : innerBC b c = gCt c

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_constT1T_of_t2_le_b_lt_t_of_t1_le_c_of_c_lt_t2 {b c : Rand} (hb1 : t2 ≤ b) (hb2 : b < t) (hc1 : t1 ≤ c) (hc2 : c < t2) : innerBC b c = constT1T

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_constT2T2_of_t2_le_b_lt_t_of_t2_le_c_of_c_lt_t {b c : Rand} (hb1 : t2 ≤ b) (hb2 : b < t) (hc1 : t2 ≤ c) (hc2 : c < t) : innerBC b c = constT2T2

Pointwise formulas for the remaining b-ranges

For b < t1 and for t1 ≤ b < t2, innerBC b c is still piecewise polynomial in b,c, and can be integrated explicitly.

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_gCt_of_b_lt_t1_of_c_lt_b {b c : Rand} (hb : b < t1) (hc : c < b) : innerBC b c = gCt c

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_gTB_of_b_lt_t1_of_b_le_c_of_c_lt_t {b c : Rand} (hb : b < t1) (hc1 : b ≤ c) (hc2 : c < t) : innerBC b c = gTB b

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_zero_of_b_lt_t1_of_t_le_c {b c : Rand} (hb : b < t1) (hc : t ≤ c) : innerBC b c = 0

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_gCt_of_t1_le_b_lt_t2_of_c_lt_t1 {b c : Rand} (hb1 : t1 ≤ b) (hb2 : b < t2) (hc : c < t1) : innerBC b c = gCt c

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_gCt2_of_t1_le_b_lt_t2_of_t1_le_c_of_c_lt_b {b c : Rand} (hb1 : t1 ≤ b) (hb2 : b < t2) (hc1 : t1 ≤ c) (hc2 : c < b) : innerBC b c = gCt2 c

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_gT2B_of_t1_le_b_lt_t2_of_b_le_c_of_c_lt_t2 {b c : Rand} (hb1 : t1 ≤ b) (hb2 : b < t2) (hc1 : b ≤ c) (hc2 : c < t2) : innerBC b c = gT2B b

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_constT1T_of_t1_le_b_lt_t2_of_t2_le_c_of_c_lt_t {b c : Rand} (hb1 : t1 ≤ b) (hb2 : b < t2) (hc1 : t2 ≤ c) (hc2 : c < t) : innerBC b c = constT1T

theorem Distributed2Coloring.UpperBound.Recursive3Param.innerBC_eq_zero_of_t1_le_b_lt_t2_of_t_lt_c {b c : Rand} (hb1 : t1 ≤ b) (hb2 : b < t2) (hc : t < c) : innerBC b c = 0

A 2D triangle integral swap

We use Tonelli/Fubini to evaluate integrals over regions of the form {(b,c) | c < b} without introducing subtractions at the ℝ≥0∞ level.

theorem Distributed2Coloring.UpperBound.Recursive3Param.lintegral_triangle_Iio (B : Rand) (f : Rand → ENNReal) (hf : Measurable f) : ∫⁻ (b : Rand) in Set.Iio B, ∫⁻ (c : Rand) in Set.Iio b, f c ∂μ ∂μ = ∫⁻ (c : Rand) in Set.Iio B, f c * μ (Set.Ioo c B) ∂μ

theorem Distributed2Coloring.UpperBound.Recursive3Param.lintegral_innerBC_Iio_one_of_t_lt_b {b : Rand} (hb : t < b) : ∫⁻ (c : Rand) in Set.Iio 1, innerBC b c ∂μ = constAboveT * μ (Set.Ico t 1)

theorem Distributed2Coloring.UpperBound.Recursive3Param.lintegral_b_above_t : ∫⁻ (b : Rand) in Set.Ico t 1, ∫⁻ (c : Rand) in Set.Iio 1, innerBC b c ∂μ ∂μ = constAboveT * μ (Set.Ico t 1) * μ (Set.Ico t 1)

theorem Distributed2Coloring.UpperBound.Recursive3Param.lintegral_b_t2_t : ∫⁻ (b : Rand) in Set.Ico t2 t, ∫⁻ (c : Rand) in Set.Iio 1, innerBC b c ∂μ ∂μ = μ (Set.Ico t2 t) * (∫⁻ (c : Rand) in Set.Iio t1, gCt c ∂μ + constT1T * μ (Set.Ico t1 t2) + constT2T2 * μ (Set.Ico t2 t))

theorem Distributed2Coloring.UpperBound.Recursive3Param.constAboveT_eq : constAboveT = ENNReal.ofReal (17 / 32)

Exact value of the constant constAboveT = t^2 + (1-t)^2.

theorem Distributed2Coloring.UpperBound.Recursive3Param.constT1T_eq : constT1T = ENNReal.ofReal (15 / 32)

Exact value of the constant constT1T = t1*t + (1-t1)*(1-t).

theorem Distributed2Coloring.UpperBound.Recursive3Param.constT2T2_eq : constT2T2 = ENNReal.ofReal (257 / 512)

Exact value of the constant constT2T2 = t2^2 + (1-t2)^2.

theorem Distributed2Coloring.UpperBound.Recursive3Param.lintegral_gCt_Iio_t1 : ∫⁻ (c : Rand) in Set.Iio t1, gCt c ∂μ = ENNReal.ofReal (81 / 512)

theorem Distributed2Coloring.UpperBound.Recursive3Param.lintegral_b_above_t_value : ∫⁻ (b : Rand) in Set.Ico t 1, ∫⁻ (c : Rand) in Set.Iio 1, innerBC b c ∂μ ∂μ = ENNReal.ofReal (153 / 2048)

Evaluate the b ≥ t region as an explicit rational value.

theorem Distributed2Coloring.UpperBound.Recursive3Param.lintegral_b_t2_t_value : ∫⁻ (b : Rand) in Set.Ico t2 t, ∫⁻ (c : Rand) in Set.Iio 1, innerBC b c ∂μ ∂μ = ENNReal.ofReal (13689 / 524288)