OAI/Combinatorics/BalancedRyser/Local/LocalSelectedKernel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.KernelBridge.encodeOutput line 14
  2. theorem OAI.Balanced.Local.KernelBridge.configuration_encodeOutput line 17
  3. def OAI.Balanced.Local.KernelBridge.transportedKernel line 22
  4. theorem OAI.Balanced.Local.KernelBridge.sum_transported_event line 25
  5. theorem OAI.Balanced.Local.KernelBridge.transported_nonneg line 36
  6. theorem OAI.Balanced.Local.KernelBridge.exists_positive_preimage line 46
  7. theorem OAI.Balanced.Local.KernelBridge.canonical_choice_mem line 59
  8. theorem OAI.Balanced.Local.KernelBridge.positive_outputs_tuple_eq line 68
  9. theorem OAI.Balanced.Local.KernelBridge.transported_cylinder_le line 81
  10. theorem OAI.Balanced.Local.KernelBridge.transported_kernelConditions line 132
  11. theorem OAI.Balanced.Local.KernelBridge.original_offset_atom_real line 159
  12. theorem OAI.Balanced.Local.KernelBridge.transported_probability_eq_jointMass line 163
  13. theorem OAI.Balanced.Local.KernelBridge.transported_successMass_eq line 179