English
Equality for interpStrip' given as 0 when bounds vanish, else a product of cpow terms.
Русский
Равенство interpStrip' при задании: 0, если пределы обращаются в нуль, иначе произведение cpow-частей.
LaTeX
$$$\\interpStrip'\\,f\\,l\\,u\\,z = \\begin{cases}0, & sSupNormIm f l = 0 \\lor sSupNormIm f u = 0, \\\\ sSupNormIm f l^{1 - ((z - l)/(u - l))} \\cdot sSupNormIm f u^{((z - l)/(u - l))}, & \\text{else}.\\end{cases}$$$
Lean4
theorem eventuallyle (z : ℂ) (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1))
(hd : DiffContOnCl ℂ f (verticalStrip 0 1)) (hz : z ∈ verticalStrip 0 1) :
(fun _ : ℝ ↦ ‖f z‖) ≤ᶠ[𝓝[>] 0] (fun ε ↦ ‖((ε + sSupNormIm f 0) ^ (1 - z) * (ε + sSupNormIm f 1) ^ z : ℂ)‖) := by
filter_upwards [self_mem_nhdsWithin] with ε (hε : 0 < ε) using
norm_le_interpStrip_of_mem_verticalClosedStrip_eps f ε hε z hB hd
(mem_of_mem_of_subset hz (preimage_mono Ioo_subset_Icc_self))
