OAI/Analysis/AncientFlat/Energy/EnergyTime.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParametrixUniqueness.bounded_bcf line 9
  2. lemma OAI.ParametrixUniqueness.pair_comm line 13
  3. lemma OAI.ParametrixUniqueness.pair_self line 16
  4. lemma OAI.ParametrixUniqueness.pair_add_left line 18
  5. lemma OAI.ParametrixUniqueness.pair_smul_left line 22
  6. lemma OAI.ParametrixUniqueness.pair_add_right line 26
  7. lemma OAI.ParametrixUniqueness.pair_smul_right line 28
  8. def OAI.ParametrixUniqueness.pairLM line 30
  9. lemma OAI.ParametrixUniqueness.cross_bcf_le line 32
  10. lemma OAI.ParametrixUniqueness.pair_bcf_bound line 42
  11. def OAI.ParametrixUniqueness.pairCLM line 44
  12. lemma OAI.ParametrixUniqueness.pairCLM_apply line 46
  13. lemma OAI.ParametrixUniqueness.hasDerivAt_bilinear_diag line 47
  14. lemma OAI.ParametrixUniqueness.hasDerivAt_mass line 53
  15. lemma OAI.ParametrixUniqueness.continuousOn_mass line 57
  16. lemma OAI.ParametrixUniqueness.mass_eq_zero_bcf line 61