OAI/Analysis/PlanarPacking/FiniteU.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exterior coupling in the finite interpolation system

Column estimates control the coupling between the central and exterior coordinates.

  1. def OAI.SharpPlanar.Numerical.Umat line 63
  2. lemma OAI.SharpPlanar.Numerical.WUplus_column line 64
  3. lemma OAI.SharpPlanar.Numerical.WUplus_norm line 163
  4. lemma OAI.SharpPlanar.Numerical.inversePlus_U_norm line 166
  5. lemma OAI.SharpPlanar.Numerical.WUminus_column line 173
  6. lemma OAI.SharpPlanar.Numerical.WUminus_norm line 272
  7. lemma OAI.SharpPlanar.Numerical.inverseMinus_U_norm line 275