OAI/Analysis/Triangular/Energy/Definitions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.AtomicTriangular.LocallyFinite line 11

   Also declared: ComparatorChallenges/TriangularEnergy.lean:53 (same declaration text).

2. abbrev OAI.AtomicTriangular.diskPoints line 12

   Also declared: ComparatorChallenges/TriangularEnergy.lean:54 (same declaration text).

3. abbrev OAI.AtomicTriangular.diskCount line 13

   Also declared: ComparatorChallenges/TriangularEnergy.lean:55 (same declaration text).

4. abbrev OAI.AtomicTriangular.DensityOne line 14

   Also declared: ComparatorChallenges/TriangularEnergy.lean:56 (same declaration text).

5. abbrev OAI.AtomicTriangular.AdmissiblePotential line 15

   Also declared: ComparatorChallenges/TriangularEnergy.lean:57 (same declaration text).

6. abbrev OAI.AtomicTriangular.diskEnergy line 16

   Also declared: ComparatorChallenges/TriangularEnergy.lean:58 (same declaration text).

7. abbrev OAI.AtomicTriangular.energy line 17

   Also declared: ComparatorChallenges/TriangularEnergy.lean:59 (same declaration text).

8. def OAI.AtomicTriangular.latticeEnergy line 20

   Source documentation

   The full nonzero-lattice energy, allowing a divergent series.

   Also declared: ComparatorChallenges/TriangularEnergy.lean:62 (same declaration text).

   def latticeEnergy (g : ℝ → ℝ) : ℝ≥0∞ :=
   …