OAI/NumberTheory/CubicMoment/Theta/CubicThetaWindowWeak.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The exact compact-window weak equation connects the low forcing with the high cusp observation of every actual spectral residue.

  1. def OAI.CubicFirstMoment.cubicThetaWindowForcingSection line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaWindowForcingSection_compact line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaWindowForcingL2 line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaWindow_coordinate_equation line 29
  5. theorem OAI.CubicFirstMoment.cubicThetaWindow_global_weak line 49
  6. lemma OAI.CubicFirstMoment.cubicThetaWindow_forcing_balance line 60
  7. lemma OAI.CubicFirstMoment.cubicThetaResidue_forcing_orthogonal_closed line 80
  8. lemma OAI.CubicFirstMoment.cubicThetaResidue_forcing_orthogonal line 88