OAI/NumberTheory/CubicMoment/Theta/CubicThetaC1Localization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Localize a C1 section by one actual arithmetic core profile. The periodized result is its scalar bump cutoff and lies in the energy graph.

  1. lemma OAI.CubicFirstMoment.cubicThetaC1Localization_regular line 14
  2. def OAI.CubicFirstMoment.cubicThetaC1CoreFunction line 29
  3. lemma OAI.CubicFirstMoment.cubicThetaC1CoreFunction_support line 32
  4. lemma OAI.CubicFirstMoment.cubicThetaC1CoreFunction_compact line 36
  5. lemma OAI.CubicFirstMoment.cubicThetaC1CoreFunction_regular line 39
  6. def OAI.CubicFirstMoment.cubicThetaCoreSquare line 46
  7. lemma OAI.CubicFirstMoment.cubicThetaC1CoreFunction_periodization line 50
  8. lemma OAI.CubicFirstMoment.cubicThetaC1CoreFunction_mem_energy line 81