OAI/Analysis/PlanarPacking/FiniteTail.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Tails of the interpolation operator

Coordinate projections and shell estimates bound the tails of the interpolation operator.

  1. def OAI.SharpPlanar.tailScalar line 15
  2. lemma OAI.SharpPlanar.tailScalar_summable line 17
  3. lemma OAI.SharpPlanar.tailScalar_eq line 22
  4. lemma OAI.SharpPlanar.rowTailNorm_nonneg line 31
  5. lemma OAI.SharpPlanar.rowTailNorm_zero line 33
  6. lemma OAI.SharpPlanar.finiteRestriction_tail line 41
  7. lemma OAI.SharpPlanar.norm_S_le line 48
  8. lemma OAI.SharpPlanar.Numerical.exterior_low_tail line 56
  9. lemma OAI.SharpPlanar.Numerical.compressed_low_L line 81
  10. lemma OAI.SharpPlanar.Numerical.exterior_central_norm line 84
  11. lemma OAI.SharpPlanar.Numerical.exterior_exterior_norm line 98
  12. lemma OAI.SharpPlanar.Numerical.finite_discard_norm line 106
  13. lemma OAI.SharpPlanar.Numerical.finite_discard_S line 116