OAI/Combinatorics/ThinTrees/Metric/Numerator.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Metric numerator.

  1. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.diagonal_sq_le line 21
  2. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.positive_bad_bound line 29
  3. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.weighted_boundary_sum line 95
  4. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.hierarchy_numerator_bound line 118
  5. lemma OAI.AlgorithmicThinTrees.MetricProfiles.squared_euclidean_numerator_bound line 203
  6. theorem OAI.AlgorithmicThinTrees.MetricProfiles.polynomial_metric_numerator line 232