OAI/Geometry/RCD/Coordinates/NormalizedPositiveWeights.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Common minorization of normalized positive kernel rows

Uniform lower and upper kernel bounds give a strict loss in the oscillation of weighted means, independently of the positive base weight.

  1. theorem OAI.RegularPointCoordinates.normalized_weight_lower line 15
  2. theorem OAI.RegularPointCoordinates.normalized_positive_weights_difference line 27