OAI/Analysis/AncientFlat/Energy/EnergyQuadratic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParametrixUniqueness.mass line 10
  2. def OAI.ParametrixUniqueness.cross line 11
  3. def OAI.ParametrixUniqueness.pair line 12
  4. lemma OAI.ParametrixUniqueness.integrable_mass line 13
  5. lemma OAI.ParametrixUniqueness.integrable_cross line 17
  6. lemma OAI.ParametrixUniqueness.integrable_pair line 21
  7. lemma OAI.ParametrixUniqueness.mass_nonneg line 25
  8. lemma OAI.ParametrixUniqueness.cross_nonneg line 27
  9. lemma OAI.ParametrixUniqueness.weighted_young line 29
  10. lemma OAI.ParametrixUniqueness.abs_coeff_pair_le line 52
  11. lemma OAI.ParametrixUniqueness.abs_pair_le line 71