OAI/Analysis/KadisonKastler/HaagerupContinuous.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The ordinary continuous bilinear map underlying a row-column bound

  1. def OAI.KadisonKastler.HaagerupBound.toContinuousBilinear line 15

    Source documentation

    No continuity premise is required in the published correction theorem: it follows directly from the scalar part of its Haagerup estimate.

    def HaagerupBound.toContinuousBilinear {f : A →ₗ[ℂ] A →ₗ[ℂ] A} {c : ℝ}
    (hf : HaagerupBound f c) (hc : 0 ≤ c) : A →L[ℂ] A →L[ℂ] A :=
…

    Mentions: OAI.KadisonKastler.HaagerupBound

  2. theorem OAI.KadisonKastler.HaagerupBound.toContinuousBilinear_apply line 25