English
For z in verticalStrip 0 1 and hd, hB, the bound ‖f z‖ ≤ ‖interpStrip f z‖ holds; the interpolant dominates the function norm.
Русский
Для z в вертикальной полосе 0 1 и при hd, hB выполняется: ‖f z‖ ≤ ‖interpStrip f z‖.
LaTeX
$$$\\|f(z)\\| \\le \\|\\interpStrip f z\\|,$ для всех $z ∈ \\text{verticalStrip } 0 1$ при подходящих условиях.$$
Lean4
theorem norm_le_interpStrip_of_mem_verticalStrip_zero (z : ℂ) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
(hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1)) (hz : z ∈ verticalStrip 0 1) : ‖f z‖ ≤ ‖interpStrip f z‖ :=
by
apply tendsto_le_of_eventuallyLE _ _ (eventuallyle f z hB hd hz)
·
simp only [tendsto_const_nhds_iff]
-- Proof that we can let epsilon tend to zero.
· rw [interpStrip_eq_of_mem_verticalStrip _ _ hz]
convert ContinuousWithinAt.tendsto _ using 2
· simp only [ofReal_zero, zero_add]
· simp_rw [← ofReal_add]
have :
∀ x ∈ Ioi 0,
(x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
‖((x + sSupNormIm f 0 : ℝ) ^ (1 - z) * (x + sSupNormIm f 1 : ℝ) ^ z : ℂ)‖ :=
by
intro x hx
simp only [norm_mul]
repeat rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]
· simp only [sub_re, one_re]
· simpa using (ne_comm.mpr (ne_of_lt hz.1))
· simpa [sub_eq_zero] using (ne_comm.mpr (ne_of_lt hz.2))
apply tendsto_nhdsWithin_congr this _
simp only [zero_add]
rw [norm_mul, norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _,
norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _]
· apply Tendsto.mul
· apply Tendsto.rpow_const
· nth_rw 2 [← zero_add (sSupNormIm f 0)]
exact
Tendsto.add_const (sSupNormIm f 0)
(tendsto_nhdsWithin_of_tendsto_nhds (Continuous.tendsto continuous_id' _))
· right; simp only [sub_nonneg, le_of_lt hz.2]
· apply Tendsto.rpow_const
· nth_rw 2 [← zero_add (sSupNormIm f 1)]
exact
Tendsto.add_const (sSupNormIm f 1)
(tendsto_nhdsWithin_of_tendsto_nhds (Continuous.tendsto continuous_id' _))
· right; simp only [le_of_lt hz.1]
· simpa using (ne_comm.mpr (ne_of_lt hz.1))
· simpa [sub_eq_zero] using (ne_comm.mpr (ne_of_lt hz.2))
