OAI/Analysis/PlanarPacking/FiniteProjection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite coordinate projections

Restriction and extension identify the first shell coordinates with a finite subspace of the absolutely summable interpolation space.

  1. lemma OAI.SharpPlanar.finiteProjection_apply line 18
  2. abbrev OAI.SharpPlanar.Numerical.RJ line 34
  3. abbrev OAI.SharpPlanar.Numerical.IJ line 35
  4. abbrev OAI.SharpPlanar.Numerical.RE line 36
  5. abbrev OAI.SharpPlanar.Numerical.IE line 37
  6. abbrev OAI.SharpPlanar.Numerical.RF line 38
  7. abbrev OAI.SharpPlanar.Numerical.IF line 39
  8. abbrev OAI.SharpPlanar.Numerical.RL line 40
  9. abbrev OAI.SharpPlanar.Numerical.IL line 41