OAI/Geometry/SmoothYau/Smoothness/CompactMetricInverseJets.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.geometric_complex_product_jet_bound line 39
  2. lemma OAI.YauCounterexamples.compact_raw_jet_bound line 67
  3. lemma OAI.YauCounterexamples.complex_power_envelope_jet_bound line 88
  4. theorem OAI.YauCounterexamples.real_power_weighted_jets line 138
  5. lemma OAI.YauCounterexamples.sphericalRadius_eq_planar_norm line 226
  6. lemma OAI.YauCounterexamples.spherical_chart_pullback_smooth line 238
  7. lemma OAI.YauCounterexamples.roundPlanarChart_contDiff line 245
  8. def OAI.YauCounterexamples.sphericalChartWeight line 249
  9. def OAI.YauCounterexamples.sphericalExceptionalInChart line 253
  10. lemma OAI.YauCounterexamples.sphericalChartWeight_lower line 257
  11. lemma OAI.YauCounterexamples.sphericalChartWeight_upper line 261
  12. theorem OAI.YauCounterexamples.spherical_background_input_bounds line 269
  13. theorem OAI.YauCounterexamples.spherical_exceptional_eventually_coverage line 292
  14. lemma OAI.YauCounterexamples.roundPower_abs_le_radius_pow line 316
  15. theorem OAI.YauCounterexamples.spherical_background_sign_small line 321
  16. lemma OAI.YauCounterexamples.complex_power_jet_bound line 386
  17. lemma OAI.YauCounterexamples.complex_power_jet_bound_on line 409
  18. theorem OAI.YauCounterexamples.annular_real_power_jets line 424
  19. theorem OAI.YauCounterexamples.roundPower_annular_chart_jets line 497
  20. lemma OAI.YauCounterexamples.compact_metric_inverse_jets line 551
  21. theorem OAI.YauCounterexamples.roundPower_conjugate_projection_control line 576