OAI/Analysis/LipschitzFree/LabelBumps.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Lipschitz label bumps and affine mass estimates

  1. def OAI.DiscreteFree.labelBump line 17
  2. theorem OAI.DiscreteFree.labelBump_nonneg line 21
  3. theorem OAI.DiscreteFree.labelBump_le line 25
  4. theorem OAI.DiscreteFree.labelBump_self line 32
  5. theorem OAI.DiscreteFree.labelBump_sub line 35
  6. theorem OAI.DiscreteFree.labelBump_lipschitz line 51
  7. theorem OAI.DiscreteFree.labelBump_positive line 61
  8. theorem OAI.DiscreteFree.affine_bump_mass line 73