OAI/Analysis/LipschitzHilbert/Trees/SourceFiniteThresholdLevels.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A finite collection has a dyadic level below all its positive densities, and a level above any prescribed initial size or density.

  1. theorem OAI.LipschitzHilbert.finite_positive_lower_bound line 10
  2. theorem OAI.LipschitzHilbert.exists_dyadic_zero_detection line 29
  3. theorem OAI.LipschitzHilbert.exists_dyadic_upper_level line 39