OAI/Analysis/TriangularHilbert/ErrorEnvelope.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularHilbert.Heat.errorProfile line 10
  2. def OAI.TriangularHilbert.Heat.endpointError line 12
  3. lemma OAI.TriangularHilbert.Heat.kernelProfile_zero line 14
  4. lemma OAI.TriangularHilbert.Heat.profile_contDiff line 18
  5. lemma OAI.TriangularHilbert.Heat.density_three_six line 22
  6. lemma OAI.TriangularHilbert.Heat.polynomial_exp_le line 32
  7. lemma OAI.TriangularHilbert.Heat.errorProfile_exists_bound line 41
  8. def OAI.TriangularHilbert.Heat.envelopeConstant line 95
  9. lemma OAI.TriangularHilbert.Heat.envelopeConstant_pos line 96
  10. lemma OAI.TriangularHilbert.Heat.errorProfile_bound line 97
  11. lemma OAI.TriangularHilbert.Heat.endpointError_bound line 100