OAI/Combinatorics/ThinTrees/Metric/ScaleCharging.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Metric scale charging.

  1. structure OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CompactPackage line 17
  2. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CompactPackage.mass line 24
  3. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CompactPackage.finite_bound line 26
  4. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CompactPackage.ordered_bound line 51
  5. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedBag.weaken line 70
  6. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedFamily.weaken line 76
  7. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.mass_eq line 88
  8. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.geometric_of_pairwise line 93
  9. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.ratios_of_mem line 103
  10. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.fresh_of_pairwise line 109
  11. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.finite_bound line 119
  12. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.AssignedSequence.ordered_bound line 136
  13. abbrev OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CapturedFamily line 165
  14. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CapturedFamily.radius line 170
  15. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CapturedFamily.upper line 173
  16. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CapturedFamily.mass line 176
  17. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CapturedFamily.owners line 179
  18. def OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CapturedFamily.Ratio line 183
  19. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CapturedFamily.mass_nonneg line 188
  20. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CapturedFamily.mixed_bound line 193
  21. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.CapturedFamily.scale_bound line 271
  22. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.capturePackage line 326
  23. lemma OAI.AlgorithmicThinTrees.MetricProfiles.AssignedGeometry.homogeneous_scale_bound line 375