scale — Mathlib

English

The auxiliary scale f,l,u maps z ↦ f(l + z(u−l)); it is used to transfer bounds along the strip.

Русский

Вспомогательная шкала scale(f,l,u) задаёт z ↦ f(l + z(u−l)) и служит для переноса ограничений между полосами.

LaTeX

$$$\\text{scale }(f,l,u): \\mathbb{C} \\to E\\quad (z \\mapsto f\\bigl(l + z\\,(u - l)\\bigr)).$$$

Lean4

/-- An auxiliary function to prove the general statement of Hadamard's three lines theorem. -/
def scale (f : ℂ → E) (l u : ℝ) : ℂ → E := fun z ↦ f (l + z • (u - l))

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