OAI/Geometry/RuledCovering/Model.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RuledApproximation.Plane line 12

    Also declared: ComparatorChallenges/CylinderCovering.lean:231 (same declaration text), ComparatorChallenges/RuledCovering.lean:10 (same declaration text).

  2. abbrev OAI.RuledApproximation.Space line 13

    Also declared: ComparatorChallenges/CylinderCovering.lean:232 (same declaration text), ComparatorChallenges/RuledCovering.lean:11 (same declaration text).

  3. def OAI.RuledApproximation.vec2 line 15

    Also declared: ComparatorChallenges/CylinderCovering.lean:233 (same declaration text), ComparatorChallenges/RuledCovering.lean:13 (same declaration text).

  4. def OAI.RuledApproximation.vec3 line 16

    Also declared: ComparatorChallenges/CylinderCovering.lean:234 (same declaration text), ComparatorChallenges/RuledCovering.lean:14 (same declaration text).

  5. def OAI.RuledApproximation.axial line 17

    Also declared: ComparatorChallenges/CylinderCovering.lean:235 (same declaration text), ComparatorChallenges/RuledCovering.lean:15 (same declaration text).

  6. def OAI.RuledApproximation.IsParallelogram line 19

    Also declared: ComparatorChallenges/CylinderCovering.lean:237 (same declaration text), ComparatorChallenges/RuledCovering.lean:17 (same declaration text).

  7. def OAI.RuledApproximation.IsTriangle line 24

    Also declared: ComparatorChallenges/RuledCovering.lean:22 (same declaration text).

  8. structure OAI.RuledApproximation.Cylinder line 29

    Also declared: ComparatorChallenges/CylinderCovering.lean:241 (same declaration text), ComparatorChallenges/RuledCovering.lean:27 (same declaration text).

  9. def OAI.RuledApproximation.Cylinder.carrier line 36

    Also declared: ComparatorChallenges/CylinderCovering.lean:248 (same declaration text), ComparatorChallenges/RuledCovering.lean:34 (same declaration text).

  10. def OAI.RuledApproximation.Cylinder.area line 39

    Also declared: ComparatorChallenges/CylinderCovering.lean:251 (same declaration text), ComparatorChallenges/RuledCovering.lean:37 (same declaration text).

  11. def OAI.RuledApproximation.Cylinder.parallelogram line 41

    Also declared: ComparatorChallenges/CylinderCovering.lean:253 (same declaration text), ComparatorChallenges/RuledCovering.lean:39 (same declaration text).

  12. def OAI.RuledApproximation.Cylinder.triangle line 43

    Also declared: ComparatorChallenges/RuledCovering.lean:41 (same declaration text).

  13. def OAI.RuledApproximation.Cylinder.openBounded line 45

    Also declared: ComparatorChallenges/CylinderCovering.lean:255 (same declaration text), ComparatorChallenges/RuledCovering.lean:43 (same declaration text).

  14. def OAI.RuledApproximation.familySet line 49

    Also declared: ComparatorChallenges/CylinderCovering.lean:259 (same declaration text), ComparatorChallenges/RuledCovering.lean:47 (same declaration text).

  15. def OAI.RuledApproximation.familyArea line 50

    Also declared: ComparatorChallenges/CylinderCovering.lean:260 (same declaration text), ComparatorChallenges/RuledCovering.lean:48 (same declaration text).

  16. def OAI.RuledApproximation.HasFiniteCover line 52

    Also declared: ComparatorChallenges/CylinderCovering.lean:262 (same declaration text), ComparatorChallenges/RuledCovering.lean:50 (same declaration text).

  17. def OAI.RuledApproximation.SmoothNear line 57

    Source documentation

    No boundary hypothesis is included in this neighborhood regularity predicate.

    Also declared: ComparatorChallenges/CylinderCovering.lean:266 (same declaration text), ComparatorChallenges/RuledCovering.lean:55 (same declaration text).

    def SmoothNear (n : WithTop ℕ∞) (D : Set Plane) (v : Plane → Plane) : Prop :=
…

    Mentions: OAI.RuledApproximation.Plane

  18. def OAI.RuledApproximation.HyperbolicAt line 61

    Source documentation

    In dimension two these two distinct nonzero eigenvalues are all the eigenvalues.

    Also declared: ComparatorChallenges/CylinderCovering.lean:269 (same declaration text), ComparatorChallenges/RuledCovering.lean:59 (same declaration text).

    def HyperbolicAt (L : ℝ) (v : Plane → Plane) (p : Plane) : Prop :=
…

    Mentions: OAI.RuledApproximation.Plane

  19. def OAI.RuledApproximation.weight line 66

    Also declared: ComparatorChallenges/CylinderCovering.lean:274 (same declaration text), ComparatorChallenges/RuledCovering.lean:64 (same declaration text).

  20. def OAI.RuledApproximation.physicalWeight line 67

    Also declared: ComparatorChallenges/CylinderCovering.lean:275 (same declaration text), ComparatorChallenges/RuledCovering.lean:65 (same declaration text).

  21. def OAI.RuledApproximation.ruled line 70

    Also declared: ComparatorChallenges/CylinderCovering.lean:278 (same declaration text), ComparatorChallenges/RuledCovering.lean:68 (same declaration text).

  22. def OAI.RuledApproximation.physicalRuled line 74

    Also declared: ComparatorChallenges/CylinderCovering.lean:282 (same declaration text), ComparatorChallenges/RuledCovering.lean:72 (same declaration text).

  23. def OAI.RuledApproximation.HyperbolicStatement line 78

    Also declared: ComparatorChallenges/CylinderCovering.lean:286 (same declaration text), ComparatorChallenges/RuledCovering.lean:76 (same declaration text).

  24. def OAI.RuledApproximation.PhysicalHyperbolicStatement line 85

    Also declared: ComparatorChallenges/RuledCovering.lean:83 (same declaration text).

  25. def OAI.RuledApproximation.OpenRectangleC2 line 93

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

  26. def OAI.RuledApproximation.LogarithmicStatement line 98

    Also declared: ComparatorChallenges/RuledCovering.lean:96 (same declaration text).

  27. def OAI.RuledApproximation.ProductCellStatement line 109

    Also declared: ComparatorChallenges/RuledCovering.lean:107 (same declaration text).

  28. def OAI.RuledApproximation.OrthogonalGridStatement line 116

    Also declared: ComparatorChallenges/RuledCovering.lean:114 (same declaration text).

  29. def OAI.RuledApproximation.unitSquare line 126

    Also declared: ComparatorChallenges/CylinderCovering.lean:293 (same declaration text), ComparatorChallenges/RuledCovering.lean:124 (same declaration text).

  30. def OAI.RuledApproximation.IsSquareTile line 128

    Also declared: ComparatorChallenges/CylinderCovering.lean:295 (same declaration text), ComparatorChallenges/RuledCovering.lean:126 (same declaration text).

  31. def OAI.RuledApproximation.auxiliaryCylinder line 132

    Also declared: ComparatorChallenges/CylinderCovering.lean:299 (same declaration text), ComparatorChallenges/RuledCovering.lean:130 (same declaration text).

  32. def OAI.RuledApproximation.firstPhysicalMap line 135

    Also declared: ComparatorChallenges/CylinderCovering.lean:302 (same declaration text), ComparatorChallenges/RuledCovering.lean:133 (same declaration text).

  33. def OAI.RuledApproximation.secondPhysicalMap line 136

    Also declared: ComparatorChallenges/CylinderCovering.lean:303 (same declaration text), ComparatorChallenges/RuledCovering.lean:134 (same declaration text).

  34. def OAI.RuledApproximation.NilpotentStatement line 139

    Also declared: ComparatorChallenges/RuledCovering.lean:137 (same declaration text).

  35. def OAI.RuledApproximation.tetrahedron line 156

    Source documentation

    The regular edge-2 tetrahedron in physical coordinates.

    Also declared: ComparatorChallenges/RuledCovering.lean:154 (same declaration text).

    def tetrahedron : Set Space :=
…

    Mentions: OAI.RuledApproximation.Space

  36. def OAI.RuledApproximation.singularField line 160

    Also declared: ComparatorChallenges/RuledCovering.lean:158 (same declaration text).

  37. def OAI.RuledApproximation.ceilingPolynomial line 165

    Also declared: ComparatorChallenges/RuledCovering.lean:163 (same declaration text).

  38. def OAI.RuledApproximation.singularDomain line 168

    Also declared: ComparatorChallenges/RuledCovering.lean:166 (same declaration text).

  39. def OAI.RuledApproximation.singularLower line 172

    Also declared: ComparatorChallenges/RuledCovering.lean:170 (same declaration text).

  40. def OAI.RuledApproximation.singularUpper line 176

    Also declared: ComparatorChallenges/RuledCovering.lean:174 (same declaration text).

  41. def OAI.RuledApproximation.lowerTip line 181

    Also declared: ComparatorChallenges/RuledCovering.lean:179 (same declaration text).

  42. def OAI.RuledApproximation.upperTip line 184

    Also declared: ComparatorChallenges/RuledCovering.lean:182 (same declaration text).

  43. def OAI.RuledApproximation.singularCost line 187

    Also declared: ComparatorChallenges/RuledCovering.lean:185 (same declaration text).

  44. def OAI.RuledApproximation.singularCoefficient line 191

    Also declared: ComparatorChallenges/RuledCovering.lean:189 (same declaration text).

  45. def OAI.RuledApproximation.SingularStatement line 194

    Also declared: ComparatorChallenges/RuledCovering.lean:192 (same declaration text).

  46. def OAI.RuledApproximation.FullMain line 213

    Also declared: ComparatorChallenges/RuledCovering.lean:211 (same declaration text).