OAI/Probability/BinarySweep/GridBounds/GridChildAverage.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.finitePush_conditional line 18
  2. lemma OAI.BinaryCoordinateSweeps.independentConditional_expectation line 24
  3. lemma OAI.BinaryCoordinateSweeps.sigma_relative line 37
  4. def OAI.BinaryCoordinateSweeps.GridSplit.rowInputEquiv line 48
  5. lemma OAI.BinaryCoordinateSweeps.GridSplit.rowRelative_sigma line 51
  6. lemma OAI.BinaryCoordinateSweeps.GridSplit.columnRelative_sigma line 59
  7. theorem OAI.BinaryCoordinateSweeps.GridSplit.rowAverage_child_laws line 71
  8. theorem OAI.BinaryCoordinateSweeps.GridSplit.columnAverage_child_laws line 97
  9. abbrev OAI.BinaryCoordinateSweeps.GridSplit.Junction line 138
  10. abbrev OAI.BinaryCoordinateSweeps.GridSplit.junctionSize line 139
  11. def OAI.BinaryCoordinateSweeps.GridSplit.junctionEnum line 141
  12. def OAI.BinaryCoordinateSweeps.GridSplit.physicalBoard line 143
  13. def OAI.BinaryCoordinateSweeps.GridSplit.rowGrouping line 154
  14. def OAI.BinaryCoordinateSweeps.GridSplit.columnGrouping line 158
  15. lemma OAI.BinaryCoordinateSweeps.GridSplit.rowReference_right line 162
  16. lemma OAI.BinaryCoordinateSweeps.GridSplit.rowGrouping_first line 166
  17. lemma OAI.BinaryCoordinateSweeps.GridSplit.columnGrouping_first line 174
  18. lemma OAI.BinaryCoordinateSweeps.GridSplit.physicalBoard_row line 177
  19. lemma OAI.BinaryCoordinateSweeps.GridSplit.physicalBoard_column line 182
  20. lemma OAI.BinaryCoordinateSweeps.GridSplit.junctionSize_eq line 187
  21. def OAI.BinaryCoordinateSweeps.Signed.finBlockPermEquiv line 200
  22. theorem OAI.BinaryCoordinateSweeps.Signed.groupedAverage_literal line 204
  23. lemma OAI.BinaryCoordinateSweeps.Signed.groupedAverage_literal_linear line 221