OAI/Analysis/Conductivity/Model.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ScalarConductivity.R3 line 11

   Also declared: ComparatorChallenges/Conductivity.lean:11 (same declaration text).

2. abbrev OAI.ScalarConductivity.JetFiber line 12

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

3. def OAI.ScalarConductivity.ball line 13

   Also declared: ComparatorChallenges/Conductivity.lean:13 (same declaration text).

4. def OAI.ScalarConductivity.ballMeasure line 14

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

5. abbrev OAI.ScalarConductivity.JetSpace line 15

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

6. def OAI.ScalarConductivity.smoothJet line 17

   Also declared: ComparatorChallenges/Conductivity.lean:17 (same declaration text).

7. def OAI.ScalarConductivity.smoothJets line 20

   Also declared: ComparatorChallenges/Conductivity.lean:20 (same declaration text).

8. def OAI.ScalarConductivity.compactSmoothJets line 24

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

9. def OAI.ScalarConductivity.H1Space line 29

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

10. abbrev OAI.ScalarConductivity.H1 line 31

    Also declared: ComparatorChallenges/Conductivity.lean:31 (same declaration text).

11. def OAI.ScalarConductivity.zeroTraceAmbient line 33

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

12. def OAI.ScalarConductivity.H10 line 36

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

13. instance OAI.ScalarConductivity.H10_isClosed line 38

    Also declared: ComparatorChallenges/Conductivity.lean:38 (same declaration text).

14. abbrev OAI.ScalarConductivity.TraceSpace line 42

    Also declared: ComparatorChallenges/Conductivity.lean:42 (same declaration text).

15. abbrev OAI.ScalarConductivity.TraceDual line 43

    Also declared: ComparatorChallenges/Conductivity.lean:43 (same declaration text).

16. abbrev OAI.ScalarConductivity.DNOperator line 44

    Also declared: ComparatorChallenges/Conductivity.lean:44 (same declaration text).

17. def OAI.ScalarConductivity.trace line 46

    Also declared: ComparatorChallenges/Conductivity.lean:46 (same declaration text).

18. def OAI.ScalarConductivity.weakGradient line 48

    Also declared: ComparatorChallenges/Conductivity.lean:48 (same declaration text).

19. def OAI.ScalarConductivity.energy line 51

    Also declared: ComparatorChallenges/Conductivity.lean:51 (same declaration text).

20. def OAI.ScalarConductivity.Harmonic line 54

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

21. def OAI.ScalarConductivity.IsDirichletToNeumann line 57

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

22. def OAI.ScalarConductivity.EqualOneNearBoundary line 63

    Also declared: ComparatorChallenges/Conductivity.lean:63 (same declaration text).

23. def OAI.ScalarConductivity.MainStatement line 66

    Also declared: ComparatorChallenges/Conductivity.lean:66 (same declaration text).