OAI/GroupTheory/SimpleAmenable/RandomFields/RecoveredConstantCovariance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.initial_constant_covariance_eventually line 11
2. def OAI.SimpleAmenable.OffsetFrame.zero line 32
3. theorem OAI.SimpleAmenable.InitialCoverSystem.constant_mem_polygonStars line 46
4. theorem OAI.SimpleAmenable.InitialCoverSystem.distinctSlotStar_zero_constant line 54
5. theorem OAI.SimpleAmenable.InitialCoverSystem.distinctSlotStar_offset_formula line 73
6. def OAI.SimpleAmenable.InitialCoverSystem.constantReindexedFrame line 82
7. theorem OAI.SimpleAmenable.InitialCoverSystem.distinctSlotStar_constant_transport line 115