Theorems · Theorem · complex analysis

Complex.HadamardThreeLines.interpStrip_eq_of_pos

∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (z : ℂ),
  0 < Complex.HadamardThreeLines.sSupNormIm f 0 →
    0 < Complex.HadamardThreeLines.sSupNormIm f 1 →
      Complex.HadamardThreeLines.interpStrip f z =
        ↑(Complex.HadamardThreeLines.sSupNormIm f 0) ^ (1 - z) * ↑(Complex.HadamardThreeLines.sSupNormIm f 1) ^ z

Rewrite for InterpStrip when 0 < sSupNormIm f 0 and 0 < sSupNormIm f 1.

Defined in: Mathlib.Analysis.Complex.Hadamard
Cited by: 3 results in Mathlib
Foundations: Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
Complexstatement and proof · cited by 5,565
Complex.ofRealstatement and proof · cited by 1,654
ne_of_gtproof · cited by 637
Complex.HadamardThreeLines.sSupNormImstatement and proof · cited by 19
Complex.HadamardThreeLines.interpStripstatement · cited by 9

Cited by3

Results whose statement or proof uses this declaration.

Complex.HadamardThreeLines.diffContOnCl_interpStripproof · cited by 1
Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip₀₁'proof · cited by 1
Complex.HadamardThreeLines.interpStrip_eq_of_mem_verticalStripproof · cited by 1