OAI/Geometry/TamingCompatibility/DifferentialForms/HermitianErrorSources.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.HermitianRadial.shiftedLogError line 19
  2. def OAI.TamingCompatibility.HermitianRadial.shiftedSqrtError line 21
  3. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogError_smooth line 25
  4. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtError_smooth line 31
  5. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogError_support line 37
  6. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtError_support line 41
  7. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogError_weight line 46
  8. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtError_weight line 51
  9. lemma OAI.TamingCompatibility.HermitianRadial.shiftedLogError_derivatives_bounded line 56
  10. lemma OAI.TamingCompatibility.HermitianRadial.shiftedSqrtError_derivatives_bounded line 65
  11. def OAI.TamingCompatibility.HermitianRadial.logErrorSchwartz line 77
  12. def OAI.TamingCompatibility.HermitianRadial.sqrtErrorSchwartz line 82
  13. def OAI.TamingCompatibility.HermitianRadial.logErrorSupported line 88
  14. def OAI.TamingCompatibility.HermitianRadial.sqrtErrorSupported line 91
  15. lemma OAI.TamingCompatibility.HermitianRadial.logErrorSchwartz_uniform_inputs line 95
  16. lemma OAI.TamingCompatibility.HermitianRadial.sqrtErrorSchwartz_uniform_inputs line 120
  17. def OAI.TamingCompatibility.HermitianRadial.logSourceSchwartz line 161
  18. def OAI.TamingCompatibility.HermitianRadial.sqrtSourceSchwartz line 167
  19. lemma OAI.TamingCompatibility.HermitianRadial.logSourceSchwartz_reconstruction line 173
  20. lemma OAI.TamingCompatibility.HermitianRadial.sqrtSourceSchwartz_reconstruction line 193