OAI/Analysis/AncientFlat/Energy/EnergyWeight.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParametrixUniqueness.radius line 10
  2. def OAI.ParametrixUniqueness.weight line 11
  3. lemma OAI.ParametrixUniqueness.radius_pos line 13
  4. lemma OAI.ParametrixUniqueness.radius_sq line 15
  5. lemma OAI.ParametrixUniqueness.radius_one_le line 17
  6. lemma OAI.ParametrixUniqueness.norm_le_radius line 21
  7. lemma OAI.ParametrixUniqueness.weight_pos line 25
  8. lemma OAI.ParametrixUniqueness.contDiff_radius line 28
  9. lemma OAI.ParametrixUniqueness.contDiff_weight line 30
  10. lemma OAI.ParametrixUniqueness.hasFDerivAt_radius line 33
  11. lemma OAI.ParametrixUniqueness.hasFDerivAt_weight line 40
  12. lemma OAI.ParametrixUniqueness.norm_fderiv_weight_le line 46
  13. def OAI.ParametrixUniqueness.dir line 54
  14. lemma OAI.ParametrixUniqueness.contDiff_dir line 57
  15. def OAI.ParametrixUniqueness.radialComponent line 62
  16. lemma OAI.ParametrixUniqueness.contDiff_radialComponent line 64
  17. lemma OAI.ParametrixUniqueness.radialComponent_bound line 68
  18. lemma OAI.ParametrixUniqueness.dir_radialComponent line 75
  19. lemma OAI.ParametrixUniqueness.dir_weight line 90
  20. lemma OAI.ParametrixUniqueness.dir_dir_weight line 97
  21. lemma OAI.ParametrixUniqueness.dir_dir_weight_bound line 111
  22. lemma OAI.ParametrixUniqueness.integrable_weight line 128