OAI/NumberTheory/CubicMoment/Theta/CubicThetaLocalOperator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Locality and finite additivity of the actual hyperbolic operator for twice continuously differentiable functions.

  1. lemma OAI.CubicFirstMoment.cubicThetaHyperbolicOperator_germ line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaHyperbolicOperator_finite line 31