OAI/Probability/Ballisticity/RowBridge.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.DirectionalTransience.RowBridge.toRealline 13 - lemma
OAI.DirectionalTransience.RowBridge.measurable_toRealline 22 - def
OAI.DirectionalTransience.RowBridge.rowLawline 27 - instance
OAI.DirectionalTransience.RowBridge.rowLaw_probabilityline 30 - def
OAI.DirectionalTransience.RowBridge.environmentline 34 - lemma
OAI.DirectionalTransience.RowBridge.measurable_environmentline 37 - lemma
OAI.DirectionalTransience.RowBridge.environmentLaw_mapline 40 - lemma
OAI.DirectionalTransience.RowBridge.strictEllipticityline 44 - lemma
OAI.DirectionalTransience.RowBridge.entryWeightline 57 - lemma
OAI.DirectionalTransience.RowBridge.annealedLaw_eqline 67