OAI/Geometry/KahlerSplitting/MetricBounds.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalCoverSplitting.continuousMetricInChart line 16
  2. theorem OAI.UniversalCoverSplitting.continuousMetricInChart_apply line 24
  3. theorem OAI.UniversalCoverSplitting.KahlerMetric.continuous_metricInChart line 27
  4. theorem OAI.UniversalCoverSplitting.KahlerMetric.continuous_quadraticInChart line 35
  5. theorem OAI.UniversalCoverSplitting.metricInChart_smul line 41
  6. theorem OAI.UniversalCoverSplitting.chart_inverse_derivative_injective line 49
  7. theorem OAI.UniversalCoverSplitting.KahlerMetric.positive_quadraticInChart line 72
  8. theorem OAI.UniversalCoverSplitting.metricInChart_forward line 80
  9. theorem OAI.UniversalCoverSplitting.projectionInChart_forward line 98
  10. theorem OAI.UniversalCoverSplitting.KahlerMetric.exists_projection_bound_on_chartCompact line 116
  11. theorem OAI.UniversalCoverSplitting.KahlerMetric.nonnegative line 146
  12. theorem OAI.UniversalCoverSplitting.KahlerMetric.exists_uniform_projection_quadraticBound line 152
  13. def OAI.UniversalCoverSplitting.metricNorm line 184
  14. theorem OAI.UniversalCoverSplitting.KahlerMetric.exists_uniform_projection_normBound line 187
  15. def OAI.UniversalCoverSplitting.KahlerMetric.realInnerCore line 198
  16. theorem OAI.UniversalCoverSplitting.metricNorm_add_le line 206
  17. theorem OAI.UniversalCoverSplitting.metric_abs_le line 212
  18. theorem OAI.UniversalCoverSplitting.KahlerMetric.orthogonal_I line 217
  19. theorem OAI.UniversalCoverSplitting.KahlerMetric.quadratic_complex_smul line 224
  20. theorem OAI.UniversalCoverSplitting.metricNorm_complex_smul line 237
  21. theorem OAI.UniversalCoverSplitting.projectionInChart_sub_id line 251
  22. theorem OAI.UniversalCoverSplitting.HolomorphicProjection.complement line 276
  23. theorem OAI.UniversalCoverSplitting.HolomorphicSplitting.complement_holomorphic line 284
  24. theorem OAI.UniversalCoverSplitting.KahlerMetric.exists_uniform_splitting_bound line 287
  25. theorem OAI.UniversalCoverSplitting.mixed_direction_metric_norm_le line 298
  26. theorem OAI.UniversalCoverSplitting.exists_quadratic_comparison line 342
  27. theorem OAI.UniversalCoverSplitting.KahlerMetric.exists_chart_metric_comparison line 397
  28. theorem OAI.UniversalCoverSplitting.KahlerMetric.exists_chart_speed_comparison line 418
  29. def OAI.UniversalCoverSplitting.curveSpeed line 447
  30. def OAI.UniversalCoverSplitting.curveArea line 450
  31. theorem OAI.UniversalCoverSplitting.curveSpeed_nonneg line 453
  32. theorem OAI.UniversalCoverSplitting.chart_deriv_curve line 456
  33. theorem OAI.UniversalCoverSplitting.curveSpeed_eq_chart line 467
  34. theorem OAI.UniversalCoverSplitting.curveSpeed_continuousOn line 476
  35. theorem OAI.UniversalCoverSplitting.curveSpeed_affine line 502