OAI/Analysis/PlanarPacking/Indices.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Finite node coordinates

These coordinates enumerate the value and derivative data on the first triangular shell nodes in the planar Fourier interpolation problem.

  1. def OAI.SharpPlanar.Numerical.node1 line 14
  2. def OAI.SharpPlanar.Numerical.node3 line 15
  3. def OAI.SharpPlanar.Numerical.node4 line 16
  4. def OAI.SharpPlanar.Numerical.jNode line 17
  5. def OAI.SharpPlanar.Numerical.jDeriv line 18
  6. def OAI.SharpPlanar.Numerical.node7 line 19
  7. def OAI.SharpPlanar.Numerical.node9 line 20
  8. def OAI.SharpPlanar.Numerical.node12 line 21
  9. def OAI.SharpPlanar.Numerical.node13 line 22
  10. def OAI.SharpPlanar.Numerical.node15 line 23
  11. def OAI.SharpPlanar.Numerical.node16 line 24
  12. def OAI.SharpPlanar.Numerical.lNode line 25
  13. def OAI.SharpPlanar.Numerical.lDeriv line 26
  14. def OAI.SharpPlanar.Numerical.eNode line 28
  15. def OAI.SharpPlanar.Numerical.centralIndex line 29
  16. def OAI.SharpPlanar.Numerical.exteriorIndex line 30
  17. abbrev OAI.SharpPlanar.Numerical.FiniteIndex line 31
  18. def OAI.SharpPlanar.Numerical.finiteIndex line 32
  19. def OAI.SharpPlanar.Numerical.lowExteriorIndex line 33
  20. lemma OAI.SharpPlanar.Numerical.centralIndex_injective line 34
  21. lemma OAI.SharpPlanar.Numerical.exteriorIndex_injective line 35
  22. lemma OAI.SharpPlanar.Numerical.finiteIndex_injective line 36
  23. lemma OAI.SharpPlanar.Numerical.lowExteriorIndex_injective line 37
  24. lemma OAI.SharpPlanar.Numerical.centralIndex_bound line 38
  25. lemma OAI.SharpPlanar.Numerical.exteriorIndex_bound line 39
  26. lemma OAI.SharpPlanar.Numerical.finiteIndex_bound line 40
  27. lemma OAI.SharpPlanar.Numerical.lowExteriorIndex_bound line 41
  28. lemma OAI.SharpPlanar.Numerical.finiteIndex_cover_check line 42
  29. lemma OAI.SharpPlanar.Numerical.finiteIndex_range line 44
  30. lemma OAI.SharpPlanar.Numerical.exteriorIndex_cover_check line 52
  31. lemma OAI.SharpPlanar.Numerical.exteriorIndex_range line 54
  32. lemma OAI.SharpPlanar.Numerical.lowExteriorIndex_cover_check line 62
  33. lemma OAI.SharpPlanar.Numerical.lowExteriorIndex_range line 64