Theorems · Theorem · complex analysis

Complex.HadamardThreeLines.eventuallyle

∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) [inst_1 : NormedSpace ℂ E] (z : ℂ),
  BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
    DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1) →
      z ∈ Complex.HadamardThreeLines.verticalStrip 0 1 →
        (fun x => ‖f z‖) ≤ᶠ[nhdsWithin 0 (Set.Ioi 0)] fun ε =>
          ‖(↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 0)) ^ (1 - z) *
              (↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 1)) ^ z‖

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites23

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

Setstatement · cited by 53,352
Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
NormedSpacestatement and proof · cited by 12,499
Set.imagestatement and proof · cited by 5,609
Complexstatement and proof · cited by 5,565
Norm.normstatement and proof · cited by 5,413
nhdsWithinstatement · cited by 1,912
Filter.univ_mem'proof · cited by 1,672
Complex.ofRealstatement · cited by 1,654
Filter.mp_memproof · cited by 1,537
Set.Ioistatement and proof · cited by 1,463

Cited by1

Results whose statement or proof uses this declaration.

Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalStrip_zeroproof · cited by 1