OAI/Analysis/PlanarPacking/FiniteFull.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The finite interpolation system

Schur complements give existence, uniqueness and norm bounds for the finite system.

  1. def OAI.SharpPlanar.Numerical.signedS line 16
  2. def OAI.SharpPlanar.Numerical.centralV line 17
  3. def OAI.SharpPlanar.Numerical.signedU line 19
  4. def OAI.SharpPlanar.Numerical.signedL line 20
  5. def OAI.SharpPlanar.Numerical.signedE line 21
  6. def OAI.SharpPlanar.Numerical.finiteA line 22
  7. lemma OAI.SharpPlanar.Numerical.compressed_D line 24
  8. lemma OAI.SharpPlanar.Numerical.compressed_U line 26
  9. lemma OAI.SharpPlanar.Numerical.centralV_norm line 28
  10. lemma OAI.SharpPlanar.Numerical.signedVU_norm line 32
  11. lemma OAI.SharpPlanar.Numerical.signedL_norm line 37
  12. lemma OAI.SharpPlanar.Numerical.signedE_norm line 40
  13. lemma OAI.SharpPlanar.Numerical.signedS_norm line 43
  14. lemma OAI.SharpPlanar.Numerical.centralV_left line 45
  15. lemma OAI.SharpPlanar.Numerical.finiteA_left line 64
  16. lemma OAI.SharpPlanar.Numerical.finiteA_right line 74
  17. lemma OAI.SharpPlanar.Numerical.finiteA_coercive line 84
  18. lemma OAI.SharpPlanar.Numerical.finiteA_bijective line 90
  19. def OAI.SharpPlanar.Numerical.finiteEquiv line 97
  20. def OAI.SharpPlanar.Numerical.finiteV line 99
  21. lemma OAI.SharpPlanar.Numerical.finiteV_norm line 101
  22. lemma OAI.SharpPlanar.Numerical.finiteV_left line 107
  23. lemma OAI.SharpPlanar.Numerical.finiteV_right line 110
  24. lemma OAI.SharpPlanar.Numerical.signed_discard line 113
  25. lemma OAI.SharpPlanar.Numerical.signed_discard_norm line 120
  26. theorem OAI.SharpPlanar.Numerical.interpolation_exists_unique line 126
  27. theorem OAI.SharpPlanar.Numerical.interpolation_norm_bound line 130