TileStructure.Forest.gtc_sum_Icc_le_two

lemma gtc_sum_Icc_le_two : ∑ k ∈ Finset.Icc (s J) S, (D : ℝ≥0∞) ^ ((s J - k) / (a : ℝ)) ≤ 2 := by  calc    _ = ∑ k ∈ Finset.Icc (s J) S, ((D : ℝ≥0∞) ^ (a : ℝ)⁻¹) ^ (s J - k) := by      congr with k; rw [← ENNReal.rpow_intCast, ← ENNReal.rpow_mul]; congr 1      rw [← div_eq_inv_mul, Int.cast_sub]    _ ≤ ∑ k ∈ Finset.Icc (s J) S, 2 ^ (s J - k) := by      gcongr with k mk; rw [← ENNReal.rpow_intCast, ← ENNReal.rpow_intCast]      apply ENNReal.rpow_le_rpow_of_nonpos (by simp_all)      rw [defaultD, Nat.cast_pow, Nat.cast_ofNat, ← ENNReal.rpow_natCast, ← ENNReal.rpow_mul]      nth_rw 1 [← ENNReal.rpow_one 2]; apply ENNReal.rpow_le_rpow_of_exponent_le one_le_two      rw [Nat.cast_mul, Nat.cast_pow, sq, mul_assoc, mul_self_mul_inv]      norm_cast      nlinarith [seven_le_c, four_le_a X]    _ = ∑ k ∈ Finset.Icc 0 (S - s J).toNat, 2 ^ (-k : ℤ) := by      have : s J ≤ S := scale_mem_Icc.2      apply Finset.sum_nbij' (fun (k : ℤ) ↦ (k - s J).toNat) (· + s J) <;> intro k hk      pick_goal -1      · rw [Finset.mem_Icc] at hk        rw [Int.toNat_of_nonneg (by lia), neg_sub]      all_goals simp only [Finset.mem_Icc] at hk ⊢; omega    _ ≤ ∑' k : ℕ, 2 ^ (-k : ℤ) := ENNReal.sum_le_tsum _    _ = _ := ENNReal.sum_geometric_two_pow_neg_one