OAI/Combinatorics/SumProduct/Alignment/RawHarmonic01.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DyadicHarmonicBoundary.raw_bad_bound line 16
  2. theorem OAI.DyadicHarmonicBoundary.raw_bad_bound_simple line 46
  3. theorem OAI.DyadicHarmonicBoundary.raw_bad_tendsto line 61
  4. def OAI.AdmissibleMicrocellBoundary.earlierScale line 91
  5. lemma OAI.AdmissibleMicrocellBoundary.scale_one line 93
  6. lemma OAI.AdmissibleMicrocellBoundary.radius_four_modulus line 99
  7. theorem OAI.AdmissibleMicrocellBoundary.enlarged_rates line 118
  8. theorem OAI.AdmissibleMicrocellBoundary.uniform_raw_boundary line 139
  9. def OAI.RawHarmonicProbability.units line 192
  10. lemma OAI.RawHarmonicProbability.mass_units line 194
  11. lemma OAI.RawHarmonicProbability.units_pos line 197
  12. lemma OAI.RawHarmonicProbability.mass_pos line 200
  13. lemma OAI.RawHarmonicProbability.units_nonempty line 207
  14. def OAI.RawHarmonicProbability.law line 215
  15. lemma OAI.RawHarmonicProbability.law_apply line 220
  16. lemma OAI.RawHarmonicProbability.boundary_law line 238
  17. theorem OAI.RawHarmonicProbability.finite_boundary_bound line 250
  18. theorem OAI.RawHarmonicProbability.admissible_finite_boundary line 263