OAI/Analysis/NodalLength/Energy.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpNodal.Carleman.l2sq_pos line 15
  2. def OAI.SharpNodal.Carleman.l2norm line 23
  3. lemma OAI.SharpNodal.Carleman.l2norm_nonneg line 25
  4. lemma OAI.SharpNodal.Carleman.l2norm_sq line 27
  5. lemma OAI.SharpNodal.Carleman.normalize_l2sq line 30
  6. lemma OAI.SharpNodal.Carleman.partial_tsupport_subset line 36
  7. lemma OAI.SharpNodal.Carleman.abs_mul_mul_le line 40
  8. lemma OAI.SharpNodal.Carleman.integral_coefficient_mul_abs_le line 51
  9. lemma OAI.SharpNodal.Carleman.integral_coefficient_square_abs_le line 71
  10. lemma OAI.SharpNodal.Carleman.coefficient_pairing_tendsto_zero line 80
  11. def OAI.SharpNodal.Carleman.plusPart line 92
  12. lemma OAI.SharpNodal.Carleman.smooth_plus line 94
  13. lemma OAI.SharpNodal.Carleman.compact_plus line 97
  14. def OAI.SharpNodal.Carleman.gradientEnergy line 100
  15. lemma OAI.SharpNodal.Carleman.gradientEnergy_nonneg line 102
  16. lemma OAI.SharpNodal.Carleman.plus_energy_identity line 105
  17. lemma OAI.SharpNodal.Carleman.pairing_abs_le_l2norm line 114
  18. lemma OAI.SharpNodal.Carleman.l2norm_eq_one line 123
  19. lemma OAI.SharpNodal.Carleman.plus_energy_bound line 126
  20. lemma OAI.SharpNodal.Carleman.commutator_le_sum_square line 138
  21. lemma OAI.SharpNodal.Carleman.carleman_scalar_bootstrap line 144
  22. def OAI.SharpNodal.Carleman.hessianEnergy line 184
  23. def OAI.SharpNodal.Carleman.bilaplacianEnergy line 188
  24. def OAI.SharpNodal.Carleman.potentialTransport line 192
  25. lemma OAI.SharpNodal.Carleman.transport_commutator_energy line 195
  26. lemma OAI.SharpNodal.Carleman.hessianEnergy_abs_le line 204
  27. lemma OAI.SharpNodal.Carleman.bilaplacianEnergy_abs_le line 223
  28. lemma OAI.SharpNodal.Carleman.potentialTransport_abs_le line 239
  29. lemma OAI.SharpNodal.Carleman.transport_commutator_abs_le line 251
  30. lemma OAI.SharpNodal.Carleman.operator_bootstrap line 276