OAI/Geometry/TamingCompatibility/DifferentialForms/RadialGradientBridge.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.RadialPotential.logGradientProfile line 18
  2. def OAI.TamingCompatibility.RadialPotential.sqrtGradientProfile line 20
  3. lemma OAI.TamingCompatibility.RadialPotential.logGradientProfile_eq_fderiv line 23
  4. lemma OAI.TamingCompatibility.RadialPotential.sqrtGradientProfile_eq_fderiv line 27
  5. lemma OAI.TamingCompatibility.RadialPotential.logGradientProfile_joint_smooth_at line 32
  6. lemma OAI.TamingCompatibility.RadialPotential.sqrtGradientProfile_joint_smooth_at line 40
  7. lemma OAI.TamingCompatibility.RadialPotential.cutoff_log_gradient_derivatives_bounded line 48
  8. lemma OAI.TamingCompatibility.RadialPotential.cutoff_sqrt_gradient_derivatives_bounded line 59
  9. lemma OAI.TamingCompatibility.RadialPotential.logGradientProfile_scale line 70
  10. lemma OAI.TamingCompatibility.RadialPotential.sqrtGradientProfile_scale line 76
  11. def OAI.TamingCompatibility.RadialPotential.unitCutoff line 96
  12. def OAI.TamingCompatibility.RadialPotential.scaledCutoff line 98
  13. def OAI.TamingCompatibility.RadialPotential.shellCutoff line 100
  14. lemma OAI.TamingCompatibility.RadialPotential.unitCutoff_smooth line 102
  15. lemma OAI.TamingCompatibility.RadialPotential.unitCutoff_one line 105
  16. lemma OAI.TamingCompatibility.RadialPotential.unitCutoff_zero line 109
  17. lemma OAI.TamingCompatibility.RadialPotential.unitCutoff_nonneg line 113
  18. lemma OAI.TamingCompatibility.RadialPotential.unitCutoff_le_one line 114
  19. lemma OAI.TamingCompatibility.RadialPotential.scaledCutoff_smooth line 116
  20. lemma OAI.TamingCompatibility.RadialPotential.scaledCutoff_one line 119
  21. lemma OAI.TamingCompatibility.RadialPotential.scaledCutoff_zero line 125
  22. lemma OAI.TamingCompatibility.RadialPotential.scaledCutoff_nonneg line 131
  23. lemma OAI.TamingCompatibility.RadialPotential.scaledCutoff_le_one line 132
  24. lemma OAI.TamingCompatibility.RadialPotential.scaledCutoff_tsupport line 134
  25. lemma OAI.TamingCompatibility.RadialPotential.scaledCutoff_compact line 142
  26. lemma OAI.TamingCompatibility.RadialPotential.shellCutoff_smooth line 146
  27. lemma OAI.TamingCompatibility.RadialPotential.shellCutoff_zero_inner line 149
  28. lemma OAI.TamingCompatibility.RadialPotential.shellCutoff_tsupport line 154
  29. lemma OAI.TamingCompatibility.RadialPotential.shellCutoff_compact line 170
  30. lemma OAI.TamingCompatibility.RadialPotential.shellCutoff_abs_le_one line 175
  31. lemma OAI.TamingCompatibility.RadialPotential.scaledCutoff_scale line 181
  32. lemma OAI.TamingCompatibility.RadialPotential.shellCutoff_scale line 188
  33. lemma OAI.TamingCompatibility.RadialPotential.dyadic_cutoff_telescope line 195
  34. def OAI.TamingCompatibility.RadialPotential.sourcePiece line 208
  35. lemma OAI.TamingCompatibility.RadialPotential.source_finite_reconstruction line 210
  36. lemma OAI.TamingCompatibility.RadialPotential.exists_dyadic_reconstruction_scale line 223
  37. lemma OAI.TamingCompatibility.RadialPotential.map_source_finite_reconstruction line 228