l_upper_bound

lemma l_upper_bound : l < 2 ^ n := by  have ql1 : volume (E₂ l p') / volume (𝓘 p' : Set X) ≤ 1 := by    apply ENNReal.div_le_of_le_mul; rw [one_mul]; exact measure_mono (E₂_subset ..)  replace qp' := (lt_quotient_rearrange qp').trans_le ql1  rw [← ENNReal.mul_lt_mul_iff_left (c := 2 ^ (n : ℤ)) (by simp) (by simp), one_mul, mul_assoc,    ← ENNReal.zpow_add two_ne_zero ENNReal.ofNat_ne_top, neg_add_cancel, zpow_zero, mul_one,    show (2 ^ (n : ℤ) : ℝ≥0∞) = (2 ^ (n : ℤ) : ℝ≥0) by simp, ENNReal.coe_lt_coe,    zpow_natCast] at qp'  calc    _ ≤ l ^ a := le_self_pow₀ (one_le_two.trans hl) (by linarith [four_le_a X])    _ ≤ 2 ^ (4 * a) * l ^ a := by      nth_rw 1 [← one_mul (l ^ a)]; gcongr; exact_mod_cast Nat.one_le_two_pow    _ < _ := qp'