OAI/Geometry/IntegralFillings/Model.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpIntegralFillings.Euc line 14

   Also declared: ComparatorChallenges/FillingCoefficient.lean:14 (same declaration text).

2. abbrev OAI.SharpIntegralFillings.Functional line 15

   Also declared: ComparatorChallenges/FillingCoefficient.lean:15 (same declaration text).

3. def OAI.SharpIntegralFillings.BoundedLip line 21

   Also declared: ComparatorChallenges/FillingCoefficient.lean:21 (same declaration text).

4. def OAI.SharpIntegralFillings.Admissible line 24

   Also declared: ComparatorChallenges/FillingCoefficient.lean:24 (same declaration text).

5. def OAI.SharpIntegralFillings.Controls line 27

   Also declared: ComparatorChallenges/FillingCoefficient.lean:27 (same declaration text).

6. def OAI.SharpIntegralFillings.mass line 32

   Also declared: ComparatorChallenges/FillingCoefficient.lean:32 (same declaration text).

7. structure OAI.SharpIntegralFillings.IsMetricCurrent line 36

   Also declared: ComparatorChallenges/FillingCoefficient.lean:36 (same declaration text).

8. def OAI.SharpIntegralFillings.boundarySucc line 54

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

9. def OAI.SharpIntegralFillings.boundary line 57

   Also declared: ComparatorChallenges/FillingCoefficient.lean:57 (same declaration text).

10. structure OAI.SharpIntegralFillings.IntegerChart line 61

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

11. def OAI.SharpIntegralFillings.IntegerChart.scalar line 74

    Also declared: ComparatorChallenges/FillingCoefficient.lean:74 (same declaration text).

12. def OAI.SharpIntegralFillings.IntegerChart.jacobian line 77

    Also declared: ComparatorChallenges/FillingCoefficient.lean:77 (same declaration text).

13. def OAI.SharpIntegralFillings.IntegerChart.action line 81

    Also declared: ComparatorChallenges/FillingCoefficient.lean:81 (same declaration text).

14. def OAI.SharpIntegralFillings.IntegerChart.image line 86

    Also declared: ComparatorChallenges/FillingCoefficient.lean:86 (same declaration text).

15. def OAI.SharpIntegralFillings.IntegerRectifiable line 90

    Also declared: ComparatorChallenges/FillingCoefficient.lean:90 (same declaration text).

16. def OAI.SharpIntegralFillings.IsIntegral line 97

    Also declared: ComparatorChallenges/FillingCoefficient.lean:97 (same declaration text).

17. abbrev OAI.SharpIntegralFillings.IntegralCurrent line 102

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

18. def OAI.SharpIntegralFillings.CompactlySupported line 105

    Also declared: ComparatorChallenges/FillingCoefficient.lean:105 (same declaration text).

19. def OAI.SharpIntegralFillings.IsCycle line 109

    Also declared: ComparatorChallenges/FillingCoefficient.lean:109 (same declaration text).

20. def OAI.SharpIntegralFillings.omega line 113

    Also declared: ComparatorChallenges/FillingCoefficient.lean:113 (same declaration text).

21. def OAI.SharpIntegralFillings.sphereArea line 115

    Also declared: ComparatorChallenges/FillingCoefficient.lean:115 (same declaration text).

22. def OAI.SharpIntegralFillings.fillingCoefficient line 116

    Also declared: ComparatorChallenges/FillingCoefficient.lean:116 (same declaration text).

23. def OAI.SharpIntegralFillings.fillingPower line 118

    Also declared: ComparatorChallenges/FillingCoefficient.lean:118 (same declaration text).