OAI/Geometry/SmoothYau/SphereMetric/ExistsThreeScalarProducer.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.threeWaveLift line 17
  2. lemma OAI.YauCounterexamples.threeWaveLift_apply line 19
  3. lemma OAI.YauCounterexamples.threeWaveLift_smooth line 24
  4. lemma OAI.YauCounterexamples.threeWaveLift_tsupport line 29
  5. lemma OAI.YauCounterexamples.threeWaveLift_laplacian line 36
  6. lemma OAI.YauCounterexamples.threeNormalInv_continuous line 51
  7. lemma OAI.YauCounterexamples.threeNormalInv_image_source line 53
  8. lemma OAI.YauCounterexamples.linearEquiv_comp_jets_bound line 58
  9. theorem OAI.YauCounterexamples.three_wave_lift_jets line 73
  10. lemma OAI.YauCounterexamples.three_chart_pullback_smooth line 133
  11. lemma OAI.YauCounterexamples.threeCoupled_residual_tsupport line 139
  12. theorem OAI.YauCounterexamples.threeCoupled_global_residual_rapid_decay line 158
  13. lemma OAI.YauCounterexamples.threeWeight_ge_exp line 191
  14. theorem OAI.YauCounterexamples.three_wave_background_chart_bounds line 204
  15. lemma OAI.YauCounterexamples.three_centered_gradient_norm line 327
  16. lemma OAI.YauCounterexamples.three_centered_gradient_norm_of_agree line 332
  17. lemma OAI.YauCounterexamples.three_wave_centered_first_jet line 348
  18. lemma OAI.YauCounterexamples.three_compact_direction_metric_bound line 408
  19. lemma OAI.YauCounterexamples.three_realWaveJet_intrinsic_upper line 438
  20. lemma OAI.YauCounterexamples.three_exceptional_intrinsic_margin line 496
  21. lemma OAI.YauCounterexamples.weighted_exterior_absorption line 531
  22. lemma OAI.YauCounterexamples.three_exterior_intrinsic_margin line 542
  23. theorem OAI.YauCounterexamples.exists_three_global_quasimodes line 627
  24. theorem OAI.YauCounterexamples.exists_three_scalar_producer line 767