English
If f is sufficiently regular and bounded, then ||F f ε z|| ≤ 1 for z in verticalClosedStrip(0,1).
Русский
Если f достаточно гладкая и ограниченная, то ||F f ε z|| ≤ 1 для z внутри вертикальной закрытой полосы.
LaTeX
$$$\|F(f,\varepsilon)(z)\| \le 1$ for z in \mathrm{verticalClosedStrip}(0,1)$$
Lean4
theorem norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip (f : ℂ → E) (ε : ℝ) (hε : 0 < ε) (z : ℂ)
(hd : DiffContOnCl ℂ f (verticalStrip 0 1)) (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1))
(hz : z ∈ verticalClosedStrip 0 1) : ‖F f ε z‖ ≤ 1 :=
by
apply
PhragmenLindelof.vertical_strip (DiffContOnCl.smul (diffContOnCl_invInterpStrip f hε) hd) _
(fun x hx ↦ F_edge_le_one f ε hε x hB (Or.inl hx)) (fun x hx ↦ F_edge_le_one f ε hε x hB (Or.inr hx)) hz.1 hz.2
use 0
rw [sub_zero, div_one]
refine ⟨Real.pi_pos, ?_⟩
obtain ⟨BF, hBF⟩ := F_BddAbove f ε hε hB
simp only [comp_apply, mem_upperBounds, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hBF
use BF
rw [Asymptotics.isBigO_iff]
use 1
rw [eventually_inf_principal]
apply Eventually.of_forall
intro x hx
norm_num
exact
(hBF x ((preimage_mono Ioo_subset_Icc_self) hx)).trans ((le_of_lt (lt_add_one BF)).trans (Real.add_one_le_exp BF))
