OAI/Probability/Ballisticity/Estimates/RawPairLocality.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.variableHitKernel line 14
  2. instance OAI.DirectionalTransience.variableHitKernel_finite line 20
  3. def OAI.DirectionalTransience.variablePairHitKernel line 27
  4. instance OAI.DirectionalTransience.variablePairHitKernel_finite line 32
  5. lemma OAI.DirectionalTransience.variablePairHitKernel_apply line 35
  6. lemma OAI.DirectionalTransience.rawPairEndpointLaw_rows line 41
  7. lemma OAI.DirectionalTransience.rawPairEndpointLaw_total_le_one line 63
  8. def OAI.DirectionalTransience.pairKernelMass line 71
  9. lemma OAI.DirectionalTransience.measurable_pairKernelMass line 75
  10. lemma OAI.DirectionalTransience.pairKernelMass_le_one line 100
  11. lemma OAI.DirectionalTransience.pairKernelMass_toReal line 110
  12. lemma OAI.DirectionalTransience.pairKernelMass_lower_iff line 123
  13. abbrev OAI.DirectionalTransience.SupportedPairMeasures line 132
  14. lemma OAI.DirectionalTransience.supportedPairMeasures_singleton line 135
  15. lemma OAI.DirectionalTransience.pairKernelMass_joint_rows line 142