OAI/Analysis/PlanarPacking/OriginPositive.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Positivity at the origin of the exact Fourier pair

  1. lemma OAI.SharpPlanar.exactJet_zero_H₁ line 13
  2. lemma OAI.SharpPlanar.exactJet_zero_H₂ line 15
  3. lemma OAI.SharpPlanar.tableOrigin_lower line 17
  4. lemma OAI.SharpPlanar.exactRight_origin_positive line 21
  5. lemma OAI.SharpPlanar.exactLeft_origin_positive line 29