Formal target: Corpus.WikipediaBloch.blochConstant_exact_value

Ahlfors and Grunsky also conjectured in [AG37] that this upper bound is the precise value of the Bloch constant.

Exact formal statement

Eq.{1} Corpus.WikipediaBloch.blochConstant
  (HDiv.hDiv.{0, 0, 0} (HMul.hMul.{0, 0, 0} (Real.Gamma (1 / 3)) (Real.Gamma (11 / 12)))
    (HMul.hMul.{0, 0, 0} (Real.Gamma (1 / 4)) (HAdd.hAdd.{0, 0, 0} 1 (Real.sqrt 3)).sqrt))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record