BKLNW.prop_3_sub_7

@[blueprint  "bklnw-prop-3-sub-7"  (title := "BKLNW Proposition 3, substep 7")  (statement := /-- $f(x) \leq f(x_0)$ for $x \in [x_0, 2^{\lfloor \frac{\log x_0}{\log 2} \rfloor + 1})$. -/)  (proof := /-- Follows since $f(x)$ decreases on $[2^{\lfloor \frac{\log x_0}{\log 2} \rfloor}, 2^{\lfloor \frac{\log x_0}{\log 2} \rfloor + 1})$. -/)  (latexEnv := "sublemma")  (discussion := 637)]theorem prop_3_sub_7 (x₀ : ℝ) (hx₀ : x₀ ≥ 2 ^ 9) (x : ℝ)    (hx : x ∈ Set.Ico x₀ (2 ^ (⌊(log x₀) / (log 2)⌋₊ + 1))) :    f x ≤ f x₀ := by  obtain ⟨hx_lo, hx_hi⟩ := hx  have hx₀_pos : 0 < x₀ := by positivity  have hlog2 : log 2 > 0 := log_pos one_lt_two  set n := ⌊(log x₀) / (log 2)⌋₊  have key : (2:ℝ)^((log x₀) / (log 2)) = x₀ := by    rw [rpow_def_of_pos (by norm_num), mul_comm, div_mul_cancel₀ _ hlog2.ne', exp_log hx₀_pos]  have hx₀_ge : x₀ ≥ 2^n := by    have : (n:ℝ) ≤ log x₀ / log 2 := Nat.floor_le (div_nonneg (log_nonneg (by linarith)) hlog2.le)    calc x₀ = 2^(log x₀ / log 2) := key.symm      _ ≥ 2^(n:ℝ) := rpow_le_rpow_of_exponent_le one_le_two this      _ = 2^n := rpow_natCast 2 n  have hx₀_lt : x₀ < 2^(n+1) := by    have : log x₀ / log 2 < n + 1 := Nat.lt_floor_add_one _    calc x₀ = 2^(log x₀ / log 2) := key.symm      _ < 2^((n:ℝ)+1) := rpow_lt_rpow_of_exponent_lt one_lt_two (by exact_mod_cast this)      _ = 2^(n+1) := by rw [← rpow_natCast]; norm_cast  have hn_ge : n ≥ 4 := by    by_contra! hcon    have : (2 : ℝ) ^ (n + 1) ≤ 2^9 := pow_le_pow_right₀ one_le_two <| by omega    linarith [hx₀, hx₀_lt]  rcases hx_lo.eq_or_lt with rfl | hlt  · rfl  · exact (prop_3_sub_2 n hn_ge ⟨hx₀_ge, hx₀_lt⟩ ⟨hx₀_ge.trans hx_lo, hx_hi⟩ hlt).le