Lemma 5.1.1 (#78)

Carleson/DiscreteCarleson.lean

@@ -476,7 +476,18 @@ lemma third_exception : volume (G₃ (X := X)) ≤ 2 ^ (- 4 : ℤ) * volume G :=
 
 /-- Lemma 5.1.1 -/
 lemma exceptional_set : volume (G' : Set X) ≤ 2 ^ (- 2 : ℤ) * volume G :=
-  sorry
+  calc volume G'
+    _ ≤ volume G₁ + volume G₂ + volume G₃ :=
+      le_add_of_le_add_right (measure_union_le _ G₃) (measure_union_le _ _)
+    _ ≤ 2 ^ (- 4 : ℤ) * volume G + 2 ^ (- 4 : ℤ) * volume G + 2 ^ (- 4 : ℤ) * volume G :=
+      add_le_add_three first_exception second_exception third_exception
+    _ = (3 : ℝ≥0∞) * 2 ^ (-4 : ℤ) * volume G := by ring
+    _ ≤ 2 ^ (- 2 : ℤ) * volume G :=
+      have coefficient_inequality : (3 : ℝ≥0∞) * 2 ^ (-4 : ℤ) ≤ (2 : ℝ≥0∞) ^ (-2 : ℤ) := by
+        change ((3 : ℝ≥0) : ℝ≥0∞) * (2 : ℝ≥0) ^ (-4 : ℤ) ≤ (2 : ℝ≥0) ^ (-2 : ℤ)
+        repeat rw [← ENNReal.coe_zpow (show (2 : ℝ≥0) ≠ 0 by norm_num)]
+        rw_mod_cast [← NNReal.coe_le_coe]; norm_num
+      mul_le_mul_right' coefficient_inequality _
 
 /-! ## Section 5.3 -/