sum_le_four_div_q_sub_one

lemma sum_le_four_div_q_sub_one (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q') {n : ℕ} :    ∑ i ∈ Finset.range n, ((2 : ℝ≥0∞)⁻¹ ^ i) ^ (q' : ℝ)⁻¹ ≤ (2 ^ 2 / (q - 1) : ℝ≥0) := by  have ltq' : 1 < q' := (NNReal.holderConjugate_iff.mp hqq'.symm).1  calc    _ = ∑ i ∈ Finset.range n, ((2 : ℝ≥0∞) ^ (-(q' : ℝ)⁻¹)) ^ i := by      congr! with i mi      simp_rw [← ENNReal.rpow_natCast, ENNReal.inv_rpow, ← ENNReal.rpow_neg, ← ENNReal.rpow_mul]      rw [mul_comm]    _ ≤ _ := ENNReal.sum_le_tsum _    _ = (1 - 2 ^ (-(q' : ℝ)⁻¹))⁻¹ := ENNReal.tsum_geometric _    _ ≤ 2 * (ENNReal.ofReal (q' : ℝ)⁻¹)⁻¹ := by      refine near_1_geometric_bound ⟨by positivity, ?_⟩      norm_cast; rw [inv_le_one_iff₀]; exact .inr ltq'.le    _ = ENNReal.ofNNReal (2 * q / (q - 1)) := by      rw [ENNReal.ofReal_inv_of_pos (by positivity), inv_inv, ofReal_coe_nnreal,        show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl, ← ENNReal.coe_mul]      rw [NNReal.holderConjugate_iff_eq_conjExponent hq.1] at hqq'      rw [hqq', mul_div_assoc]    _ ≤ _ := by rw [sq]; gcongr; exact hq.2