OAI/Combinatorics/ThinTrees/Metric/BagExtraction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Metric bag extraction.

  1. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.distance_balls_disjoint line 18
  2. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.separated_net line 32
  3. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.compact_from_net line 80
  4. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.normalized_small_balls line 184
  5. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.assigned_from_net line 261
  6. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.capture_small_balls line 353
  7. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.density_spectral_input line 425
  8. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.homogeneous_family line 446