English
sSupNormIm (scale f l u) 1 = sSupNormIm f u.
Русский
sSupNormIm (scale f l u) 1 = sSupNormIm f u.
LaTeX
$$$\\displaystyle sSupNormIm (\\text{scale } f\\, l\\, u)\\,1 = sSupNormIm f\\, u.$$$
Lean4
/-- The supremum of the norm of `scale f l u` on the line `z.re = 1` is the same as
the supremum of `f` on the line `z.re = u`. -/
theorem sSupNormIm_scale_right (f : ℂ → E) {l u : ℝ} (hul : l < u) : sSupNormIm (scale f l u) 1 = sSupNormIm f u :=
by
simp_rw [sSupNormIm, image_comp]
have : scale f l u '' (re ⁻¹' { 1 }) = f '' (re ⁻¹' { u }) :=
by
ext e
simp only [scale, smul_eq_mul, mem_image, mem_preimage, mem_singleton_iff]
constructor
· intro h
obtain ⟨z, hz₁, hz₂⟩ := h
use ↑l + z * (↑u - ↑l)
simp only [add_re, ofReal_re, mul_re, hz₁, sub_re, one_mul, sub_im, ofReal_im, sub_self, mul_zero, sub_zero,
add_sub_cancel, hz₂, and_self]
· intro h
obtain ⟨z, hz₁, hz₂⟩ := h
use ((z - l) / (u - l))
constructor
· norm_cast
rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re]
simp only [sub_re, hz₁, ofReal_re, sub_im, ofReal_im, sub_zero, ofReal_sub, sub_self, mul_zero, zero_div,
add_zero]
rw [div_mul_eq_div_div_swap, mul_div_assoc, div_self (by norm_cast; linarith), mul_one,
div_self (by norm_cast; linarith)]
· rw [div_mul_comm, div_self (by norm_cast; linarith)]
simp only [one_mul, add_sub_cancel, hz₂]
rw [this]
