OAI/Geometry/Cannon/Energy/Square.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CannonPlanar.Square line 22
  2. def OAI.CannonPlanar.clampSquare line 24
  3. lemma OAI.CannonPlanar.continuous_clampSquare line 27
  4. lemma OAI.CannonPlanar.clampSquare_coe line 31
  5. theorem OAI.CannonPlanar.square_root line 34
  6. lemma OAI.CannonPlanar.positive_everywhere line 51
  7. lemma OAI.CannonPlanar.squared_parts line 61
  8. theorem OAI.CannonPlanar.square_zero line 69
  9. instance OAI.CannonPlanar.(instance at line 166) line 166
  10. def OAI.CannonPlanar.toComplex line 169
  11. lemma OAI.CannonPlanar.continuous_toComplex line 171
  12. lemma OAI.CannonPlanar.toComplex_re line 173
  13. lemma OAI.CannonPlanar.toComplex_im line 175
  14. lemma OAI.CannonPlanar.toComplex_injective line 177
  15. theorem OAI.CannonPlanar.paths_cross line 184
  16. theorem OAI.CannonPlanar.connected_joinedIn_open line 202
  17. theorem OAI.CannonPlanar.continuum_crosses_path line 217
  18. lemma OAI.CannonPlanar.clopen_neighborhood_of_component line 231
  19. lemma OAI.CannonPlanar.clopen_separator_of_components line 245
  20. theorem OAI.CannonPlanar.level_continuum line 263
  21. def OAI.CannonRegularization.FloodThresholds line 346
  22. def OAI.CannonRegularization.flood line 349
  23. lemma OAI.CannonRegularization.floodThresholds_bddBelow line 352
  24. lemma OAI.CannonRegularization.floodThresholds_nonempty line 358
  25. lemma OAI.CannonRegularization.le_flood line 365
  26. lemma OAI.CannonRegularization.flood_le_of_path line 372
  27. lemma OAI.CannonRegularization.flood_eq_on_band line 377
  28. lemma OAI.CannonRegularization.flood_le_upper line 383
  29. lemma OAI.CannonRegularization.flood_le_max line 389
  30. theorem OAI.CannonRegularization.flood_path_variation line 410
  31. theorem OAI.CannonRegularization.continuous_flood line 429
  32. def OAI.CannonRegularization.drain line 450
  33. lemma OAI.CannonRegularization.drain_le line 453
  34. lemma OAI.CannonRegularization.drain_eq_on_band line 460
  35. lemma OAI.CannonRegularization.drain_lower line 467
  36. theorem OAI.CannonRegularization.continuous_drain line 474
  37. theorem OAI.CannonRegularization.drain_path_variation line 479
  38. def OAI.CannonRegularization.pathMaximum line 488
  39. lemma OAI.CannonRegularization.pathMaximum_le_iff line 491
  40. theorem OAI.CannonRegularization.flood_eq_inf_pathMaximum line 498
  41. def OAI.CannonRegularization.pathPrefix line 519
  42. def OAI.CannonRegularization.suffix line 525
  43. theorem OAI.CannonRegularization.flood_strict_side line 531
  44. theorem OAI.CannonRegularization.drain_strict_side line 541
  45. lemma OAI.CannonRegularization.drain_min_le line 553
  46. lemma OAI.CannonRegularization.first_level_prefix line 563
  47. theorem OAI.CannonRegularization.regularized_low_side line 590
  48. lemma OAI.CannonRegularization.path_bounds_of_pairwise line 641
  49. theorem OAI.CannonRegularization.flood_drain_path_osc line 651