IBound_aux1

@[blueprint  (title := "IBound-aux1")  (statement := /--  Given a natural number $k$ and a real number $X_0 > 0$, there exists $C \geq 1$ so that for all $X \geq X_0$,  $$  \log^k X \le C \cdot X.  $$  -/)  (proof := /--  We use the fact that $\log^k X / X$ goes to $0$ as $X \to \infty$.  Then we use the extreme value theorem to find a constant $C$ that works for all $X \geq X_0$.  -/)  (latexEnv := "lemma")]lemma IBound_aux1 (X₀ : ℝ) (X₀pos : X₀ > 0) (k : ℕ) : ∃ C ≥ 1, ∀ X ≥ X₀, Real.log X ^ k ≤ C * X := by  -- When X is large, the ratio goes to 0.  have ⟨M, hM⟩ := Filter.eventually_atTop.mp (isLittleO_log_rpow_rpow_atTop k zero_lt_one).eventuallyLE  -- When X is small, use the extreme value theorem.  let f := fun X ↦ Real.log X ^ k / X  let I := Icc X₀ M  have : 0 ∉ I := notMem_Icc_of_lt X₀pos  have f_cont : ContinuousOn f (Icc X₀ M) :=    ((continuousOn_log.pow k).mono (subset_compl_singleton_iff.mpr this)).div    continuous_id.continuousOn (fun x hx ↦ ne_of_mem_of_not_mem hx this)  have ⟨C₁, hC₁⟩ := isCompact_Icc.exists_bound_of_continuousOn f_cont  use max C₁ 1, le_max_right C₁ 1  intro X hX  have Xpos : X > 0 := lt_of_lt_of_le X₀pos hX  by_cases hXM : X ≤ M  · rw[← div_le_iff₀ Xpos]    calc      f X ≤ ‖f X‖ := le_norm_self _      _ ≤ C₁ := hC₁ X ⟨hX, hXM⟩      _ ≤ max C₁ 1 := le_max_left C₁ 1  · calc      Real.log X ^ k ≤ ‖Real.log X ^ k‖ := le_norm_self _      _ ≤ ‖X ^ 1‖ := by exact_mod_cast hM X (by linarith[hXM])      _ = 1 * X := by        rw[pow_one, one_mul]        apply norm_of_nonneg        exact Xpos.le      _ ≤ max C₁ 1 * X := by        rw[mul_le_mul_iff_left₀ Xpos]        exact le_max_right C₁ 1