OAI/MathematicalPhysics/CriticalSK/MixingMeasurability.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.generator_continuous line 10
  2. lemma OAI.CriticalSK.discreteKernel_continuous line 18
  3. lemma OAI.CriticalSK.continuousKernel_continuous line 27
  4. lemma OAI.CriticalSK.continuousKernel_time_continuous line 38
  5. lemma OAI.CriticalSK.continuousDistance_continuous line 43
  6. lemma OAI.CriticalSK.discreteDistance_continuous line 52
  7. lemma OAI.CriticalSK.continuousDistance_time_continuous line 61
  8. lemma OAI.CriticalSK.continuousMixingAt_mem line 70
  9. lemma OAI.CriticalSK.continuousMixingAt_le_iff line 80
  10. lemma OAI.CriticalSK.discreteMixingAt_le_iff line 90
  11. lemma OAI.CriticalSK.continuousMixingAt_measurable line 101
  12. lemma OAI.CriticalSK.discreteMixingAt_measurable line 114