OAI/NumberTheory/CubicMoment/Theta/CubicThetaFiniteEnergySections.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual C1 sections of finite value and gradient energy form a complex vector space. This retains their literal pointwise functions.

  1. def OAI.CubicFirstMoment.cubicThetaFiniteEnergySections line 12
  2. def OAI.CubicFirstMoment.cubicThetaFiniteEnergyValue line 37
  3. def OAI.CubicFirstMoment.cubicThetaFiniteEnergyGradient line 42
  4. def OAI.CubicFirstMoment.cubicThetaFiniteEnergyEmbedding line 60
  5. lemma OAI.CubicFirstMoment.cubicThetaFiniteEnergyEmbedding_value line 66
  6. lemma OAI.CubicFirstMoment.cubicThetaFiniteEnergyEmbedding_gradient line 69
  7. lemma OAI.CubicFirstMoment.cubicThetaSmoothTests_finiteEnergy line 72
  8. def OAI.CubicFirstMoment.cubicThetaSmoothToFiniteEnergy line 77
  9. lemma OAI.CubicFirstMoment.cubicThetaFiniteEnergyEmbedding_smooth line 80