BKLNW.prop_3_sub_2

@[blueprint  "bklnw-prop-3-sub-2"  (title := "BKLNW Proposition 3, substep 2")  (statement := /-- $f$ decreases on $[2^n, 2^{n+1})$.-/)  (proof := /-- Clear. -/)  (latexEnv := "sublemma")  (discussion := 632)]theorem prop_3_sub_2 (n : ℕ) (hn : n ≥ 4) : StrictAntiOn f (Set.Ico (2^n) (2^(n + 1))) := by  have hlog2 : (0 : ℝ) < log 2 := log_pos one_lt_two  have hfloor : ∀ x ∈ Set.Ico (2^n : ℝ) (2^(n+1)), ⌊log x / log 2⌋₊ = n := fun x ⟨hlo, hhi⟩ ↦ by    rw [Nat.floor_eq_iff <| div_nonneg (log_pos <| lt_of_lt_of_le (by      norm_cast; exact Nat.one_lt_two_pow (by omega)) hlo).le hlog2.le, le_div_iff₀ hlog2,        div_lt_iff₀ hlog2]    refine ⟨?_, ?_⟩    · calc (n : ℝ) * log 2 = log ((2 : ℝ)^n) := (log_pow 2 n).symm        _ ≤ log x := log_le_log (by positivity) hlo    · calc log x < log ((2 : ℝ)^(n+1)) := log_lt_log (lt_of_lt_of_le (by positivity : (0 : ℝ) < 2^n) hlo) hhi        _ = (↑n + 1) * log 2 := by rw [log_pow]; push_cast; ring  intro a ha b hb hab  simp only [f, hfloor a ha, hfloor b hb]  refine sum_lt_sum (fun k hk ↦ ?_) ⟨4, mem_Icc.mpr ⟨by omega, by omega⟩, ?_⟩  · rcases eq_or_ne k 3 with rfl | hk3    · simp    · have hk' : 3 < k := by simp only [mem_Icc] at hk; omega      exact (rpow_lt_rpow_of_neg (lt_of_lt_of_le (by positivity) ha.1) hab        (by have : (k:ℝ) > 3 := mod_cast hk'; field_simp; linarith)).le  · exact rpow_lt_rpow_of_neg (lt_of_lt_of_le (by positivity) ha.1) hab (by norm_num)