OAI/Analysis/LipschitzHilbert/Estimates/GeometricScaleWeights.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform row and column bounds for the actual geometric scale kernel.

  1. theorem OAI.LipschitzHilbert.sum_half_powers_le_two line 14
  2. theorem OAI.LipschitzHilbert.sum_half_distance_le_four line 24
  3. def OAI.LipschitzHilbert.scaleWeight line 79
  4. theorem OAI.LipschitzHilbert.scaleWeight_pos line 81
  5. theorem OAI.LipschitzHilbert.scaleWeight_sum line 85
  6. theorem OAI.LipschitzHilbert.scaleWeight_sum_column line 89