OAI/Geometry/SmoothYau/Smoothness/ThreeCoupledCleanChartJets.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.sphericalWaveLift line 37
  2. lemma OAI.YauCounterexamples.sphericalWaveLift_apply line 39
  3. lemma OAI.YauCounterexamples.sphericalWaveLift_smooth line 43
  4. lemma OAI.YauCounterexamples.sphericalWaveLift_tsupport line 47
  5. lemma OAI.YauCounterexamples.sphericalWaveLift_laplacian line 56
  6. lemma OAI.YauCounterexamples.spherical_sublevel_compact line 64
  7. theorem OAI.YauCounterexamples.spherical_wave_lift_jets line 68
  8. theorem OAI.YauCounterexamples.spherical_wave_centered_first_jet line 126
  9. lemma OAI.YauCounterexamples.scalarDifferential_chart_vector line 222
  10. lemma OAI.YauCounterexamples.chart_derivative_dual_bound line 235
  11. lemma OAI.YauCounterexamples.realWaveJet_intrinsic_upper line 246
  12. lemma OAI.YauCounterexamples.realWaveJet_to_intrinsic_lower line 296
  13. def OAI.YauCounterexamples.sphericalWeight line 318
  14. lemma OAI.YauCounterexamples.sphericalWeight_pos line 321
  15. lemma OAI.YauCounterexamples.spherical_inner_is_exceptional line 324
  16. lemma OAI.YauCounterexamples.spherical_global_exceptional_coverage line 347
  17. theorem OAI.YauCounterexamples.spherical_global_jet_lower line 366
  18. lemma OAI.YauCounterexamples.sphericalWeight_chart line 444
  19. lemma OAI.YauCounterexamples.sphericalWeight_ge_exp line 449
  20. lemma OAI.YauCounterexamples.real_smooth_add_jet_bound line 453
  21. theorem OAI.YauCounterexamples.spherical_wave_background_chart_bounds line 460
  22. lemma OAI.YauCounterexamples.real_power_variable_weighted_jets line 595
  23. def OAI.YauCounterexamples.threeWeight line 624
  24. lemma OAI.YauCounterexamples.threeWeight_pos line 626
  25. lemma OAI.YauCounterexamples.threeCoupled_split_powers line 630
  26. theorem OAI.YauCounterexamples.threeCoupled_weighted_chart_jets line 637
  27. lemma OAI.YauCounterexamples.threeCoupled_dominated_chart_jets line 686
  28. theorem OAI.YauCounterexamples.threeCoupled_dominated_residual_rapid_decay line 719
  29. lemma OAI.YauCounterexamples.threeCoupled_clean_chart_jets line 775
  30. theorem OAI.YauCounterexamples.threeCoupled_conjugate_projection_uniform line 807