OAI/Geometry/CoveringDensity/Model.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CoveringOrder.Space line 9

   Also declared: ComparatorChallenges/CoveringDensity.lean:9 (same declaration text).

2. structure OAI.CoveringOrder.LatticeCover line 12

   Source documentation

   Actual discrete full-rank lattice coverings; no assumed density theorem.

   Also declared: ComparatorChallenges/CoveringDensity.lean:12 (same declaration text).

   structure LatticeCover {n : ℕ} (K : Set (Space n)) where
   …

   Mentions: OAI.CoveringOrder.Space

3. def OAI.CoveringOrder.euclideanVolume line 18

   Also declared: ComparatorChallenges/CoveringDensity.lean:18 (same declaration text).

4. def OAI.CoveringOrder.euclideanCovolume line 29

   Also declared: ComparatorChallenges/CoveringDensity.lean:29 (same declaration text).

5. def OAI.CoveringOrder.latticeDensity line 33

   Also declared: ComparatorChallenges/CoveringDensity.lean:33 (same declaration text).

6. def OAI.CoveringOrder.thetaL line 37

   Also declared: ComparatorChallenges/CoveringDensity.lean:37 (same declaration text).

7. abbrev OAI.TranslativeCovering.Space line 47

   Also declared: ComparatorChallenges/CoveringDensity.lean:47 (same declaration text).

8. def OAI.TranslativeCovering.cube line 49

   Also declared: ComparatorChallenges/CoveringDensity.lean:49 (same declaration text).

9. def OAI.TranslativeCovering.LocallyFiniteCenters line 52

   Also declared: ComparatorChallenges/CoveringDensity.lean:52 (same declaration text).

10. def OAI.TranslativeCovering.Covers line 55

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

11. def OAI.TranslativeCovering.ConvexBody line 58

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

12. def OAI.TranslativeCovering.CentrallySymmetric line 61

    Also declared: ComparatorChallenges/CoveringDensity.lean:61 (same declaration text).

13. def OAI.TranslativeCovering.upperCenterIntensity line 64

    Also declared: ComparatorChallenges/CoveringDensity.lean:64 (same declaration text).

14. def OAI.TranslativeCovering.thetaT line 68

    Also declared: ComparatorChallenges/CoveringDensity.lean:68 (same declaration text).

15. abbrev OAI.CoveringOrder.Body line 78

    Also declared: ComparatorChallenges/CoveringDensity.lean:78 (same declaration text).

16. abbrev OAI.CoveringOrder.SymmetricBody line 79

    Also declared: ComparatorChallenges/CoveringDensity.lean:79 (same declaration text).

17. def OAI.CoveringOrder.translativeSup line 82

    Also declared: ComparatorChallenges/CoveringDensity.lean:82 (same declaration text).

18. def OAI.CoveringOrder.symmetricTranslativeSup line 85

    Also declared: ComparatorChallenges/CoveringDensity.lean:85 (same declaration text).

19. def OAI.CoveringOrder.latticeSup line 88

    Also declared: ComparatorChallenges/CoveringDensity.lean:88 (same declaration text).

20. def OAI.CoveringOrder.symmetricLatticeSup line 91

    Also declared: ComparatorChallenges/CoveringDensity.lean:91 (same declaration text).

21. def OAI.CoveringOrder.orderBounds line 95

    Source documentation

    The finite real comparison scale, viewed in extended nonnegative reals.

    Also declared: ComparatorChallenges/CoveringDensity.lean:95 (same declaration text).

    def orderBounds (c C : ℝ) (n : ℕ) (a : ℝ≥0∞) : Prop :=
    …

22. def OAI.CoveringOrder.OptimalOrder line 102

    Source documentation

    All four extremal quantities have common absolute positive comparison constants. ENNReal bounds imply finiteness rather than mapping a potentially infinite density to zero through toReal.

    Also declared: ComparatorChallenges/CoveringDensity.lean:102 (same declaration text).

    def OptimalOrder : Prop :=
    …

23. def OAI.TranslativeCovering.MainStatement line 115