Skip to content

Commit 0477177

Browse files
committed
feat: Hadamard three-lines theorem (#7919)
This PR introduces a version of the Hadamard three-lines theorem (see [here](https://en.wikipedia.org/wiki/Hadamard_three-lines_theorem)), 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!
1 parent 859845f commit 0477177

File tree

2 files changed

+420
-0
lines changed

2 files changed

+420
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -841,6 +841,7 @@ import Mathlib.Analysis.Complex.CauchyIntegral
841841
import Mathlib.Analysis.Complex.Circle
842842
import Mathlib.Analysis.Complex.Conformal
843843
import Mathlib.Analysis.Complex.Convex
844+
import Mathlib.Analysis.Complex.Hadamard
844845
import Mathlib.Analysis.Complex.HalfPlane
845846
import Mathlib.Analysis.Complex.Isometry
846847
import Mathlib.Analysis.Complex.Liouville

0 commit comments

Comments
 (0)