OAI/NumberTheory/CubicMoment/Theta/CubicThetaC1EnergySums.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite sums of compact C1 sections preserve their actual value-gradient data. This permits finite reconstruction from chart pieces.

  1. lemma OAI.CubicFirstMoment.cubicThetaCompactSection_add line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaC1EnergyData_add line 28
  3. lemma OAI.CubicFirstMoment.cubicThetaSectionFunction_sum line 44
  4. lemma OAI.CubicFirstMoment.cubicThetaC1Section_sum line 49
  5. lemma OAI.CubicFirstMoment.cubicThetaCompactSection_sum line 55
  6. lemma OAI.CubicFirstMoment.cubicThetaC1EnergyData_sum line 71