OAI/Probability/Ballisticity/Estimates/ObservedCharges.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.observerShrinkEvent line 15
  2. lemma OAI.DirectionalTransience.measurableSet_observerShrinkEvent line 20
  3. def OAI.DirectionalTransience.observedCharge line 29
  4. lemma OAI.DirectionalTransience.measurable_observedCharge line 37
  5. lemma OAI.DirectionalTransience.observedCharge_mean line 61
  6. lemma OAI.DirectionalTransience.observedCharge_mean_le line 89
  7. lemma OAI.DirectionalTransience.commonLayer_before_selected_bound line 141
  8. def OAI.DirectionalTransience.allocatedSmallCuts line 195
  9. lemma OAI.DirectionalTransience.allocatedSmallCuts_card_le line 201
  10. lemma OAI.DirectionalTransience.allocatedSmallCuts_nonempty_shrink line 217
  11. lemma OAI.DirectionalTransience.allocatedSmallCuts_le_charge line 241