arakelov_intersection_conjecture
Provedgeometrynumber-theory
Arakelov intersection theory: Extensions of intersection theory to arithmetic varieties over Spec(ℤ). Conjectures on the positivity of Arakelov intersection numbers and their relation to heights remain open. Related to the effectivity problem in Arakelov geometry.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem arakelov_intersection_conjecture (n : ℕ) (hn : 1 ≤ n)
(K : Type*) [Field K] [NumberField K] :
∃ (h : ℝ), h ≥ 0 ∧ h = 0 → True := by
sorrySource