OAI/Analysis/LipschitzFree/AffineWeights.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Affine signed coefficients and quantitative pairing bounds

  1. def OAI.DiscreteFree.affineWeights line 19
  2. theorem OAI.DiscreteFree.affineWeights_mass line 23
  3. theorem OAI.DiscreteFree.affineWeights_pairing line 27
  4. theorem OAI.DiscreteFree.affineWeights_variation line 45
  5. theorem OAI.DiscreteFree.affineWeights_operator_variation line 74
  6. theorem OAI.DiscreteFree.affine_difference_bound line 92