English
For any bounded B and any ε>0, there exists δ>0 such that for all q,r with |r| ≤ B and |q-r| ≤ δ, we have |q^n - r^n| < ε.
Русский
Для любого ограниченного множества величин B и любого ε>0 существует δ>0 такое, что для всех q,r с |r| ≤ B и |q-r| ≤ δ выполнено |q^n - r^n| < ε.
LaTeX
$$$\forall B>0, \forall ε>0, \forall n∈\mathbb{N}, \exists δ>0, \forall q,r,\; |r|≤B \rightarrow |q-r|≤δ \rightarrow |q^n - r^n|<ε$$$
Lean4
theorem uniform_continuous_npow_on_bounded (B : α) {ε : α} (hε : 0 < ε) (n : ℕ) :
∃ δ > 0, ∀ q r : α, |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε :=
by
wlog B_pos : 0 < B generalizing B
· have ⟨δ, δ_pos, cont⟩ := this 1 zero_lt_one
exact ⟨δ, δ_pos, fun q r hr ↦ cont q r (hr.trans ((le_of_not_gt B_pos).trans zero_le_one))⟩
have pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1) :=
zero_lt_one.trans_le <|
le_add_of_nonneg_right <|
mul_nonneg n.cast_nonneg <| (pow_pos (B_pos.trans <| lt_add_of_pos_right _ zero_lt_one) _).le
refine
⟨min 1 (ε / (1 + n * (B + 1) ^ (n - 1))), lt_min zero_lt_one (div_pos hε pos), fun q r hr hqr ↦
(abs_pow_sub_pow_le ..).trans_lt ?_⟩
rw [le_inf_iff, le_div_iff₀ pos, mul_one_add, ← mul_assoc] at hqr
obtain h | h := (abs_nonneg (q - r)).eq_or_lt
· simpa only [← h, zero_mul] using hε
refine (lt_of_le_of_lt ?_ <| lt_add_of_pos_left _ h).trans_le hqr.2
refine
mul_le_mul_of_nonneg_left (pow_le_pow_left₀ ((abs_nonneg _).trans le_sup_left) ?_ _)
(mul_nonneg (abs_nonneg _) n.cast_nonneg)
refine max_le ?_ (hr.trans <| le_add_of_nonneg_right zero_le_one)
exact add_sub_cancel r q ▸ (abs_add_le ..).trans (add_le_add hr hqr.1)
