OAI/Geometry/TamingCompatibility/DifferentialForms/RadialErrorSources.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TamingCompatibility.RadialPotential.tsupport_translated_subset line 17
  2. def OAI.TamingCompatibility.RadialPotential.shiftedLogError line 25
  3. def OAI.TamingCompatibility.RadialPotential.shiftedSqrtError line 27
  4. lemma OAI.TamingCompatibility.RadialPotential.shiftedLogError_smooth line 31
  5. lemma OAI.TamingCompatibility.RadialPotential.shiftedSqrtError_smooth line 37
  6. lemma OAI.TamingCompatibility.RadialPotential.shiftedLogError_support line 43
  7. lemma OAI.TamingCompatibility.RadialPotential.shiftedSqrtError_support line 47
  8. lemma OAI.TamingCompatibility.RadialPotential.shiftedLogError_weight line 52
  9. lemma OAI.TamingCompatibility.RadialPotential.shiftedSqrtError_weight line 57
  10. lemma OAI.TamingCompatibility.RadialPotential.shiftedLogError_derivatives_bounded line 62
  11. lemma OAI.TamingCompatibility.RadialPotential.shiftedSqrtError_derivatives_bounded line 71
  12. def OAI.TamingCompatibility.RadialPotential.logErrorSchwartz line 83
  13. def OAI.TamingCompatibility.RadialPotential.sqrtErrorSchwartz line 88
  14. def OAI.TamingCompatibility.RadialPotential.logErrorSupported line 94
  15. def OAI.TamingCompatibility.RadialPotential.sqrtErrorSupported line 97
  16. lemma OAI.TamingCompatibility.RadialPotential.logErrorSchwartz_uniform_inputs line 101
  17. lemma OAI.TamingCompatibility.RadialPotential.sqrtErrorSchwartz_uniform_inputs line 126