Theorems · Definition · complex analysis

Complex.HadamardThreeLines.invInterpStrip

{E : Type u_1} → [NormedAddCommGroup E] → (ℂ → E) → ℂ → ℝ → ℂ

The inverse of the interpolation of sSupNormIm on the two boundaries. In other words, this is the inverse of the right side of the target inequality: |f(z)| ≤ |M(0) ^ (1-z)| * |M(1) ^ z|. Shifting this by a positive epsilon allows us to prove the case when either of the boundaries is zero.

Defined in

Mathlib.Analysis.Complex.Hadamard

Cited by

5 results in Mathlib

Foundations

Depth 191 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroup