OAI/Combinatorics/PlanarL1/Parameters.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarL1.Parameters.R line 12

    Source documentation

    Universal ordered parameter choices. The two free widths are chosen strictly smaller than every displayed upper bound, not adapted to a graph.

    def R : ℝ := 1/10^8
  2. def OAI.PlanarL1.Parameters.D line 13
  3. def OAI.PlanarL1.Parameters.g line 14
  4. def OAI.PlanarL1.Parameters.j line 15
  5. def OAI.PlanarL1.Parameters.epsilon line 16
  6. def OAI.PlanarL1.Parameters.EA line 17
  7. def OAI.PlanarL1.Parameters.EB line 18
  8. def OAI.PlanarL1.Parameters.zetaA line 19
  9. def OAI.PlanarL1.Parameters.zetaB line 20
  10. def OAI.PlanarL1.Parameters.a₁ line 21
  11. def OAI.PlanarL1.Parameters.a₂ line 22
  12. def OAI.PlanarL1.Parameters.kappaA line 23
  13. def OAI.PlanarL1.Parameters.kappaB line 24
  14. def OAI.PlanarL1.Parameters.lambda line 25
  15. lemma OAI.PlanarL1.Parameters.positive line 27
  16. lemma OAI.PlanarL1.Parameters.interpolationA line 31
  17. lemma OAI.PlanarL1.Parameters.interpolationB line 34
  18. lemma OAI.PlanarL1.Parameters.thinA line 37
  19. lemma OAI.PlanarL1.Parameters.widthA line 38
  20. lemma OAI.PlanarL1.Parameters.widthB line 39
  21. lemma OAI.PlanarL1.Parameters.verticalA line 41
  22. lemma OAI.PlanarL1.Parameters.verticalB line 44
  23. structure OAI.PlanarL1.Parameters.Interpolation line 49

    Source documentation

    Numeric input to the literal interpolation hierarchy.

    structure Interpolation where
…
  24. def OAI.PlanarL1.Parameters.broad line 59
  25. def OAI.PlanarL1.Parameters.narrow line 62