OAI/Combinatorics/SumProduct/Alignment/DyadicHarmonic01.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UnitNeighborhoodCost.cover_count line 26
  2. theorem OAI.UnitNeighborhoodCost.harmonic_cover line 40
  3. def OAI.MicrocellBoundary.bad line 82
  4. lemma OAI.MicrocellBoundary.cover line 85
  5. theorem OAI.MicrocellBoundary.stable line 108
  6. theorem OAI.MicrocellBoundary.harmonic_bad_bound line 119
  7. def OAI.DyadicHarmonicBoundary.mass line 153
  8. def OAI.DyadicHarmonicBoundary.badMass line 154
  9. lemma OAI.DyadicHarmonicBoundary.mass_units line 157
  10. lemma OAI.DyadicHarmonicBoundary.badMass_units line 159
  11. lemma OAI.DyadicHarmonicBoundary.mass_nonneg line 163
  12. lemma OAI.DyadicHarmonicBoundary.badMass_nonneg line 164
  13. lemma OAI.DyadicHarmonicBoundary.mass_mono line 166
  14. lemma OAI.DyadicHarmonicBoundary.badMass_mono line 168
  15. lemma OAI.DyadicHarmonicBoundary.dyadic_lower line 171
  16. lemma OAI.DyadicHarmonicBoundary.dyadic_upper line 189
  17. lemma OAI.DyadicHarmonicBoundary.dyadic_sum line 202
  18. theorem OAI.DyadicHarmonicBoundary.dyadic_transfer line 217