OAI/Analysis/PlanarPacking/FiniteSplit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite decompositions of ℓ¹ coordinates

The central and exterior coordinate blocks give an additive decomposition of the ℓ¹ norm.

  1. def OAI.SharpPlanar.l1Left line 16
  2. def OAI.SharpPlanar.l1Right line 18
  3. lemma OAI.SharpPlanar.l1Left_apply line 20
  4. lemma OAI.SharpPlanar.l1Right_apply line 21
  5. lemma OAI.SharpPlanar.l1Split_norm line 22
  6. lemma OAI.SharpPlanar.Numerical.finiteEmbedding_split line 30
  7. lemma OAI.SharpPlanar.Numerical.finiteRestriction_left line 41
  8. lemma OAI.SharpPlanar.Numerical.finiteRestriction_right line 44