OAI/NumberTheory/CubicMoment/Angular/AngularLatticeProfile.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual angular annulus is a smooth compactly supported plane function. Its area integral is zero in every nonzero integral mode.

  1. def OAI.CubicFirstMoment.angularPlanePhase line 14
  2. def OAI.CubicFirstMoment.angularAnnulus line 16
  3. lemma OAI.CubicFirstMoment.angularPlanePhase_mul line 19
  4. lemma OAI.CubicFirstMoment.angularPlanePhase_coe line 24
  5. lemma OAI.CubicFirstMoment.angularPlanePhase_contDiffAt line 27
  6. lemma OAI.CubicFirstMoment.angularAnnulus_compact line 40
  7. lemma OAI.CubicFirstMoment.angularAnnulus_smooth line 46
  8. def OAI.CubicFirstMoment.angularAnnulusSchwartz line 65
  9. lemma OAI.CubicFirstMoment.angularAnnulus_rotation line 69
  10. lemma OAI.CubicFirstMoment.exists_angular_sign_rotation line 75
  11. theorem OAI.CubicFirstMoment.integral_angularAnnulus_eq_zero line 90

    Source documentation

    Continuous rotational symmetry kills the area term; the discrete primary-lattice sum itself need not vanish.

    theorem integral_angularAnnulus_eq_zero {ℓ : ℤ} (hℓ : ℓ ≠ 0) (W : ℝ → ℂ) :
    (∫ z : ℂ, angularAnnulus ℓ W z) = 0 := by
…

    Mentions: OAI.CubicFirstMoment.angularAnnulus