OAI/Geometry/QuadricBundles/Plurisubharmonic.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuadricCounterexample.radialIntegral line 11
  2. lemma OAI.QuadricCounterexample.radialIntegral_zero line 14
  3. lemma OAI.QuadricCounterexample.radialIntegral_rotation line 18
  4. lemma OAI.QuadricCounterexample.radialIntegral_eq_of_norm_eq line 30
  5. lemma OAI.QuadricCounterexample.radialIntegral_pos_radius line 40
  6. lemma OAI.QuadricCounterexample.complex_closedBall_ae_ball line 64
  7. lemma OAI.QuadricCounterexample.compact_integral_continuousOn line 72
  8. def OAI.QuadricCounterexample.radialLinear line 89
  9. lemma OAI.QuadricCounterexample.radialLinear_apply line 90
  10. def OAI.QuadricCounterexample.radialFirst line 92
  11. def OAI.QuadricCounterexample.radialSecond line 94
  12. lemma OAI.QuadricCounterexample.radialSecond_apply line 98
  13. lemma OAI.QuadricCounterexample.radialFirst_hasFDerivAt line 102
  14. lemma OAI.QuadricCounterexample.radialSecond_hasFDerivAt line 107
  15. lemma OAI.QuadricCounterexample.radialFamily_maps_closedBall line 113
  16. lemma OAI.QuadricCounterexample.radialFamily_continuous line 121
  17. lemma OAI.QuadricCounterexample.radialFirst_continuous line 127
  18. lemma OAI.QuadricCounterexample.radialSecond_continuous line 140
  19. lemma OAI.QuadricCounterexample.radialIntegral_C2 line 156
  20. lemma OAI.QuadricCounterexample.integral_bilinear_apply line 186
  21. lemma OAI.QuadricCounterexample.radialIntegral_laplacian line 194
  22. lemma OAI.QuadricCounterexample.radialIntegral_laplacian_nonneg line 243
  23. theorem OAI.QuadricCounterexample.C2_disk_submean line 253
  24. def OAI.QuadricCounterexample.DiskSubharmonicOn line 293
  25. theorem OAI.QuadricCounterexample.DiskSubharmonicOn.of_C2_laplacian_nonneg line 298
  26. lemma OAI.QuadricCounterexample.hessian_comp_apply line 304
  27. lemma OAI.QuadricCounterexample.holomorphic_real_hessian_trace line 331
  28. lemma OAI.QuadricCounterexample.holomorphic_real_derivative_I line 340
  29. def OAI.QuadricCounterexample.leviTrace line 349
  30. lemma OAI.QuadricCounterexample.holomorphic_disk_hessian_trace line 354
  31. def OAI.QuadricCounterexample.DiskPshOn line 370
  32. theorem OAI.QuadricCounterexample.DiskPshOn.of_C2_leviTrace_nonneg line 375