third_exception

lemma third_exception : volume (G₃ (X := X)) ≤ 2 ^ (-4 : ℤ) * volume G := by  calc    _ ≤ ∑' n, volume (⋃ k, ⋃ (_ : k ≤ n), ⋃ j, ⋃ (_ : j ≤ 2 * n + 3),        ⋃ p ∈ 𝔏₄ (X := X) k n j, (𝓘 p : Set X)) := measure_iUnion_le _    _ ≤ ∑' n, ∑' k, volume (⋃ (_ : k ≤ n), ⋃ j, ⋃ (_ : j ≤ 2 * n + 3),        ⋃ p ∈ 𝔏₄ (X := X) k n j, (𝓘 p : Set X)) := by gcongr; exact measure_iUnion_le _    _ = ∑' n, ∑' k, volume (if k ≤ n then ⋃ j, ⋃ (_ : j ≤ 2 * n + 3),        ⋃ p ∈ 𝔏₄ (X := X) k n j, (𝓘 p : Set X) else ∅) := by congr!; exact iUnion_eq_if _    _ = ∑' n, ∑' k, if k ≤ n then volume (⋃ j, ⋃ (_ : j ≤ 2 * n + 3),        ⋃ p ∈ 𝔏₄ (X := X) k n j, (𝓘 p : Set X)) else 0 := by congr!; split_ifs <;> simp    _ ≤ ∑' n, ∑' k, if k ≤ n then ∑' j, volume (⋃ (_ : j ≤ 2 * n + 3),        ⋃ p ∈ 𝔏₄ (X := X) k n j, (𝓘 p : Set X)) else 0 := by      gcongr; split_ifs      · exact measure_iUnion_le _      · exact le_rfl    _ ≤ ∑' n, ∑' k, if k ≤ n then ∑' j, volume (⋃ p ∈ 𝔏₄ (X := X) k n j, (𝓘 p : Set X)) else 0 := by      gcongr; split_ifs      · gcongr; exact iUnion_subset fun _ _ ↦ id      · exact le_rfl    _ ≤ ∑' n, ∑' k, if k ≤ n then ∑' (j : ℕ),        C5_2_9 X n * 2 ^ (9 * a - j : ℤ) * 2 ^ (n + k + 3) * volume G else 0 := by      gcongr; split_ifs      · gcongr; exact third_exception_aux      · exact le_rfl    _ = ∑' k, 2 ^ (9 * a + 4 + 2 * k) * D ^ (1 - κ * Z * (k + 1)) * volume G *        ∑' n, if k ≤ n then (2 * D ^ (-κ * Z) : ℝ≥0∞) ^ (n - k : ℝ) else 0 :=      third_exception_rearrangement    _ ≤ ∑' k, 2 ^ (9 * a + 4 + 2 * k) * D ^ (1 - κ * Z * (k + 1)) * volume G *        ∑' n, if k ≤ n then 2⁻¹ ^ (n - k : ℝ) else 0 := by      gcongr with k n; split_ifs with hnk      · refine ENNReal.rpow_le_rpow ?_ (by simpa using hnk)        calc          _ ≤ 2 * (2 : ℝ≥0∞) ^ (-100 : ℝ) := mul_le_mul_right (DκZ_le_two_rpow_100 (X := X)) 2          _ ≤ _ := by            nth_rw 1 [← ENNReal.rpow_one 2, ← ENNReal.rpow_add _ _ (by simp) (by simp),              ← ENNReal.rpow_neg_one 2]            exact ENNReal.rpow_le_rpow_of_exponent_le one_le_two (by norm_num)      · exact le_rfl    _ = ∑' k, 2 ^ (9 * a + 4 + 2 * k) * D ^ (1 - κ * Z * (k + 1)) * volume G *        ∑' (n : ℕ), 2 ^ (-(1 : ℕ) * n : ℤ) := by      congr! 3 with k; convert tsum_geometric_ite_eq_tsum_geometric with n hnk      rw [← ENNReal.rpow_neg_one, ← ENNReal.rpow_mul]; norm_cast    _ = ∑' k, 2 ^ (9 * a + 4 + 2 * k) * D ^ (1 - κ * Z * (k + 1)) * volume G * 2 := by      congr!; simpa using ENNReal.sum_geometric_two_pow_neg_one    _ = 2 ^ (9 * a + 5) * D ^ (1 - κ * Z) * volume G *        ∑' (k : ℕ), (2 : ℝ≥0∞) ^ (2 * k) * D ^ (-κ * Z * k) := by      rw [← ENNReal.tsum_mul_left]; congr with k      have lhsr :          (2 : ℝ≥0∞) ^ (9 * a + 4 + 2 * k) * D ^ (1 - κ * Z * (k + 1)) * volume G * 2 =          2 ^ (9 * a + 5) * 2 ^ (2 * k) * D ^ (1 - κ * Z * (k + 1)) * volume G := by ring      have rhsr :          (2 : ℝ≥0∞) ^ (9 * a + 5) * D ^ (1 - κ * Z) * volume G * (2 ^ (2 * k) * D ^ (-κ * Z * k)) =          2 ^ (9 * a + 5) * 2 ^ (2 * k) * (D ^ (1 - κ * Z) * D ^ (-κ * Z * k)) * volume G := by        ring      rw [lhsr, rhsr]; congr      rw [← ENNReal.rpow_add _ _ (by rw [defaultD]; simp) (by rw [defaultD]; simp)]      congr; ring    _ = 2 ^ (9 * a + 5) * D ^ (1 - κ * Z) * volume G *        ∑' k, ((2 : ℝ≥0∞) ^ 2 * D ^ (-κ * Z)) ^ k := by      congr! with k      rw [ENNReal.rpow_mul, ← ENNReal.rpow_natCast, Nat.cast_mul, ENNReal.rpow_mul 2,        ← ENNReal.mul_rpow_of_ne_top (by simp) (by simp), ENNReal.rpow_natCast]      congr 2; norm_cast    _ ≤ 2 ^ (9 * a + 5) * D ^ (1 - κ * Z) * volume G * ∑' k, 2⁻¹ ^ k := by      gcongr _ * ∑' _, ?_      refine pow_le_pow_left' ?_ _      calc        _ ≤ 2 ^ 2 * (2 : ℝ≥0∞) ^ (-100 : ℝ) := mul_le_mul_right (DκZ_le_two_rpow_100 (X := X)) _        _ ≤ _ := by          nth_rw 1 [← ENNReal.rpow_natCast, ← ENNReal.rpow_add _ _ (by simp) (by simp),            ← ENNReal.rpow_neg_one 2]          exact ENNReal.rpow_le_rpow_of_exponent_le one_le_two (by norm_num)    _ = 2 ^ (9 * a + 5) * D ^ (1 - κ * Z) * volume G * 2 := by      congr; convert ENNReal.sum_geometric_two_pow_neg_one with k      rw [← ENNReal.rpow_intCast, show (-k : ℤ) = (-k : ℝ) by norm_cast, ENNReal.rpow_neg,        ← ENNReal.inv_pow, ENNReal.rpow_natCast]    _ ≤ 2 ^ (9 * a + 5) * D ^ (-1 : ℝ) * volume G * 2 := by      gcongr      · exact_mod_cast one_le_realD _      · linarith [two_le_κZ (X := X)]    _ = 2 ^ (9 * a + 6 - 𝕔 * a ^ 2 : ℤ) * volume G := by      rw [← mul_rotate, ← mul_assoc, ← pow_succ', defaultD, Nat.cast_pow,        show ((2 : ℕ) : ℝ≥0∞) = 2 by rfl, ← ENNReal.rpow_natCast, ← ENNReal.rpow_natCast,        ← ENNReal.rpow_mul, ← ENNReal.rpow_add _ _ (by simp) (by simp), ← ENNReal.rpow_intCast]      congr 2; norm_num; ring    _ ≤ _ := by      gcongr      · norm_num      simp only [Int.reduceNeg, tsub_le_iff_right, le_neg_add_iff_add_le]      norm_cast      calc      4 + (9 * a + 6)      _ = 9 * a + 10 := by ring      _ ≤ 3 * 4 * a + 4 * 4 := by lia      _ ≤ 3 * a * a + a * a := by gcongr <;> linarith [four_le_a X]      _ = 4 * a ^ 2 := by ring      _ ≤ 𝕔 * a ^ 2 := by        gcongr        linarith [seven_le_c]