OAI/Analysis/NodalLength/SupportLimits.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpNodal.Carleman.SupportIndex line 15
  2. def OAI.SharpNodal.Carleman.supportFilter line 17
  3. def OAI.SharpNodal.Carleman.SupportLimit line 20
  4. lemma OAI.SharpNodal.Carleman.eventually_support_iff line 24
  5. lemma OAI.SharpNodal.Carleman.SupportLimit.eventually_abs_sub_le line 37
  6. lemma OAI.SharpNodal.Carleman.SupportLimit.const line 45
  7. lemma OAI.SharpNodal.Carleman.SupportLimit.of_seq line 49
  8. lemma OAI.SharpNodal.Carleman.SupportLimit.add line 53
  9. lemma OAI.SharpNodal.Carleman.SupportLimit.sub line 57
  10. lemma OAI.SharpNodal.Carleman.SupportLimit.mul line 61
  11. lemma OAI.SharpNodal.Carleman.SupportLimit.neg line 65
  12. lemma OAI.SharpNodal.Carleman.SupportLimit.pow line 68
  13. lemma OAI.SharpNodal.Carleman.coefficient_square_tendsto_const_support line 72
  14. lemma OAI.SharpNodal.Carleman.coefficient_pairing_support_zero_of_bound line 91
  15. def OAI.SharpNodal.Carleman.hessianGradientEnergy line 116
  16. lemma OAI.SharpNodal.Carleman.carleman_commutator_energy line 120
  17. lemma OAI.SharpNodal.Carleman.integral_normalized_hessianGradient line 132
  18. lemma OAI.SharpNodal.Carleman.normalized_hessianGradient_limit line 147
  19. lemma OAI.SharpNodal.Carleman.variable_quadratic_difference_support_limit line 164
  20. lemma OAI.SharpNodal.Carleman.normalized_hessian_trace_support_limit line 206
  21. lemma OAI.SharpNodal.Carleman.normalized_gradient_energy_support_limit line 239
  22. lemma OAI.SharpNodal.Carleman.l2sq_coefficient_mul_support_zero line 260
  23. lemma OAI.SharpNodal.Carleman.normalized_parallel_support_limit line 278
  24. lemma OAI.SharpNodal.Carleman.normalized_potential_coefficient_limit line 322
  25. lemma OAI.SharpNodal.Carleman.normalized_bilaplacian_limit line 336
  26. lemma OAI.SharpNodal.Carleman.normalized_potentialTransport_limit line 356
  27. lemma OAI.SharpNodal.Carleman.hessian_form_expansion line 373
  28. lemma OAI.SharpNodal.Carleman.normalized_commutator_trace_limit line 382