exists_pow_btwn — Mathlib

English

For n ≠ 0, and x < y with 0 < y, there exists q ∈ K with 0 < q and x < q^n < y.

Русский

Для n ≠ 0 и x < y с 0 < y существует q ∈ K с 0 < q и x < q^n < y.

LaTeX

$$$\exists q\in K,\ 0

Lean4

theorem exists_pow_btwn {n : ℕ} (hn : n ≠ 0) {x y : K} (h : x < y) (hy : 0 < y) :
    ∃ q : K, 0 < q ∧ x < q ^ n ∧ q ^ n < y :=
  by
  have ⟨δ, δ_pos, cont⟩ := uniform_continuous_npow_on_bounded (max 1 y) (sub_pos.mpr <| max_lt_iff.mpr ⟨h, hy⟩) n
  have ex : ∃ m : ℕ, y ≤ (m * δ) ^ n :=
    by
    have ⟨m, hm⟩ := exists_nat_ge (y / δ + 1 / δ)
    refine ⟨m, le_trans ?_ (le_self_pow₀ ?_ hn)⟩ <;> rw [← div_le_iff₀ δ_pos]
    · exact (lt_add_of_pos_right _ <| by positivity).le.trans hm
    · exact (le_add_of_nonneg_left <| by positivity).trans hm
  let m := Nat.find ex
  have m_pos : 0 < m := (Nat.find_pos _).mpr <| by simpa [zero_pow hn] using hy
  let q := m.pred * δ
  have qny : q ^ n < y := lt_of_not_ge (Nat.find_min ex <| Nat.pred_lt m_pos.ne')
  have q1y : |q| < max 1 y :=
    (abs_eq_self.mpr <| by positivity).trans_lt <|
      lt_max_iff.mpr (or_iff_not_imp_left.mpr fun q1 ↦ (le_self_pow₀ (le_of_not_gt q1) hn).trans_lt qny)
  have xqn : max x 0 < q ^ n :=
    calc
      _ = y - (y - max x 0) := by rw [sub_sub_cancel]
      _ ≤ (m * δ) ^ n - (y - max x 0) := (sub_le_sub_right (Nat.find_spec ex) _)
      _ < (m * δ) ^ n - ((m * δ) ^ n - q ^ n) :=
        by
        refine sub_lt_sub_left ((le_abs_self _).trans_lt <| cont _ _ q1y.le ?_) _
        rw [← Nat.succ_pred_eq_of_pos m_pos, Nat.cast_succ, ← sub_mul, add_sub_cancel_left, one_mul,
          abs_eq_self.mpr (by positivity)]
      _ = q ^ n := sub_sub_cancel ..
  exact
    ⟨q, lt_of_le_of_ne (by positivity) fun q0 ↦ (le_sup_right.trans_lt xqn).ne <| q0 ▸ (zero_pow hn).symm,
      le_sup_left.trans_lt xqn, qny⟩

Похожие утверждения