OAI/NumberTheory/CubicMoment/Theta/CubicThetaLocalEnergyJet.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual local hyperbolic energy jets: the value has weight v^(-3/2), and each Euclidean derivative has weight v^(-1/2). Their squared norm is the hyperbolic mass plus Dirichlet density.

  1. abbrev OAI.CubicFirstMoment.CubicThetaLocalJet line 14
  2. def OAI.CubicFirstMoment.cubicThetaLocalEnergyJet line 16
  3. lemma OAI.CubicFirstMoment.cubicTheta_weighted_positive_continuous line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaLocalEnergyJet_continuous line 31
  5. lemma OAI.CubicFirstMoment.cubicThetaLocalEnergyJet_compact line 47
  6. lemma OAI.CubicFirstMoment.cubicThetaLocalEnergyJet_memLp line 58
  7. lemma OAI.CubicFirstMoment.cubicThetaLocalEnergyJet_norm_sq line 65