BKLNW.a2_crude_le

lemma a2_crude_le (b : ℝ) (hb : 0 ≤ b) :    Inputs.default.a₂ b ≤ (1 + Inputs.default.α) * ((⌊b / log 2⌋₊ : ℝ) + 1) := by  have hα : (0 : ℝ) ≤ Inputs.default.α := by    change (0 : ℝ) ≤ 1.93378e-8 * BKLNW_app.table_8_margin    norm_num [BKLNW_app.table_8_margin]  have hlog2 : (0 : ℝ) < log 2 := Real.log_pos one_lt_two  have hfe : f (exp b) ≤ (⌊b / log 2⌋₊ : ℝ) + 1 := by    have := f_crude_le (exp b) (Real.one_le_exp hb)    rw [Real.log_exp] at this    linarith  have hf2 : f ((2 : ℝ) ^ (⌊b / log 2⌋₊ + 1)) ≤ (⌊b / log 2⌋₊ : ℝ) + 1 := by    have h1 : (1 : ℝ) ≤ (2 : ℝ) ^ (⌊b / log 2⌋₊ + 1) := one_le_pow₀ (by norm_num)    have := f_crude_le ((2 : ℝ) ^ (⌊b / log 2⌋₊ + 1)) h1    rw [Real.log_pow] at this    rw [mul_div_assoc, div_self hlog2.ne', mul_one, Nat.floor_natCast] at this    push_cast at this ⊢    linarith  have hmax : max (f (exp b)) (f ((2 : ℝ) ^ (⌊b / log 2⌋₊ + 1))) ≤ (⌊b / log 2⌋₊ : ℝ) + 1 :=    max_le hfe hf2  unfold Inputs.a₂  gcongr