OAI/Probability/SpanningForest/InnovationPhaseRecurrence.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.InnovationPhaseRecurrence.phaseOn line 12
  2. lemma OAI.Problem336.InnovationPhaseRecurrence.norm_phaseOn_le_one line 15
  3. lemma OAI.Problem336.InnovationPhaseRecurrence.measurable_phaseOn line 23
  4. lemma OAI.Problem336.InnovationPhaseRecurrence.phaseOn_mul_increment line 29
  5. lemma OAI.Problem336.InnovationPhaseRecurrence.integral_phaseOn_self line 41
  6. lemma OAI.Problem336.InnovationPhaseRecurrence.integral_phaseOn_eq_setIntegral line 46
  7. lemma OAI.Problem336.InnovationPhaseRecurrence.phase_recurrence_of_weighted_step line 52
  8. theorem OAI.Problem336.InnovationPhaseRecurrence.restricted_characteristic_of_phase_steps line 61
  9. theorem OAI.Problem336.InnovationPhaseRecurrence.restricted_characteristic_of_bounded_test_steps line 92
  10. theorem OAI.Problem336.InnovationPhaseRecurrence.restricted_characteristic_of_adapted_bounded_test_steps line 120
  11. def OAI.Problem336.InnovationPhaseRecurrence.timeGrid line 143
  12. lemma OAI.Problem336.InnovationPhaseRecurrence.timeGrid_zero line 146
  13. lemma OAI.Problem336.InnovationPhaseRecurrence.timeGrid_finish line 149
  14. lemma OAI.Problem336.InnovationPhaseRecurrence.timeGrid_mono line 153
  15. lemma OAI.Problem336.InnovationPhaseRecurrence.le_timeGrid line 158
  16. lemma OAI.Problem336.InnovationPhaseRecurrence.timeGrid_le_finish line 161
  17. lemma OAI.Problem336.InnovationPhaseRecurrence.timeGrid_succ_sub line 165
  18. theorem OAI.Problem336.InnovationPhaseRecurrence.restricted_characteristic_of_local_bounded_test_bound line 172