OAI/Probability/ContinuumTransition/FreeFamily.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ContinuumTemperature.measurableSet_freeConfig line 11
  2. def OAI.ContinuumTemperature.freeFamily line 31
  3. lemma OAI.ContinuumTemperature.freeFamily_relabel line 34
  4. lemma OAI.ContinuumTemperature.freeFamily_measurable line 46
  5. lemma OAI.ContinuumTemperature.freeFamily_nonneg line 49
  6. lemma OAI.ContinuumTemperature.freeFamily_le_exp line 54
  7. lemma OAI.ContinuumTemperature.freeFamily_summable line 61
  8. lemma OAI.ContinuumTemperature.rootCover_volume_real line 65
  9. lemma OAI.ContinuumTemperature.freeConfig_volume_le line 76