OAI/NumberTheory/CubicMoment/Angular/AngularPowerWeights.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed real powers preserve the actual positive annular weight family. The smooth extension used in the proof agrees with the power wherever the original weight is nonzero.

  1. def OAI.CubicFirstMoment.UniformLogWeights.realPower line 13
  2. theorem OAI.CubicFirstMoment.LogarithmicWeightFamily.power_lattice_bound line 43