BKLNW.a2_mid_le

lemma a2_mid_le (b : ℝ) (hb : 0 < b) (K : ℕ) (hK : ⌊b / log 2⌋₊ = K) (h12 : 12 ≤ K) :    Inputs.default.a₂ b ≤ (1 + Inputs.default.α) *      ((∑ k ∈ Finset.Icc (3:ℕ) 12, Real.exp (b * (1 / (k : ℝ) - 1 / 3))) +        ((K : ℝ) - 11) * Real.exp (b * (1 / 13 - 1 / 3))) := by  have hα : (0 : ℝ) ≤ Inputs.default.α := by    change (0 : ℝ) ≤ 1.93378e-8 * BKLNW_app.table_8_margin    norm_num [BKLNW_app.table_8_margin]  -- the common dominating sum, with the k = 13.. tail collapsed  set S : ℝ := (∑ k ∈ Finset.Icc (3:ℕ) 12, Real.exp (b * (1 / (k : ℝ) - 1 / 3))) +      ((K : ℝ) - 11) * Real.exp (b * (1 / 13 - 1 / 3)) with hS  have hsplit : ∀ (M : ℕ), 12 ≤ M →      (∑ k ∈ Finset.Icc 3 M, Real.exp (b * (1 / (k : ℝ) - 1 / 3))) ≤      (∑ k ∈ Finset.Icc (3:ℕ) 12, Real.exp (b * (1 / (k : ℝ) - 1 / 3))) +        ((M : ℝ) - 12) * Real.exp (b * (1 / 13 - 1 / 3)) := by    intro M hM    have hunion : Finset.Icc 3 M = Finset.Icc (3:ℕ) 12 ∪ Finset.Icc 13 M := by      ext a      simp only [Finset.mem_Icc, Finset.mem_union]      omega    rw [hunion, Finset.sum_union (by      apply Finset.disjoint_left.mpr      intro a ha hb'      have h1 := (Finset.mem_Icc.mp ha).2      have h2 := (Finset.mem_Icc.mp hb').1      omega)]    refine add_le_add le_rfl ?_    calc (∑ k ∈ Finset.Icc 13 M, Real.exp (b * (1 / (k : ℝ) - 1 / 3)))        ≤ (Finset.Icc 13 M).card • Real.exp (b * (1 / 13 - 1 / 3)) := by          apply Finset.sum_le_card_nsmul          intro k hk          have hk13 : 13 ≤ k := (Finset.mem_Icc.mp hk).1          apply Real.exp_le_exp.mpr          have hkr : (13 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk13          have : (1 : ℝ) / (k : ℝ) ≤ 1 / 13 := one_div_le_one_div_of_le (by norm_num) hkr          nlinarith [hb]      _ ≤ ((M : ℝ) - 12) * Real.exp (b * (1 / 13 - 1 / 3)) := by          rw [nsmul_eq_mul, Nat.card_Icc]          have : ((M + 1 - 13 : ℕ) : ℝ) ≤ (M : ℝ) - 12 := by            have h13 : 13 ≤ M + 1 := by omega            rw [Nat.cast_sub h13]            push_cast            linarith          exact mul_le_mul_of_nonneg_right this (Real.exp_pos _).le  have hfe : f (Real.exp b) ≤ S := by    rw [f_exp_eq b K hK, hS]    calc (∑ k ∈ Finset.Icc 3 K, Real.exp (b * (1 / (k : ℝ) - 1 / 3)))        ≤ (∑ k ∈ Finset.Icc (3:ℕ) 12, Real.exp (b * (1 / (k : ℝ) - 1 / 3))) +            ((K : ℝ) - 12) * Real.exp (b * (1 / 13 - 1 / 3)) := hsplit K h12      _ ≤ _ := by          refine add_le_add le_rfl (mul_le_mul_of_nonneg_right ?_ (Real.exp_pos _).le)          linarith  have hf2 : f ((2 : ℝ) ^ (K + 1)) ≤ S := by    refine (f_two_pow_le b hb K hK).trans ?_    rw [hS]    calc (∑ k ∈ Finset.Icc 3 (K + 1), Real.exp (b * (1 / (k : ℝ) - 1 / 3)))        ≤ (∑ k ∈ Finset.Icc (3:ℕ) 12, Real.exp (b * (1 / (k : ℝ) - 1 / 3))) +            (((K + 1 : ℕ) : ℝ) - 12) * Real.exp (b * (1 / 13 - 1 / 3)) := hsplit (K + 1) (by omega)      _ ≤ _ := by          refine add_le_add le_rfl (mul_le_mul_of_nonneg_right ?_ (Real.exp_pos _).le)          push_cast; linarith  have hmax : max (f (Real.exp b)) (f ((2 : ℝ) ^ (⌊b / log 2⌋₊ + 1))) ≤ S := by    rw [hK]    exact max_le hfe hf2  unfold Inputs.a₂  gcongr