OAI/Analysis/HotSpots/TraceRank.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.CircleGeometry.continuous_exists_eq_antipodal line 15
  2. lemma OAI.StrictHotSpots.CircleGeometry.not_continuous_injective_to_real line 31
  3. theorem OAI.StrictHotSpots.CircleGeometry.not_subset_affine_line line 38
  4. lemma OAI.StrictHotSpots.HilbertMultipliers.coordinate_separates line 80
  5. lemma OAI.StrictHotSpots.HilbertMultipliers.pair_independent line 88
  6. lemma OAI.StrictHotSpots.HilbertMultipliers.rank_two_spanning line 103
  7. lemma OAI.StrictHotSpots.HilbertMultipliers.scalar_affine_elimination line 115
  8. theorem OAI.StrictHotSpots.HilbertMultipliers.rank_two_affine_support line 126
  9. lemma OAI.StrictHotSpots.HilbertMultipliers.nonempty_open_two_points line 152
  10. theorem OAI.StrictHotSpots.HilbertMultipliers.not_dense_support_of_rank_two line 162
  11. theorem OAI.StrictHotSpots.HilbertMultipliers.no_nonzero_multiplier_in_rank_one line 182
  12. def OAI.StrictHotSpots.HilbertMultipliers.vanishingOn line 216
  13. lemma OAI.StrictHotSpots.HilbertMultipliers.vanishingOn_le line 226
  14. instance OAI.StrictHotSpots.HilbertMultipliers.(instance at line 229) line 229
  15. theorem OAI.StrictHotSpots.HilbertMultipliers.multiplier_contradiction line 237
  16. def OAI.StrictHotSpots.closedGradientTrace line 279
  17. def OAI.StrictHotSpots.closedTraceSpace line 285
  18. lemma OAI.StrictHotSpots.closedTraceSpace_rank line 288
  19. lemma OAI.StrictHotSpots.closedTraceSpace_local_rank line 297
  20. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.boundary_gradient_not_zero line 355