summand_bound_of_mem_verticalStrip

English

If z lies in a vertical strip with A,B and k ≥ 0, then the same bound as above holds with r at the left edge raised to (-k).

Русский

Если z лежит в вертикальной полосе с A,B и k ≥ 0, то выполняется аналогичное неравенство с r на левой границе в степени (-k).

LaTeX

$$$\\forall z \\in \\mathrm{verticalStrip}(A,B),\\; \\forall k \\ge 0,\\; \\forall x: \\mathbb{F}in 2 \\to \\mathbb{Z},\\; \\\\ \\|x_0 z + x_1\\|^{-k} \\le r\\langle\\langle A,B\\rangle,h_B\\rangle^{-k} \\|x\\|^{-k}$$$

Lean4

theorem summand_bound_of_mem_verticalStrip {k : ℝ} (hk : 0 ≤ k) (x : Fin 2 → ℤ) {A B : ℝ} (hB : 0 < B)
    (hz : z ∈ verticalStrip A B) : ‖x 0 * (z : ℂ) + x 1‖ ^ (-k) ≤ r ⟨⟨A, B⟩, hB⟩ ^ (-k) * ‖x‖ ^ (-k) :=
  by
  refine (summand_bound z hk x).trans (mul_le_mul_of_nonneg_right ?_ (by positivity))
  exact Real.rpow_le_rpow_of_nonpos (r_pos _) (r_lower_bound_on_verticalStrip z hB hz) (neg_nonpos.mpr hk)

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