English
sSupNormIm (scale f l u) 0 = sSupNormIm f l.
Русский
sSupNormIm (scale f l u) 0 = sSupNormIm f l.
LaTeX
$$$\\displaystyle sSupNormIm (\\text{scale } f\\, l\\, u)\\,0 = sSupNormIm f\\, l.$$$
Lean4
/-- The supremum of the norm of `scale f l u` on the line `z.re = 0` is the same as the supremum
of `f` on the line `z.re = l`. -/
theorem sSupNormIm_scale_left (f : ℂ → E) {l u : ℝ} (hul : l < u) : sSupNormIm (scale f l u) 0 = sSupNormIm f l :=
by
simp_rw [sSupNormIm, image_comp]
have : scale f l u '' (re ⁻¹' {0}) = f '' (re ⁻¹' { l }) :=
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 [hz₁, hz₂]
· 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 [hz₁]
· rw [div_mul_comm, div_self (by norm_cast; linarith)]
simp [hz₂]
rw [this]
