Log tendsto inverse

log.lean

import Mathlib

lemma foo: Filter.Tendsto ((fun x => x⁻¹) ∘ fun x => Real.log x / x) Filter.atTop Filter.atTop := by
  have bar := Filter.Tendsto.comp (f := fun x => Real.log x / x) (g := fun x => x⁻¹) (x := Filter.atTop) (y := (nhdsWithin 0 (Set.Ioi 0))) (z := Filter.atTop) ?_ ?_
  .
    exact bar
  . 
    exact tendsto_inv_nhdsGT_zero (𝕜 := ℝ)
  . 
    rw [tendsto_nhdsWithin_iff]
    refine ⟨?_, ?_⟩
    . 
      have log_div_x := Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 (by simp)
      simp at log_div_x
      exact log_div_x
    . simp
      use 2
      intro x hx
      have log_pos: 0 < Real.log x := by
        refine (Real.log_pos_iff ?_).mpr ?_ <;> linarith
      positivity

  






lemma other  (a b : ℝ) (n : ℕ) (ha : a > 0):  Filter.Tendsto ((fun x => x⁻¹) ∘ fun x => Real.log x ^ n / (a*x + b)) Filter.atTop Filter.atTop := by
  have bar := Filter.Tendsto.comp (f := fun x => Real.log x ^ n / (a*x + b)) (g := fun x => x⁻¹) (x := Filter.atTop) (y := (nhdsWithin 0 (Set.Ioi 0))) (z := Filter.atTop) ?_ ?_
  .
    exact bar
  . 
    exact tendsto_inv_nhdsGT_zero (𝕜 := ℝ)
  . 
    rw [tendsto_nhdsWithin_iff]
    refine ⟨?_, ?_⟩
    . 
      have log_div_x := Real.tendsto_pow_log_div_mul_add_atTop a b n (by linarith)
      simp at log_div_x
      exact log_div_x
    . simp
      use max 2 (1 + -b/a)
      intro x hx
      simp at hx
      obtain ⟨x_gt_two, x_other⟩ := hx
      have div_a_lt: -b/a < x := by
        linarith
      have ax_gt_b: -b < a*x := by
        have foo := div_lt_iff₀ (a := x) (b := -b) (c := a) (by linarith)
        apply foo.mp at div_a_lt
        rw [mul_comm]
        exact div_a_lt

      have log_pos: 0 < Real.log x := by
        refine (Real.log_pos_iff ?_).mpr ?_
        . linarith
        . linarith
      
      have log_pow_pos: 0 < Real.log x ^n := by
        simp [log_pos]

      have ax_pos: 0 < a*x := by
        positivity

      have denom_pos: 0 < (a * x + b) := by
        by_cases b_pos: 0 < b
        . linarith
        . 
          simp at b_pos
          rw [← neg_neg b]
          rw [← sub_eq_add_neg]
          apply sub_pos_of_lt
          exact ax_gt_b

      positivity