top_tiles

lemma top_tiles : ∑ m with m ∈ 𝔐 (X := X) k n, volume (𝓘 m : Set X) ≤    2 ^ (n + k + 3) * volume G := by  set M := 𝔐 (X := X) k n  let Mc := M.toFinset.card  calc    _ = ∫⁻ t in Ioc 0 (Mc * 2 ^ (n + 1) : ℝ), layervol (X := X) k n t := top_tiles_aux    _ = ∑ l ∈ Finset.range Mc,        ∫⁻ t in Ioc ((l : ℝ) * 2 ^ (n + 1)) ((l + 1 : ℕ) * 2 ^ (n + 1)),          layervol (X := X) k n t := by      rw [Finset.range_eq_Ico, show (0 : ℝ) = (0 : ℕ) * 2 ^ (n + 1) by simp]      exact lintegral_Ioc_partition (by positivity)    _ ≤ ∑ l ∈ Finset.range Mc,        (((l + 1) * 2 ^ (n + 1) - l * 2 ^ (n + 1) : ℕ)) *          layervol (X := X) k n ((l * 2 ^ (n + 1) : ℕ) + 1) := by      convert! Finset.sum_le_sum fun _ _ ↦ lintegral_Ioc_layervol_le <;> simp    _ = 2 ^ (n + 1) * ∑ l ∈ Finset.range Mc, layervol (X := X) k n (l * 2 ^ (n + 1) + 1 : ℕ) := by      rw [Finset.mul_sum]; congr! 2      · rw [← Nat.mul_sub_right_distrib]; simp      · congr; simp    _ = 2 ^ (n + 1) * ∑ l ∈ Finset.range Mc, volume (setA (X := X) l k n) := by      unfold layervol setA stackSize; congr! 3; ext x      rw [mem_setOf, mem_setOf, indicator_sum_eq_natCast, Nat.cast_le]      exact Nat.add_one_le_iff    _ ≤ 2 ^ (n + 1) * ∑ l ∈ Finset.range Mc, 2 ^ (k + 1 - l : ℤ) * volume G :=      mul_le_mul_right (Finset.sum_le_sum fun _ _ ↦ john_nirenberg) _    _ ≤ 2 ^ (n + 1) * ∑' (l : ℕ), 2 ^ (k + 1 - l : ℤ) * volume G :=      mul_le_mul_right (ENNReal.sum_le_tsum _) _    _ = 2 ^ (n + 1) * (volume G * 2 ^ (k + 1) * 2) := by      conv_lhs =>        enter [2, 1, l]        rw [sub_eq_add_neg, ENNReal.zpow_add (by simp) (by simp), ← mul_rotate]      rw [ENNReal.tsum_mul_left]; congr 3      · norm_cast      · exact ENNReal.sum_geometric_two_pow_neg_one    _ = _ := by      nth_rw 3 [← pow_one 2]      rw [mul_rotate, ← pow_add, ← mul_assoc, ← pow_add,        show n + 1 + (k + 1 + 1) = n + k + 3 by lia]