OAI/Dynamics/EntropyCounterexample/SpherePolynomialPerturbation.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.SpherePolynomialPerturbation.Ambient line 8
  2. abbrev OAI.Problem340.SpherePolynomialPerturbation.Sphere line 9
  3. def OAI.Problem340.SpherePolynomialPerturbation.numeratorRe line 11
  4. def OAI.Problem340.SpherePolynomialPerturbation.numeratorIm line 14
  5. def OAI.Problem340.SpherePolynomialPerturbation.squaredNumeratorReduced line 17
  6. def OAI.Problem340.SpherePolynomialPerturbation.denominator line 22
  7. def OAI.Problem340.SpherePolynomialPerturbation.ambientMap line 25
  8. lemma OAI.Problem340.SpherePolynomialPerturbation.numerator_identity line 30
  9. lemma OAI.Problem340.SpherePolynomialPerturbation.denominator_pos line 43
  10. lemma OAI.Problem340.SpherePolynomialPerturbation.ambientMap_mem_sphere line 56
  11. def OAI.Problem340.SpherePolynomialPerturbation.sphereMap line 75
  12. def OAI.Problem340.SpherePolynomialPerturbation.complexCoordinate line 78
  13. def OAI.Problem340.SpherePolynomialPerturbation.stereoCoordinate line 80
  14. lemma OAI.Problem340.SpherePolynomialPerturbation.numerator_complex line 83
  15. lemma OAI.Problem340.SpherePolynomialPerturbation.complexCoordinate_ambientMap line 90
  16. lemma OAI.Problem340.SpherePolynomialPerturbation.one_sub_height line 99
  17. theorem OAI.Problem340.SpherePolynomialPerturbation.stereoCoordinate_ambientMap line 106
  18. lemma OAI.Problem340.SpherePolynomialPerturbation.ambientMap_zero line 117
  19. lemma OAI.Problem340.SpherePolynomialPerturbation.sphereMap_zero line 127
  20. lemma OAI.Problem340.SpherePolynomialPerturbation.sphereMap_fixes_north line 131
  21. lemma OAI.Problem340.SpherePolynomialPerturbation.sphereMap_avoids_north line 142
  22. def OAI.Problem340.SpherePolynomialPerturbation.domain line 153
  23. lemma OAI.Problem340.SpherePolynomialPerturbation.contDiff_numeratorRe line 155
  24. lemma OAI.Problem340.SpherePolynomialPerturbation.contDiff_numeratorIm line 162
  25. lemma OAI.Problem340.SpherePolynomialPerturbation.contDiff_squaredNumeratorReduced line 169
  26. lemma OAI.Problem340.SpherePolynomialPerturbation.contDiff_denominator line 178
  27. lemma OAI.Problem340.SpherePolynomialPerturbation.isOpen_domain line 183
  28. lemma OAI.Problem340.SpherePolynomialPerturbation.sphere_mem_domain line 186
  29. lemma OAI.Problem340.SpherePolynomialPerturbation.contDiffOn_ambientMap line 189
  30. lemma OAI.Problem340.SpherePolynomialPerturbation.contDiffAt_ambientMap line 208
  31. lemma OAI.Problem340.SpherePolynomialPerturbation.continuous_jointSphereMap line 212
  32. theorem OAI.Problem340.SpherePolynomialPerturbation.exists_smooth_ambient_neighborhood line 218
  33. def OAI.Problem340.SpherePolynomialPerturbation.jointMap line 227
  34. def OAI.Problem340.SpherePolynomialPerturbation.inducedMap line 230
  35. def OAI.Problem340.SpherePolynomialPerturbation.fadeParameters line 233
  36. def OAI.Problem340.SpherePolynomialPerturbation.fadeHomotopy line 242
  37. lemma OAI.Problem340.SpherePolynomialPerturbation.inducedMap_zero_apply line 252