Main.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.CoveringOrder.euclideanVolume_eq_volume line 10
theorem OAI.CoveringOrder.euclideanCovolume_eq_ofReal line 13
theorem OAI.CoveringOrder.latticeDensity_eq_volume_div_covolume line 22
theorem OAI.CoveringOrder.thetaL_eq_iInf_latticeCover line 30
Source documentation
The infimum of actual lattice densities agrees with indexing by bundled covers.
```
theorem thetaL_eq_iInf_latticeCover {n : ℕ} (K : Set (Space n)) :
    thetaL K = ⨅ P : LatticeCover K,
      volume K / ENNReal.ofReal (ZLattice.covolume P.lattice volume) := by
…
```
Mentions: OAI.CoveringOrder.Space, OAI.CoveringOrder.thetaL, OAI.CoveringOrder.LatticeCover
def OAI.CoveringOrder.LatticeCover.toPeriodic line 37
Source documentation
A single lattice is a one-coset periodic covering.
```
def LatticeCover.toPeriodic {n : ℕ} {K : Set (Space n)} (P : LatticeCover K) :
    TranslativeCovering.PeriodicCover K where
…
```
Mentions: OAI.CoveringOrder.Space, OAI.CoveringOrder.LatticeCover, OAI.TranslativeCovering.PeriodicCover
theorem OAI.CoveringOrder.thetaT_le_thetaL line 50
Source documentation
Full periodization, followed by restriction to one-coset coverings.
```
theorem thetaT_le_thetaL {n : ℕ} {K : Set (Space n)}
    (hK : TranslativeCovering.ConvexBody K) :
    TranslativeCovering.thetaT K ≤ thetaL K := by
…
```
Mentions: OAI.CoveringOrder.Space, OAI.TranslativeCovering.ConvexBody, OAI.TranslativeCovering.thetaT, OAI.CoveringOrder.thetaL
theorem OAI.CoveringOrder.uniform_lattice_density_upper line 65
Source documentation
The transported upper theorem bounds the actual lattice-density infimum.
```
theorem uniform_lattice_density_upper :
    ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 2 ≤ n → ∀ K : Set (Space n),
      TranslativeCovering.ConvexBody K →
      thetaL K ≤ ENNReal.ofReal (C * (n : ℝ) * Real.log (n : ℝ)) := by
…
```
Mentions: OAI.CoveringOrder.Space, OAI.TranslativeCovering.ConvexBody, OAI.CoveringOrder.thetaL
theorem OAI.CoveringOrder.optimal_order line 79
Source documentation
All four density suprema have order n * log n with common absolute constants.
Distinct definitions of this name: ComparatorChallenges/CoveringDensity.lean:113 (different declaration text). Qualify references as OAI.CoveringOrder.optimal_order@path.
```
theorem optimal_order : OptimalOrder := by
…
```
Mentions: OAI.CoveringOrder.OptimalOrder