OAI/Analysis/AncientFlat/Energy/EnergyIBP.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParametrixUniqueness.Bounded line 12
  2. def OAI.ParametrixUniqueness.Decays line 13
  3. def OAI.ParametrixUniqueness.BoundedJets line 14
  4. lemma OAI.ParametrixUniqueness.Bounded.add line 18
  5. lemma OAI.ParametrixUniqueness.Bounded.sum line 23
  6. lemma OAI.ParametrixUniqueness.Bounded.norm line 32
  7. lemma OAI.ParametrixUniqueness.Bounded.mul line 35
  8. lemma OAI.ParametrixUniqueness.Bounded.inner line 43
  9. lemma OAI.ParametrixUniqueness.BoundedJets.of_le line 49
  10. lemma OAI.ParametrixUniqueness.BoundedJets.zero line 51
  11. lemma OAI.ParametrixUniqueness.BoundedJets.dir line 53
  12. lemma OAI.ParametrixUniqueness.Decays.add line 66
  13. lemma OAI.ParametrixUniqueness.Decays.smul line 72
  14. lemma OAI.ParametrixUniqueness.Decays.inner line 83
  15. lemma OAI.ParametrixUniqueness.decays_weight line 94
  16. lemma OAI.ParametrixUniqueness.decays_dir_weight line 96
  17. lemma OAI.ParametrixUniqueness.decays_dir_dir_weight line 100
  18. lemma OAI.ParametrixUniqueness.dir_smul line 103
  19. lemma OAI.ParametrixUniqueness.dir_add line 110
  20. lemma OAI.ParametrixUniqueness.decays_weight_mul line 116
  21. lemma OAI.ParametrixUniqueness.decays_dir_weight_mul line 118
  22. lemma OAI.ParametrixUniqueness.Decays.integrable line 126
  23. lemma OAI.ParametrixUniqueness.integral_inner_dir line 130