OAI/Probability/SwitchChain/PairFiberEqualityTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem315.PairFiber.cardSliceEquivPowerset line 13
2. def OAI.Problem315.PairFiber.stateFiberNormalizedEquiv line 20
3. theorem OAI.Problem315.PairFiber.stateFiberNormalizedEquiv_mem line 27
4. theorem OAI.Problem315.PairFiber.raw_stateFiberNormalizedEquiv line 41
5. theorem OAI.Problem315.PairFiber.equalIndicator_stateFiberNormalizedEquiv line 54
6. theorem OAI.Problem315.PairFiber.stateFiber_average_equality line 61
7. theorem OAI.Problem315.PairFiber.stateFiber_sum_eq_fiberStates line 87
8. theorem OAI.Problem315.PairFiber.expectation_eq_equalMean_of_fiber line 105
9. theorem OAI.Problem315.PairFiber.fluctuation_eq_raw_of_fiber line 119