A quartic Hilbert space modulus for a bounded bilinear form

Proved

OAI.HochschildDomination.exists_quartic_hilbert_modulus

by wurtle · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

bounded-hochschild-cohomologyoai-math

Let $M$ be a unital C*-algebra, with no order assumed, and let $B:M\to M^*$ be a bounded linear map. Then there are a complex Hilbert space $H$ , a bounded linear map $\beta:M\to H$ and a constant $C\ge0$ with

\|B(\,\cdot\,)(b)\|^4\le C\|b\|^2\|\beta(b)\|^2\qquad\text{for all }b\in M,

where $B(\,\cdot\,)(b)=$ B.flip b is the functional $a\mapsto B(a)(b)$ .

Formalization Note The statement is verbatim from OpenAI's Lean development, with the listed Definitions imported in place of the upstream modules; the definitions are supporting code for this statement. Only the keyword lemma, where used upstream, becomes theorem, and a leading include ... in or omit ... in moves to the preamble. It is a step of the Lean proof of the vanishing of higher bounded Hochschild cohomology.

Preamble

import Mathlib
import Definitions.Def_KadisonRingroseSupport2

namespace OAI

noncomputable section
open Filter Topology MeasureTheory
open scoped BigOperators ComplexOrder InnerProductSpace ComplexStarModule CStarAlgebra

open scoped InnerProductSpace ComplexOrder

namespace HochschildDomination
universe u v
variable {M : Type u} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M]

namespace PreHilbert
variable (φ ψ : M →ₚ[ℂ] ℂ)

end PreHilbert

variable (B : M →L[ℂ] StrongDual ℂ M) (φ ψ : M →ₚ[ℂ] ℂ)
  (C : ℝ) (hC : 0 ≤ C)
  (hdom : ∀ a b, ‖B a b‖ ≤ C * ‖a‖ * ‖PreHilbert.of φ ψ b‖)

end HochschildDomination

open scoped InnerProductSpace ComplexOrder
namespace HochschildDomination
universe u
variable {M : Type u} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M]
omit [PartialOrder M] [StarOrderedRing M]

Formal statement

theorem exists_quartic_hilbert_modulus (B : M →L[ℂ] StrongDual ℂ M) :
    ∃ (H : Type u) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
      (_ : CompleteSpace H) (β : M →L[ℂ] H) (C : ℝ),
      0 ≤ C ∧ ∀ b, ‖B.flip b‖^4 ≤ C * ‖b‖^2 * ‖β b‖^2 := by
  sorry

end HochschildDomination
end
end OAI

Source

OpenAI, Vanishing of higher bounded Hochschild cohomology, September 23, 2026, https://github.com/openai/math (paper: preprints/Vanishing-of-higher-bounded-Hochschild-cohomology-September-23-2026/paper.pdf; Apache License 2.0); Lean declaration `OAI.HochschildDomination.exists_quartic_hilbert_modulus`, https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Analysis/TracialCohomology/DominatedFactorization.lean#L136

View graph