Exact computation of ClassicalAlgorithm.p recursive3ParamAlg.

The final result is the dyadic rational value 94835 / 393216 ≈ 0.24117787679 < 24118/100000.

theorem Distributed2Coloring.UpperBound.Recursive3Param.aSlice_eq_of_t2_le_b_lt_t {b c : Rand} (hb1 : t2 ≤ b) (hb2 : b < t) : aSlice b c = if c < t2 then Set.Iic t else if c < t then Set.Iio t2 else ∅

theorem Distributed2Coloring.UpperBound.Recursive3Param.aSlice_eq_of_t_lt_b {b c : Rand} (hb : t < b) : aSlice b c = if c < t then Set.univ else if ↑c < 1 then Set.Iio t else ∅

theorem Distributed2Coloring.UpperBound.Recursive3Param.aSlice_eq_of_t1_le_b_lt_t2 {b c : Rand} (hb1 : t1 ≤ b) (hb2 : b < t2) : aSlice b c = if c < t1 then Set.Iic t else if c < b then Set.Iio t2 else if c < t2 then Set.Iic b else if c < t then Set.Iio t1 else ∅

Computing p

We now compute the exact value of ClassicalAlgorithm.p recursive3ParamAlg by evaluating the iterated lintegral from p_eq_lintegral_innerBC.

theorem Distributed2Coloring.UpperBound.Recursive3Param.RealHelpers.lintegral_ofReal_id_Icc (a b : ℝ) (ha : 0 ≤ a) (hab : a ≤ b) : ∫⁻ (x : ℝ) in Set.Icc a b, ENNReal.ofReal x = ENNReal.ofReal ((b ^ 2 - a ^ 2) / 2)

theorem Distributed2Coloring.UpperBound.Recursive3Param.RealHelpers.lintegral_ofReal_sub_id_Icc (r a b : ℝ) (hbr : b ≤ r) (hab : a ≤ b) : ∫⁻ (x : ℝ) in Set.Icc a b, ENNReal.ofReal (r - x) = ENNReal.ofReal (r * (b - a) - (b ^ 2 - a ^ 2) / 2)

theorem Distributed2Coloring.UpperBound.Recursive3Param.RealHelpers.lintegral_ofReal_mul_sub_Icc (r a b : ℝ) (ha : 0 ≤ a) (hbr : b ≤ r) (hab : a ≤ b) : ∫⁻ (x : ℝ) in Set.Icc a b, ENNReal.ofReal (x * (r - x)) = ENNReal.ofReal (r * (b ^ 2 - a ^ 2) / 2 - (b ^ 3 - a ^ 3) / 3)

theorem Distributed2Coloring.UpperBound.Recursive3Param.RealHelpers.lintegral_ofReal_pow_Icc (n : ℕ) (a b : ℝ) (ha : 0 ≤ a) (hab : a ≤ b) : ∫⁻ (x : ℝ) in Set.Icc a b, ENNReal.ofReal (x ^ n) = ENNReal.ofReal ((b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1))

theorem Distributed2Coloring.UpperBound.Recursive3Param.setLIntegral_ofReal_id_Icc (a b : Rand) (hab : a ≤ b) : ∫⁻ (x : Rand) in Set.Icc a b, ENNReal.ofReal ↑x = ENNReal.ofReal ((↑b ^ 2 - ↑a ^ 2) / 2)

theorem Distributed2Coloring.UpperBound.Recursive3Param.setLIntegral_ofReal_id_Iio (b : Rand) : ∫⁻ (x : Rand) in Set.Iio b, ENNReal.ofReal ↑x = ENNReal.ofReal ((↑b ^ 2 - 0 ^ 2) / 2)

theorem Distributed2Coloring.UpperBound.Recursive3Param.setLIntegral_ofReal_id_Ico (a b : Rand) (hab : a ≤ b) : ∫⁻ (x : Rand) in Set.Ico a b, ENNReal.ofReal ↑x = ENNReal.ofReal ((↑b ^ 2 - ↑a ^ 2) / 2)

theorem Distributed2Coloring.UpperBound.Recursive3Param.setLIntegral_ofReal_pow_Icc (n : ℕ) (a b : Rand) (hab : a ≤ b) : ∫⁻ (x : Rand) in Set.Icc a b, ENNReal.ofReal (↑x ^ n) = ENNReal.ofReal ((↑b ^ (n + 1) - ↑a ^ (n + 1)) / (↑n + 1))

theorem Distributed2Coloring.UpperBound.Recursive3Param.setLIntegral_ofReal_sub_id_Icc (r a b : Rand) (hab : a ≤ b) (hbr : ↑b ≤ ↑r) : ∫⁻ (x : Rand) in Set.Icc a b, ENNReal.ofReal (↑r - ↑x) = ENNReal.ofReal (↑r * (↑b - ↑a) - (↑b ^ 2 - ↑a ^ 2) / 2)

theorem Distributed2Coloring.UpperBound.Recursive3Param.setLIntegral_ofReal_mul_sub_Icc (r a b : Rand) (hab : a ≤ b) (hbr : ↑b ≤ ↑r) : ∫⁻ (x : Rand) in Set.Icc a b, ENNReal.ofReal (↑x * (↑r - ↑x)) = ENNReal.ofReal (↑r * (↑b ^ 2 - ↑a ^ 2) / 2 - (↑b ^ 3 - ↑a ^ 3) / 3)

theorem Distributed2Coloring.UpperBound.Recursive3Param.setLIntegral_ofReal_sub_id_Ico (r a b : Rand) (hab : a ≤ b) (hbr : ↑b ≤ ↑r) : ∫⁻ (x : Rand) in Set.Ico a b, ENNReal.ofReal (↑r - ↑x) = ENNReal.ofReal (↑r * (↑b - ↑a) - (↑b ^ 2 - ↑a ^ 2) / 2)

theorem Distributed2Coloring.UpperBound.Recursive3Param.setLIntegral_ofReal_mul_sub_Ico (r a b : Rand) (hab : a ≤ b) (hbr : ↑b ≤ ↑r) : ∫⁻ (x : Rand) in Set.Ico a b, ENNReal.ofReal (↑x * (↑r - ↑x)) = ENNReal.ofReal (↑r * (↑b ^ 2 - ↑a ^ 2) / 2 - (↑b ^ 3 - ↑a ^ 3) / 3)

theorem Distributed2Coloring.UpperBound.Recursive3Param.setLIntegral_ofReal_sub_id_Iio (r b : Rand) (hbr : ↑b ≤ ↑r) : ∫⁻ (x : Rand) in Set.Iio b, ENNReal.ofReal (↑r - ↑x) = ENNReal.ofReal (↑r * (↑b - 0) - (↑b ^ 2 - 0 ^ 2) / 2)

theorem Distributed2Coloring.UpperBound.Recursive3Param.setLIntegral_ofReal_mul_sub_Iio (r b : Rand) (hbr : ↑b ≤ ↑r) : ∫⁻ (x : Rand) in Set.Iio b, ENNReal.ofReal (↑x * (↑r - ↑x)) = ENNReal.ofReal (↑r * (↑b ^ 2 - 0 ^ 2) / 2 - (↑b ^ 3 - 0 ^ 3) / 3)