Commit 2025-01-31 17:41 ac2479cb

View on Github →

feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009) Make Hadamard's three lines theorem work on any vertical strip of the complex plane (i.e., the set of complex numbers of real part between l and u, provided l is less than u). Previously, the theorem would only work for l=0 and u=1. Moves:

norm_le_interp_of_mem_verticalClosedStrip -> norm_le_interp_of_mem_verticalClosedStrip₀₁
norm_le_interp_of_mem_verticalClosedStrip' -> norm_le_interp_of_mem_verticalClosedStrip₀₁'

Estimated changes

Modified Mathlib/Analysis/Complex/Hadamard.lean

modified theorem Complex.HadamardThreeLines.eventuallyle

added theorem Complex.HadamardThreeLines.interpStrip_scale

added theorem Complex.HadamardThreeLines.mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip

modified theorem Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip

added theorem Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip₀₁

modified theorem Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip'

added theorem Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip₀₁'

added theorem Complex.HadamardThreeLines.sSupNormIm_scale_left

added theorem Complex.HadamardThreeLines.sSupNormIm_scale_right

added def Complex.HadamardThreeLines.scale

added theorem Complex.HadamardThreeLines.scale_bddAbove

added theorem Complex.HadamardThreeLines.scale_bound_left

added theorem Complex.HadamardThreeLines.scale_bound_right

added theorem Complex.HadamardThreeLines.scale_diffContOnCl

added theorem Complex.HadamardThreeLines.scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip

added theorem Complex.HadamardThreeLines.scale_id_mem_verticalStrip_of_mem_verticalStrip