OAI/NumberTheory/JointDickman/Probability/TensorCutoff.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Smooth separated factors for compact polynomial approximation

  1. def OAI.JointDickman.tensorBoxBump line 13
  2. theorem OAI.JointDickman.tensorBoxBump_one line 19
  3. theorem OAI.JointDickman.tensorBoxBump_zero line 25
  4. def OAI.JointDickman.tensorPowerFactor line 35
  5. theorem OAI.JointDickman.tensorPowerFactor_apply line 39
  6. theorem OAI.JointDickman.tensorPowerFactor_support line 42
  7. theorem OAI.JointDickman.schwartz_value_derivative_bounds line 45
  8. theorem OAI.JointDickman.tensor_polynomial_expansion line 58