OAI/Analysis/PlanarPacking/FiniteInverse.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Inverse bounds for the central interpolation block

Exact rational approximate inverses give bounds for the two central blocks.

  1. lemma OAI.SharpPlanar.Numerical.defectplus_norm line 13
  2. lemma OAI.SharpPlanar.Numerical.defectminus_norm line 17
  3. lemma OAI.SharpPlanar.Numerical.Wplus_norm line 21
  4. lemma OAI.SharpPlanar.Numerical.Wminus_norm line 22
  5. lemma OAI.SharpPlanar.Numerical.defectplus_lt_one line 23
  6. lemma OAI.SharpPlanar.Numerical.defectminus_lt_one line 25
  7. def OAI.SharpPlanar.Numerical.inversePlusEquiv line 27
  8. def OAI.SharpPlanar.Numerical.inverseMinusEquiv line 29
  9. lemma OAI.SharpPlanar.Numerical.inversePlus_apply line 31
  10. lemma OAI.SharpPlanar.Numerical.inverseMinus_apply line 34
  11. lemma OAI.SharpPlanar.Numerical.inversePlus_norm line 37
  12. lemma OAI.SharpPlanar.Numerical.inverseMinus_norm line 44