Remaining region computations for the 3-parameter recursive algorithm

This file computes the contributions to ClassicalAlgorithm.p recursive3ParamAlg coming from the b < t1 and t1 ≤ b < t2 regions.

theorem Distributed2Coloring.UpperBound.Recursive3Param.gCt_eq_affine (c : Rand) : gCt c = ENNReal.ofReal (1 / 4) * ENNReal.ofReal ↑c + ENNReal.ofReal (3 / 8)

theorem Distributed2Coloring.UpperBound.Recursive3Param.gTB_eq_affine (b : Rand) : gTB b = ENNReal.ofReal (1 / 4) * ENNReal.ofReal ↑b + ENNReal.ofReal (3 / 8)

theorem Distributed2Coloring.UpperBound.Recursive3Param.gCt2_eq_affine (c : Rand) : gCt2 c = ENNReal.ofReal (1 / 16) * ENNReal.ofReal ↑c + ENNReal.ofReal (15 / 32)

theorem Distributed2Coloring.UpperBound.Recursive3Param.gT2B_eq_affine (b : Rand) : gT2B b = ENNReal.ofReal (1 / 16) * ENNReal.ofReal ↑b + ENNReal.ofReal (15 / 32)

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

theorem Distributed2Coloring.UpperBound.Recursive3Param.lintegral_b_below_t1_value : ∫⁻ (b : Rand) in Set.Iio t1, ∫⁻ (c : Rand) in Set.Iio 1, innerBC b c ∂μ ∂μ = ENNReal.ofReal (99 / 1024)

t1 ≤ b < t2 region

For t1 ≤ b < t2, the integrand splits into four c-regions: c < t1, t1 ≤ c < b, b ≤ c < t2, and t2 ≤ c < t (with zero contribution for c ≥ t).

theorem Distributed2Coloring.UpperBound.Recursive3Param.lintegral_innerBC_Iio_one_of_t1_le_b_lt_t2 {b : Rand} (hb1 : t1 ≤ b) (hb2 : b < t2) : ∫⁻ (c : Rand) in Set.Iio 1, innerBC b c ∂μ = ∫⁻ (c : Rand) in Set.Iio t1, gCt c ∂μ + gT2B b * μ (Set.Ico b t2) + constT1T * μ (Set.Ico t2 t) + ∫⁻ (c : Rand) in Set.Ico t1 b, gCt2 c ∂μ

theorem Distributed2Coloring.UpperBound.Recursive3Param.lintegral_b_t1_t2_value : ∫⁻ (b : Rand) in Set.Ico t1 t2, ∫⁻ (c : Rand) in Set.Iio 1, innerBC b c ∂μ ∂μ = ENNReal.ofReal (68705 / 1572864)