BKLNW.prop_3_sub_6

@[blueprint  "bklnw-prop-3-sub-6"  (title := "BKLNW Proposition 3, substep 6")  (statement := /-- $f(x) \leq f(2^{\lfloor \frac{\log x_0}{\log 2} \rfloor + 1})$ on $[2^{\lfloor \frac{\log x_0}{\log 2} \rfloor + 1}, \infty)$. -/)  (proof := /-- Follows from Sublemmas \ref{bklnw-prop-3-sub-2} and \ref{bklnw-prop-3-sub-5}. -/)  (latexEnv := "sublemma")  (discussion := 636)]theorem prop_3_sub_6 (x₀ : ℝ) (hx₀ : x₀ ≥ 2 ^ 9) (x : ℝ)    (hx : x ≥ 2 ^ (⌊(log x₀) / (log 2)⌋₊ + 1)) :    f x ≤ f (2 ^ (⌊(log x₀)/(log 2)⌋₊ + 1)) := by  have hlog2 : log 2 > 0 := log_pos one_lt_two  have hx_pos : x > 0 := lt_of_lt_of_le (by positivity) hx  set m := ⌊(log x₀) / (log 2)⌋₊; set n := ⌊log x / log 2⌋₊  have hm : m ≥ 9 := Nat.le_floor <| (le_div_iff₀ hlog2).mpr <| by    rw [← log_pow]; exact Real.log_le_log (by positivity) hx₀  have hn : n ≥ m + 1 := Nat.le_floor <| (le_div_iff₀ hlog2).mpr <| by    rw [← log_pow]; exact Real.log_le_log (by positivity) hx  have key : x = 2 ^ (log x / log 2) := by    rw [rpow_def_of_pos two_pos, mul_comm, div_mul_cancel₀ _ hlog2.ne', exp_log hx_pos]  have hdiv : 0 ≤ log x / log 2 :=    div_nonneg (log_nonneg (hx.trans' (one_le_pow₀ one_le_two))) hlog2.le  have hlo : (2:ℝ)^n ≤ x := by    rw [key, ← rpow_natCast]; exact rpow_le_rpow_of_exponent_le one_le_two (Nat.floor_le hdiv)  have hhi : x < 2^(n+1) := by    rw [key, ← rpow_natCast]    exact rpow_lt_rpow_of_exponent_lt one_lt_two (by exact_mod_cast Nat.lt_floor_add_one _)  have hf_x : f x ≤ f (2^n) := by    by_cases hx_eq : x = 2^n; · simp [hx_eq]    exact (prop_3_sub_2 n (by omega)      ⟨le_rfl, by exact_mod_cast Nat.pow_lt_pow_right one_lt_two (Nat.lt_succ_self n)⟩      ⟨hlo, hhi⟩ (hlo.lt_of_ne' hx_eq)).le  calc f x ≤ f (2^n) := hf_x    _ ≤ f (2^(m+1)) := by      obtain ⟨d, hd⟩ := Nat.exists_eq_add_of_le hn      rw [hd]; clear hd      induction d with      | zero => rfl      | succ d ih =>        have hmd : m + 1 + d ≥ 9 := by omega        exact (prop_3_sub_5 _ hmd).le.trans ih