OAI/Geometry/TamingCompatibility/DifferentialForms/RadialReconstruction.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.RadialPotential.logSourceSchwartz line 21
  2. def OAI.TamingCompatibility.RadialPotential.sqrtSourceSchwartz line 27
  3. lemma OAI.TamingCompatibility.RadialPotential.logSourceSchwartz_reconstruction line 33
  4. lemma OAI.TamingCompatibility.RadialPotential.sqrtSourceSchwartz_reconstruction line 53
  5. def OAI.TamingCompatibility.RadialPotential.logShellSupported line 89
  6. def OAI.TamingCompatibility.RadialPotential.logInnerSupported line 93
  7. def OAI.TamingCompatibility.RadialPotential.logSourceSupported line 97
  8. lemma OAI.TamingCompatibility.RadialPotential.logSupported_reconstruction line 101
  9. def OAI.TamingCompatibility.RadialPotential.sqrtShellSupported line 111
  10. def OAI.TamingCompatibility.RadialPotential.sqrtInnerSupported line 115
  11. def OAI.TamingCompatibility.RadialPotential.sqrtSourceSupported line 119
  12. lemma OAI.TamingCompatibility.RadialPotential.sqrtSupported_reconstruction line 123
  13. theorem OAI.TamingCompatibility.GeometricHilbert.scalarCorrection_logShell_estimates line 166
  14. theorem OAI.TamingCompatibility.GeometricHilbert.scalarCorrection_logInner_estimates line 211
  15. theorem OAI.TamingCompatibility.GeometricHilbert.scalarCorrection_sqrtShell_estimates line 256
  16. theorem OAI.TamingCompatibility.GeometricHilbert.scalarCorrection_sqrtInner_estimates line 298