OAI/Analysis/Triangular/Energy/Potentials.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularUniversal.universal_from_power_bounds line 13

   Source documentation

   The shift/Fatou/Tonelli assembly applies to the exact extended ordered-pair energy. It does not presume finite lattice energy or spacing of a competitor.

   lemma universal_from_power_bounds (C : Set Plane)
       (hpower : ∀ v : I, latticeEnergy (powerPotential v) ≤ energy (powerPotential v) C)
       {g : ℝ → ℝ} (hg : AdmissiblePotential g) : latticeEnergy g ≤ energy g C := by
   …

   Mentions: OAI.TriangularUniversal.Plane, OAI.TriangularUniversal.latticeEnergy, OAI.TriangularUniversal.powerPotential, OAI.TriangularUniversal.energy, OAI.TriangularUniversal.AdmissiblePotential

2. lemma OAI.TriangularUniversal.diskEnergy_one line 31
3. lemma OAI.TriangularUniversal.count_sub_one_tendsto line 45
4. lemma OAI.TriangularUniversal.energy_one line 60
5. def OAI.TriangularUniversal.gaussPot line 74
6. lemma OAI.TriangularUniversal.power_bounds_from_gaussians line 76
7. lemma OAI.TriangularUniversal.universal_from_gaussian_bounds line 107