OAI/Analysis/PlanarPacking/CoupledFull.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The coupled interpolation system

The finite inverse and tail estimates solve the interpolation equations in the space of absolutely summable coefficients.

  1. def OAI.SharpPlanar.interpolationInverse line 14
  2. lemma OAI.SharpPlanar.interpolationInverse_eq line 16
  3. lemma OAI.SharpPlanar.interpolationInverse_unique line 19
  4. def OAI.SharpPlanar.coupledLeft line 22
  5. def OAI.SharpPlanar.coupledRight line 24
  6. lemma OAI.SharpPlanar.coupled_equations line 26
  7. lemma OAI.SharpPlanar.coupled_unique line 40
  8. theorem OAI.SharpPlanar.coupled_exists_unique line 57