BKLNW.f_two_pow_le

lemma f_two_pow_le (b : ℝ) (hb : 0 < b) (K : ℕ) (hK : ⌊b / log 2⌋₊ = K) :    f ((2 : ℝ) ^ (K + 1)) ≤ ∑ k ∈ Finset.Icc 3 (K + 1), Real.exp (b * (1 / (k : ℝ) - 1 / 3)) := by  have hlog2 : (0 : ℝ) < log 2 := Real.log_pos one_lt_two  have h2pow : (1 : ℝ) ≤ (2 : ℝ) ^ (K + 1) := one_le_pow₀ (by norm_num)  have hidx : ⌊Real.log ((2 : ℝ) ^ (K + 1)) / Real.log 2⌋₊ = K + 1 := by    rw [Real.log_pow, mul_div_assoc, div_self hlog2.ne', mul_one, Nat.floor_natCast]  have hexp_le : Real.exp b ≤ (2 : ℝ) ^ (K + 1) := by    have hb_lt : b < ((K : ℝ) + 1) * Real.log 2 := by      have hfloor : b / Real.log 2 < (K : ℝ) + 1 := by        have := Nat.lt_floor_add_one (b / Real.log 2)        rw [hK] at this        exact_mod_cast this      calc b = (b / Real.log 2) * Real.log 2 := by field_simp        _ < ((K : ℝ) + 1) * Real.log 2 := by            exact mul_lt_mul_of_pos_right hfloor hlog2    calc Real.exp b ≤ Real.exp (((K : ℝ) + 1) * Real.log 2) := Real.exp_le_exp.mpr hb_lt.le      _ = (2 : ℝ) ^ (K + 1) := by          rw [mul_comm, Real.exp_mul, Real.exp_log (by norm_num : (0:ℝ) < 2),              show ((K : ℝ) + 1) = ((K + 1 : ℕ) : ℝ) by push_cast; ring,              Real.rpow_natCast]  unfold f  rw [hidx]  apply Finset.sum_le_sum  intro k hk  have hk3 : 3 ≤ k := (Finset.mem_Icc.mp hk).1  have hek : (1 : ℝ) / (k : ℝ) - 1 / 3 ≤ 0 := by    have hkr : (3 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk3    have : (1 : ℝ) / (k : ℝ) ≤ 1 / 3 := one_div_le_one_div_of_le (by norm_num) hkr    linarith  rw [Real.rpow_def_of_pos (by positivity : (0:ℝ) < (2:ℝ) ^ (K + 1))]  apply Real.exp_le_exp.mpr  have hlogs : b ≤ Real.log ((2 : ℝ) ^ (K + 1)) := by    calc b = Real.log (Real.exp b) := (Real.log_exp b).symm      _ ≤ Real.log ((2 : ℝ) ^ (K + 1)) :=          Real.log_le_log (Real.exp_pos b) hexp_le  nlinarith [hlogs, hek]