OAI/Combinatorics/UniformKServer/PartitionCausal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Filtration measurability of actual partition keys, anchors, and pilot parameters, with a common initially sampled finite tape.

  1. theorem OAI.UniformKServer.ActualPartitions.Config.key_measurable line 19
  2. theorem OAI.UniformKServer.ActualPartitions.Config.anchor_measurable line 30
  3. theorem OAI.UniformKServer.ActualPartitions.Config.long_measurable line 42
  4. theorem OAI.UniformKServer.ActualPartitions.Config.short_measurable line 60