OAI/Analysis/PlanarPacking/SignBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Scalar sign margins

Rational bounds for coefficient perturbations and Taylor remainders on half-gaps.

  1. lemma OAI.SharpPlanar.perturbation_zero_cap line 14
  2. lemma OAI.SharpPlanar.perturbation_one_cap line 17
  3. lemma OAI.SharpPlanar.perturbation_two_cap line 20
  4. lemma OAI.SharpPlanar.perturbation_large_cap line 23
  5. lemma OAI.SharpPlanar.taylor_cap0 line 26
  6. lemma OAI.SharpPlanar.taylor_cap1 line 30
  7. lemma OAI.SharpPlanar.taylor_cap2 line 34
  8. lemma OAI.SharpPlanar.taylor_cap3 line 38
  9. lemma OAI.SharpPlanar.taylor_cap4 line 42
  10. lemma OAI.SharpPlanar.taylor_cap5 line 46
  11. lemma OAI.SharpPlanar.taylor_cap6 line 50
  12. lemma OAI.SharpPlanar.taylor_cap7 line 54