OAI/Analysis/NodalLength/Carleman.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpNodal.Carleman.no_normalized_quasimodes line 17
  2. lemma OAI.SharpNodal.Carleman.SupportLimit.reindex line 62
  3. lemma OAI.SharpNodal.Carleman.SupportLimit.finite_bound line 72
  4. lemma OAI.SharpNodal.Carleman.normalized_derivative_potential_limit line 90
  5. lemma OAI.SharpNodal.Carleman.abs_le_mul_of_div line 112
  6. theorem OAI.SharpNodal.Carleman.no_asymptotic_quasimodes line 118
  7. def OAI.SharpNodal.Carleman.tiltedWeight line 182
  8. lemma OAI.SharpNodal.Carleman.smooth_tiltedWeight line 185
  9. lemma OAI.SharpNodal.Carleman.partial_linear line 189
  10. lemma OAI.SharpNodal.Carleman.partial_neg line 196
  11. lemma OAI.SharpNodal.Carleman.partial_sub line 200
  12. lemma OAI.SharpNodal.Carleman.partial_const line 205
  13. lemma OAI.SharpNodal.Carleman.partial_tiltedWeight line 208
  14. lemma OAI.SharpNodal.Carleman.partial2_tiltedWeight line 217
  15. lemma OAI.SharpNodal.Carleman.partial4_tiltedWeight line 226
  16. def OAI.SharpNodal.Carleman.ShrinkingSupports line 236
  17. lemma OAI.SharpNodal.Carleman.ShrinkingSupports.continuousAt line 239
  18. lemma OAI.SharpNodal.Carleman.SupportLimit.congr_eventually line 244
  19. lemma OAI.SharpNodal.Carleman.SupportLimit.zero_of_bound line 250
  20. lemma OAI.SharpNodal.Carleman.tilted_gradient_limit line 260
  21. lemma OAI.SharpNodal.Carleman.tilted_hessian_limit line 280
  22. lemma OAI.SharpNodal.Carleman.tilted_bilaplacian_limit line 291
  23. def OAI.SharpNodal.Carleman.coordinateGradient line 307
  24. lemma OAI.SharpNodal.Carleman.coordinateGradient_apply line 310
  25. lemma OAI.SharpNodal.Carleman.normalized_small_potential line 314
  26. lemma OAI.SharpNodal.Carleman.normalized_potential_gradient_limit line 327
  27. theorem OAI.SharpNodal.Carleman.no_tilted_quasimodes line 343
  28. def OAI.SharpNodal.Carleman.conjugatedOperator line 388
  29. lemma OAI.SharpNodal.Carleman.laplacian_const_mul line 391
  30. lemma OAI.SharpNodal.Carleman.skew_const_mul line 399
  31. lemma OAI.SharpNodal.Carleman.conjugatedOperator_const_mul line 406
  32. lemma OAI.SharpNodal.Carleman.ShrinkingSupports.of_ball line 414
  33. theorem OAI.SharpNodal.Carleman.local_carleman_conjugated line 425
  34. theorem OAI.SharpNodal.Carleman.local_carleman line 502