OAI/Analysis/Triangular/Energy/Universal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AtomicTriangular.universal_energy_minimum line 9

   Source documentation

   The triangular lattice minimizes every nonnegative completely monotone energy.

   Distinct definitions of this name: ComparatorChallenges/TriangularEnergy.lean:66 (different declaration text). Qualify references as OAI.AtomicTriangular.universal_energy_minimum@path.

   theorem universal_energy_minimum (g : ℝ → ℝ) (C : Set Plane)
       (hg : AdmissiblePotential g) (_hC : LocallyFinite C) (hd : DensityOne C) :
       latticeEnergy g ≤ energy g C ∧ latticeEnergy g = energy g A := by
   …

   Mentions: OAI.AtomicTriangular.Plane, OAI.AtomicTriangular.AdmissiblePotential, OAI.AtomicTriangular.LocallyFinite, OAI.AtomicTriangular.DensityOne, OAI.AtomicTriangular.latticeEnergy, OAI.AtomicTriangular.energy, OAI.AtomicTriangular.A