Commit 2024-05-07 09:50 04771772

View on Github →

feat: Hadamard three-lines theorem (#7919) This PR introduces a version of the Hadamard three-lines theorem (see here), which is a prerequisite for norm interpolation. This project was suggested by @dupuisf earlier this year. This is my first decently sized PR so thank you for your patience if I have made any mistakes!

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/Hadamard.lean

added theorem Complex.HadamardThreeLines.F_BddAbove

added theorem Complex.HadamardThreeLines.F_edge_le_one

added theorem Complex.HadamardThreeLines.abs_invInterpStrip

added theorem Complex.HadamardThreeLines.diffContOnCl_interpStrip

added theorem Complex.HadamardThreeLines.diffContOnCl_invInterpStrip

added theorem Complex.HadamardThreeLines.eventuallyle

added theorem Complex.HadamardThreeLines.interpStrip_eq_of_mem_verticalStrip

added theorem Complex.HadamardThreeLines.interpStrip_eq_of_pos

added theorem Complex.HadamardThreeLines.interpStrip_eq_of_zero

added theorem Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip

added theorem Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip_eps

added theorem Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalStrip_zero

added theorem Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip'

added theorem Complex.HadamardThreeLines.norm_le_sSupNormIm

added theorem Complex.HadamardThreeLines.norm_lt_sSupNormIm_eps

added theorem Complex.HadamardThreeLines.norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip

added theorem Complex.HadamardThreeLines.sSupNormIm_eps_pos

added theorem Complex.HadamardThreeLines.sSupNormIm_nonneg

added def Complex.HadamardThreeLines.verticalClosedStrip

added def Complex.HadamardThreeLines.verticalStrip