OAI/Geometry/QuadricBundles/Removability.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuadricCounterexample.usc_ge_of_ae_ge line 10
  2. lemma OAI.QuadricCounterexample.DiskSubharmonicOn.eq_on_ball_of_max line 29
  3. theorem OAI.QuadricCounterexample.DiskSubharmonicOn.eq_const_of_max line 50
  4. def OAI.QuadricCounterexample.LocalDiskSubmeanOn line 77
  5. theorem OAI.QuadricCounterexample.LocalDiskSubmeanOn.eq_on_ball_of_max line 82
  6. theorem OAI.QuadricCounterexample.LocalDiskSubmeanOn.eq_const_of_max line 99
  7. theorem OAI.QuadricCounterexample.LocalDiskSubmeanOn.le_boundary line 125
  8. theorem OAI.QuadricCounterexample.compact_family_local_submean line 146
  9. theorem OAI.QuadricCounterexample.submean_of_locally_psh line 191
  10. theorem OAI.QuadricCounterexample.DiskPshOn.of_locally line 280
  11. theorem OAI.QuadricCounterexample.radialIntegral_of_circle_means line 296
  12. lemma OAI.QuadricCounterexample.log_norm_subharmonic line 338
  13. theorem OAI.QuadricCounterexample.log_norm_psh line 377
  14. lemma OAI.QuadricCounterexample.DiskPshOn.comp line 383
  15. lemma OAI.QuadricCounterexample.DiskSubharmonicOn.add line 392
  16. lemma OAI.QuadricCounterexample.DiskSubharmonicOn.max line 403
  17. lemma OAI.QuadricCounterexample.DiskPshOn.add line 419
  18. lemma OAI.QuadricCounterexample.DiskPshOn.max line 426
  19. lemma OAI.QuadricCounterexample.diskPshOn_const line 433
  20. lemma OAI.QuadricCounterexample.DiskPshOn.const_mul_of_continuous line 442
  21. lemma OAI.QuadricCounterexample.DiskPshOn.mono line 455
  22. lemma OAI.QuadricCounterexample.DiskPshOn.congr line 459
  23. def OAI.QuadricCounterexample.logBarrier line 476
  24. lemma OAI.QuadricCounterexample.logBarrier_eventually_zero line 479
  25. lemma OAI.QuadricCounterexample.logBarrier_continuousOn line 497
  26. lemma OAI.QuadricCounterexample.logBarrier_nonneg line 515
  27. lemma OAI.QuadricCounterexample.logBarrier_le line 522
  28. lemma OAI.QuadricCounterexample.logBarrier_tendsto_of_ne_zero line 535
  29. theorem OAI.QuadricCounterexample.logBarrier_psh line 543
  30. theorem OAI.QuadricCounterexample.DiskSubharmonicOn.pointwise_limit line 566
  31. theorem OAI.QuadricCounterexample.DiskSubharmonicOn.integral line 594
  32. theorem OAI.QuadricCounterexample.DiskPshOn.pointwise_limit line 615
  33. lemma OAI.QuadricCounterexample.continuousOn_integral_compact_parameter line 631
  34. theorem OAI.QuadricCounterexample.DiskPshOn.integral_compact_parameter line 648
  35. theorem OAI.QuadricCounterexample.averaged_hypersurface_removal line 678
  36. lemma OAI.QuadricCounterexample.interval_translation_ne_zero_ae line 743
  37. lemma OAI.QuadricCounterexample.first_translation_continuous line 759
  38. lemma OAI.QuadricCounterexample.first_translation_dist line 765
  39. lemma OAI.QuadricCounterexample.translation_average_tendsto line 774
  40. theorem OAI.QuadricCounterexample.first_hyperplane_removable_ball line 828
  41. theorem OAI.QuadricCounterexample.first_hyperplane_removable line 873