OAI/Probability/BinarySweep/Conditional/ConditionalSpecht.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.groupAverage_comp_slots line 19
  2. theorem OAI.BinaryCoordinateSweeps.conditional_specht_hs line 32
  3. theorem OAI.BinaryCoordinateSweeps.conditional_specht_many_bound line 55
  4. lemma OAI.BinaryCoordinateSweeps.continuous_lineLaw line 77
  5. lemma OAI.BinaryCoordinateSweeps.continuous_gridWeight line 82
  6. lemma OAI.BinaryCoordinateSweeps.continuous_conditionalNormalizer line 86
  7. lemma OAI.BinaryCoordinateSweeps.continuousAt_conditionalChoiceWeight line 94
  8. lemma OAI.BinaryCoordinateSweeps.continuousAt_conditionalGroupLaw line 99
  9. lemma OAI.BinaryCoordinateSweeps.continuousAt_endpointProbability line 108
  10. lemma OAI.BinaryCoordinateSweeps.continuousAt_centeredEndpointKernel line 119
  11. lemma OAI.BinaryCoordinateSweeps.continuousAt_centeredEndpointHS line 128