OAI/Analysis/NodalLength/Normalization.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpNodal.Carleman.sqrt_div_tendsto_zero line 16
  2. lemma OAI.SharpNodal.Carleman.pairing_div_square_tendsto_zero line 29
  3. lemma OAI.SharpNodal.Carleman.coefficient_pairing_tendsto_zero_of_bound line 49
  4. lemma OAI.SharpNodal.Carleman.coefficient_square_tendsto_const line 64
  5. lemma OAI.SharpNodal.Carleman.l2sq_div line 88
  6. def OAI.SharpNodal.Carleman.normalizedPartial line 94
  7. lemma OAI.SharpNodal.Carleman.smooth_normalizedPartial line 97
  8. lemma OAI.SharpNodal.Carleman.compact_normalizedPartial line 100
  9. lemma OAI.SharpNodal.Carleman.normalizedPartial_energy line 105
  10. lemma OAI.SharpNodal.Carleman.normalized_coefficient_integral line 110
  11. lemma OAI.SharpNodal.Carleman.normalized_gradient_energy_limit line 121
  12. lemma OAI.SharpNodal.Carleman.normalizedPartial_tsupport_subset line 142
  13. lemma OAI.SharpNodal.Carleman.l2sq_add_le line 147
  14. lemma OAI.SharpNodal.Carleman.l2sq_coefficient_mul_le line 152
  15. lemma OAI.SharpNodal.Carleman.l2sq_add_tendsto_zero line 172
  16. lemma OAI.SharpNodal.Carleman.l2sq_coefficient_mul_tendsto_zero line 182
  17. lemma OAI.SharpNodal.Carleman.scaled_operator_square_limit line 195
  18. def OAI.SharpNodal.Carleman.normalizedTransport line 215
  19. lemma OAI.SharpNodal.Carleman.smooth_normalizedTransport line 219
  20. lemma OAI.SharpNodal.Carleman.compact_normalizedTransport line 224
  21. lemma OAI.SharpNodal.Carleman.normalized_transport_identity line 228
  22. lemma OAI.SharpNodal.Carleman.normalized_laplacian_abs_le line 235
  23. lemma OAI.SharpNodal.Carleman.normalized_transport_square_limit line 251
  24. lemma OAI.SharpNodal.Carleman.normalized_parallel_limit line 293
  25. lemma OAI.SharpNodal.Carleman.integral_normalized_hessian line 341
  26. lemma OAI.SharpNodal.Carleman.normalized_hessian_expansion line 355
  27. lemma OAI.SharpNodal.Carleman.integral_coefficient_difference line 376
  28. lemma OAI.SharpNodal.Carleman.variable_quadratic_difference_limit line 390
  29. lemma OAI.SharpNodal.Carleman.normalized_hessian_trace_limit line 427