OAI/Analysis/FreeWords/UltraExpectation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KKTraceTransfer.ultraOrder line 265
2. theorem OAI.KKTraceTransfer.closure_range_surjective line 280
3. theorem OAI.KKTraceTransfer.ultraProjection_surjective line 289
4. theorem OAI.KKTraceTransfer.trace_star_mul_zero_of_gns_zero line 294
5. theorem OAI.KKTraceTransfer.sequenceMean_zero_of_projection_zero line 300