OAI/Geometry/QuadricBundles/RootTrace.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuadricCounterexample.chosenRoot line 14
  2. lemma OAI.QuadricCounterexample.chosenRoot_pow line 17
  3. lemma OAI.QuadricCounterexample.same_power_orbit line 20
  4. def OAI.QuadricCounterexample.rootOrbitAverage line 28
  5. def OAI.QuadricCounterexample.rootTrace line 31
  6. lemma OAI.QuadricCounterexample.rootOrbitAverage_orbit line 34
  7. lemma OAI.QuadricCounterexample.rootTrace_pow line 44
  8. lemma OAI.QuadricCounterexample.continuous_rootOrbitAverage line 50
  9. theorem OAI.QuadricCounterexample.continuous_rootTrace line 58
  10. lemma OAI.QuadricCounterexample.rootTrace_zero line 67
  11. lemma OAI.QuadricCounterexample.rootTrace_nonneg line 78
  12. lemma OAI.QuadricCounterexample.DiskPshOn.sum line 90
  13. lemma OAI.QuadricCounterexample.rootTrace_eq_of_pow line 104
  14. theorem OAI.QuadricCounterexample.continuousOn_rootTrace line 108
  15. def OAI.QuadricCounterexample.centeredRoot line 130
  16. lemma OAI.QuadricCounterexample.centeredRoot_pow line 133
  17. lemma OAI.QuadricCounterexample.centeredRoot_differentiableOn line 138
  18. theorem OAI.QuadricCounterexample.rootTrace_psh_off_zero line 149
  19. theorem OAI.QuadricCounterexample.rootTrace_psh line 189
  20. def OAI.QuadricCounterexample.swapBase line 213
  21. lemma OAI.QuadricCounterexample.swapBase_swapBase line 216
  22. lemma OAI.QuadricCounterexample.differentiable_swapBase line 218
  23. def OAI.QuadricCounterexample.secondRootTrace line 225
  24. lemma OAI.QuadricCounterexample.continuousOn_secondRootTrace line 228
  25. lemma OAI.QuadricCounterexample.secondRootTrace_psh line 241
  26. def OAI.QuadricCounterexample.doubleRootTrace line 257
  27. lemma OAI.QuadricCounterexample.doubleRootTrace_formula line 261
  28. lemma OAI.QuadricCounterexample.continuousOn_doubleRootTrace line 271
  29. theorem OAI.QuadricCounterexample.doubleRootTrace_psh line 279