OAI/Analysis/CircleDomains/Sobolev/RescaledScalarBump.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The fixed scalar cutoff translated to a level and rescaled to its band width, with its exact derivative and support.

  1. def OAI.CircleDomainRigidity.rescaledScalarBump line 12
  2. lemma OAI.CircleDomainRigidity.rescaledScalarBump_contDiff line 15
  3. lemma OAI.CircleDomainRigidity.rescaledScalarBump_deriv line 19
  4. lemma OAI.CircleDomainRigidity.rescaledScalarBump_unit line 29
  5. lemma OAI.CircleDomainRigidity.rescaledScalarBump_one line 32
  6. lemma OAI.CircleDomainRigidity.rescaledScalarBump_zero line 38
  7. lemma OAI.CircleDomainRigidity.rescaledScalarBump_deriv_bound line 46