OAI/Probability/SwitchChain/SliceReindexedComparison.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.SliceNormalized.pullback line 12
  2. theorem OAI.Problem315.SliceNormalized.pullback_apply line 17
  3. def OAI.Problem315.SliceNormalized.reindexedRaw line 22
  4. theorem OAI.Problem315.SliceNormalized.reindexedRaw_apply line 25
  5. def OAI.Problem315.SliceNormalized.reindexedMove line 30
  6. theorem OAI.Problem315.SliceNormalized.reindexedMove_apply line 35
  7. theorem OAI.Problem315.SliceNormalized.pullback_move line 42
  8. theorem OAI.Problem315.SliceNormalized.norm_projection_pullback line 49
  9. theorem OAI.Problem315.SliceNormalized.reindexed_projection_energy_le_swap_energy line 57
  10. theorem OAI.Problem315.SliceNormalized.reindexed_projection_energy_le_swap_sum line 73