OAI/Geometry/TriangularCovering/Basic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TriangularCovering.Space line 11

   Also declared: ComparatorChallenges/CylinderCovering.lean:12 (same declaration text), ComparatorChallenges/TriangularCovering.lean:11 (same declaration text).

2. def OAI.TriangularCovering.H line 13

   Also declared: ComparatorChallenges/CylinderCovering.lean:14 (same declaration text), ComparatorChallenges/TriangularCovering.lean:13 (same declaration text).

3. def OAI.TriangularCovering.point line 15

   Also declared: ComparatorChallenges/CylinderCovering.lean:16 (same declaration text), ComparatorChallenges/TriangularCovering.lean:15 (same declaration text).

4. def OAI.TriangularCovering.K line 18

   Source documentation

   The closed tetrahedron in physical Euclidean coordinates.

   Also declared: ComparatorChallenges/CylinderCovering.lean:18 (same declaration text), ComparatorChallenges/TriangularCovering.lean:17 (same declaration text).

   def K : Set Space :=
   …

   Mentions: OAI.TriangularCovering.Space

5. def OAI.TriangularCovering.projection line 22

   Source documentation

   Orthogonal projection onto the plane normal to a unit vector.

   Also declared: ComparatorChallenges/CylinderCovering.lean:21 (same declaration text), ComparatorChallenges/TriangularCovering.lean:20 (same declaration text).

   def projection (u z : Space) : Space := z - (inner ℝ u z) • u

   Mentions: OAI.TriangularCovering.Space

6. def OAI.TriangularCovering.area line 25

   Source documentation

   Euclidean planar Lebesgue area, extended to ambient subsets.

   Also declared: ComparatorChallenges/CylinderCovering.lean:23 (same declaration text), ComparatorChallenges/TriangularCovering.lean:22 (same declaration text).

   def area (B : Set Space) : ℝ := (Measure.euclideanHausdorffMeasure 2 B).toReal

   Mentions: OAI.TriangularCovering.Space

7. def OAI.TriangularCovering.shadowArea line 27

   Also declared: ComparatorChallenges/CylinderCovering.lean:25 (same declaration text), ComparatorChallenges/TriangularCovering.lean:24 (same declaration text).

8. def OAI.TriangularCovering.A_min line 29

   Also declared: ComparatorChallenges/CylinderCovering.lean:27 (same declaration text), ComparatorChallenges/TriangularCovering.lean:26 (same declaration text).

9. structure OAI.TriangularCovering.TriCylinder line 32

   Source documentation

   A nondegenerate, closed triangular base in the perpendicular linear plane.

   Also declared: ComparatorChallenges/CylinderCovering.lean:29 (same declaration text), ComparatorChallenges/TriangularCovering.lean:28 (same declaration text).

   structure TriCylinder where
   …

10. def OAI.TriangularCovering.TriCylinder.carrier line 45

    Source documentation

    The entire cylinder, with all boundary points included.

    Also declared: ComparatorChallenges/CylinderCovering.lean:41 (same declaration text), ComparatorChallenges/TriangularCovering.lean:40 (same declaration text).

    def TriCylinder.carrier (c : TriCylinder) : Set Space :=
    …

    Mentions: OAI.TriangularCovering.TriCylinder, OAI.TriangularCovering.Space

11. def OAI.TriangularCovering.Covers line 48

    Also declared: ComparatorChallenges/CylinderCovering.lean:44 (same declaration text), ComparatorChallenges/TriangularCovering.lean:43 (same declaration text).

12. def OAI.TriangularCovering.totalArea line 51

    Also declared: ComparatorChallenges/CylinderCovering.lean:47 (same declaration text), ComparatorChallenges/TriangularCovering.lean:46 (same declaration text).

13. def OAI.TriangularCovering.relativeCost line 54

    Also declared: ComparatorChallenges/CylinderCovering.lean:50 (same declaration text), ComparatorChallenges/TriangularCovering.lean:49 (same declaration text).

14. def OAI.TriangularCovering.n line 57

    Also declared: ComparatorChallenges/CylinderCovering.lean:53 (same declaration text), ComparatorChallenges/TriangularCovering.lean:52 (same declaration text).

15. def OAI.TriangularCovering.MainAsymptotic line 60

    Source documentation

    Uniform O(ε⁴), with exactly twice the ceiling of 2/ε² cylinders.

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

    def MainAsymptotic : Prop :=
    …

16. def OAI.TriangularCovering.NormalizedCounterexample line 69

    Source documentation

    A strict directionwise half-area bound for the same regular tetrahedron.

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

    def NormalizedCounterexample : Prop :=
    …