r_lower_bound_on_verticalStrip — Mathlib

English

If z lies in the vertical strip with left edge A and height B, then r at the left corner is no larger than r(z).

Русский

Если z лежит в вертикальном полосе с левой гранью A и высотой B, то r на левой границе не превышает r(z).

LaTeX

$$$ r\\bigl(\\langle \\langle A,B\\rangle, h\\rangle\\bigr) \\le r(z) \\quad \\text{for } z \\in \\mathrm{verticalStrip}(A,B) \\text{ with } B>0$$

Lean4

theorem r_lower_bound_on_verticalStrip {A B : ℝ} (h : 0 < B) (hz : z ∈ verticalStrip A B) : r ⟨⟨A, B⟩, h⟩ ≤ r z :=
  by
  apply min_le_min hz.2
  rw [Real.sqrt_le_sqrt_iff (by apply (r1_pos z).le)]
  simp only [r1_eq, div_pow, one_div]
  rw [inv_le_inv₀ (by positivity) (by positivity), add_le_add_iff_right, ← even_two.pow_abs]
  gcongr
  exacts [hz.1, hz.2]

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