OAI/Analysis/CircleDomains/Rigidity/SmoothTraceTruncation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Smooth scalar truncations vanish near the zero trace and converge to positive inputs with a derivative bound independent of the scale.

  1. def OAI.CircleDomainRigidity.smoothTraceTruncation line 14
  2. theorem OAI.CircleDomainRigidity.smoothTraceTruncation_contDiff line 17
  3. theorem OAI.CircleDomainRigidity.smoothTraceTruncation_zero line 22
  4. theorem OAI.CircleDomainRigidity.smoothTraceTruncation_eq_self line 29
  5. theorem OAI.CircleDomainRigidity.smoothTransition_deriv_zero_left line 36
  6. theorem OAI.CircleDomainRigidity.smoothTransition_deriv_zero_right line 44
  7. theorem OAI.CircleDomainRigidity.smoothTraceTruncation_deriv line 52
  8. theorem OAI.CircleDomainRigidity.smoothTraceTruncation_deriv_zero line 63
  9. theorem OAI.CircleDomainRigidity.smoothTraceTruncation_deriv_one line 70
  10. theorem OAI.CircleDomainRigidity.smoothTraceTruncation_mem line 79
  11. theorem OAI.CircleDomainRigidity.smoothTraceTruncation_uniform_deriv_bound line 84