OAI/Analysis/PlanarPacking/RationalBounds.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Rational Fourier envelopes

Explicit rational majorants control the direct and transformed spectral envelopes at integral and half-integral radii.

  1. def OAI.SharpPlanar.piUpper line 16
  2. lemma OAI.SharpPlanar.piUpper_pos line 17
  3. lemma OAI.SharpPlanar.pi_le_upper line 18
  4. def OAI.SharpPlanar.pieceIntCap line 19
  5. def OAI.SharpPlanar.atomIntCap line 21
  6. lemma OAI.SharpPlanar.pieceIntCap_nonneg line 23
  7. lemma OAI.SharpPlanar.atomIntCap_nonneg line 25
  8. lemma OAI.SharpPlanar.pieceL_le_intCap line 27
  9. lemma OAI.SharpPlanar.atomL_le_intCap line 31
  10. def OAI.SharpPlanar.directRational line 34
  11. def OAI.SharpPlanar.transformRational line 36
  12. def OAI.SharpPlanar.atomicRational line 38
  13. lemma OAI.SharpPlanar.directEnvelope_le_rat line 40
  14. lemma OAI.SharpPlanar.transformEnvelope_le_rat line 46
  15. lemma OAI.SharpPlanar.atomicEnvelope_le_rat line 53
  16. def OAI.SharpPlanar.taylorEnvelope line 60
  17. def OAI.SharpPlanar.halfBase line 62
  18. lemma OAI.SharpPlanar.halfBase_pos line 63
  19. lemma OAI.SharpPlanar.halfBase_contains line 64
  20. def OAI.SharpPlanar.halfMass line 73
  21. lemma OAI.SharpPlanar.halfMass_nonneg line 75
  22. lemma OAI.SharpPlanar.pieceMass_half line 77
  23. def OAI.SharpPlanar.halfCap line 87
  24. lemma OAI.SharpPlanar.pieceL_half line 88
  25. def OAI.SharpPlanar.halfTransform line 95
  26. lemma OAI.SharpPlanar.transformEnvelope_le_half line 97