English
Under appropriate smoothness and boundedness hypotheses, ||F f ε z|| ≤ 1 for z in the closed vertical strip.
Русский
При надлежащих условиях гладкости и ограниченности, ||F f ε z|| ≤ 1 для z внутри закрытой вертикальной полосы.
LaTeX
$$$\|F(f,\varepsilon)(z)\| \le 1$ for z ∈ verticalClosedStrip(0,1) under the stated hypotheses$$
Lean4
/-- When the function `f` is bounded above on a vertical strip, then so is `F`. -/
theorem F_BddAbove (f : ℂ → E) (ε : ℝ) (hε : ε > 0) (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1)) :
BddAbove ((norm ∘ (F f ε)) '' verticalClosedStrip 0 1) := by
-- Rewriting goal
simp only [F, comp_apply, invInterpStrip]
rw [bddAbove_def] at *
rcases hB with
⟨B, hB⟩
-- Using bound
use ((max 1 ((ε + sSupNormIm f 0) ^ (-(1 : ℝ)))) * max 1 ((ε + sSupNormIm f 1) ^ (-(1 : ℝ)))) * B
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
intro z hset
specialize
hB (‖f z‖)
(by simpa [image_congr, mem_image, comp_apply] using ⟨z, hset, rfl⟩)
-- Proof that the bound is correct
simp only [norm_smul, norm_mul, ← ofReal_add]
gcongr
-- Bounding individual terms
· by_cases hM0_one :
1 ≤
ε +
sSupNormIm f
0
-- `1 ≤ sSupNormIm f 0`
· apply le_trans _ (le_max_left _ _)
simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 0), sub_re, one_re,
Real.rpow_le_one_of_one_le_of_nonpos hM0_one (sub_nonpos.mpr hset.2)]
-- `0 < sSupNormIm f 0 < 1`
· rw [not_le] at hM0_one; apply le_trans _ (le_max_right _ _)
simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 0), sub_re, one_re]
apply Real.rpow_le_rpow_of_exponent_ge (sSupNormIm_eps_pos f hε 0) (le_of_lt hM0_one) _
simp only [neg_le_sub_iff_le_add, le_add_iff_nonneg_left, hset.1]
· by_cases hM1_one :
1 ≤
ε +
sSupNormIm f
1
-- `1 ≤ sSupNormIm f 1`
· apply le_trans _ (le_max_left _ _)
simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 1), neg_re,
Real.rpow_le_one_of_one_le_of_nonpos hM1_one (Right.neg_nonpos_iff.mpr hset.1)]
-- `0 < sSupNormIm f 1 < 1`
· rw [not_le] at hM1_one; apply le_trans _ (le_max_right _ _)
simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 1), neg_re,
Real.rpow_le_rpow_of_exponent_ge (sSupNormIm_eps_pos f hε 1) (le_of_lt hM1_one) (neg_le_neg_iff.mpr hset.2)]
