OAI/Analysis/PlanarPacking/DataSplit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fixed and summable parts of cardinal data

Splitting cardinal data separates the fixed coefficients from the absolutely summable interpolation unknowns.

  1. def OAI.SharpPlanar.fixedPart line 13
  2. lemma OAI.SharpPlanar.density_split line 14
  3. lemma OAI.SharpPlanar.K_split line 18
  4. lemma OAI.SharpPlanar.K_fixed₁ line 36
  5. lemma OAI.SharpPlanar.K_fixed₂ line 38
  6. lemma OAI.SharpPlanar.transformedJets_fixed₁ line 40
  7. lemma OAI.SharpPlanar.transformedJets_fixed₂ line 47