OAI/Computability/DirectedFeedback/Games/EqualityFiber.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.relativeDensity_filter_eq_expect line 12
  2. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.retention_image line 28
  3. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.relativeDensity_neighbors_eq_nonzero_average_half line 39
  4. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.liftedFiber_retention_eq_half line 79
  5. def OAI.DFVSGames.Inverse.EqualityFiber.fiberMass line 103
  6. def OAI.DFVSGames.Inverse.EqualityFiber.fiberFlow line 107
  7. def OAI.DFVSGames.Inverse.EqualityFiber.equalityAcceptance line 111
  8. theorem OAI.DFVSGames.Inverse.EqualityFiber.sum_fiberMass line 115
  9. theorem OAI.DFVSGames.Inverse.EqualityFiber.fiberMass_nonneg line 123
  10. theorem OAI.DFVSGames.Inverse.EqualityFiber.fiberFlow_nonneg line 133
  11. theorem OAI.DFVSGames.Inverse.EqualityFiber.fiberFlow_le_mass line 146
  12. theorem OAI.DFVSGames.Inverse.EqualityFiber.sum_sameFiber_indicator_inline_EqualityFiber line 164
  13. theorem OAI.DFVSGames.Inverse.EqualityFiber.sum_fiberFlow line 177
  14. theorem OAI.DFVSGames.Inverse.EqualityFiber.exists_positive_mass_le_flow line 190
  15. theorem OAI.DFVSGames.Inverse.EqualityFiber.exists_fiber_retention line 217
  16. theorem OAI.DFVSGames.Inverse.EqualityFiber.nonzero_retention_ge_half line 231
  17. theorem OAI.DFVSGames.Inverse.EqualityFiber.chart_retention_ge_quarter line 239
  18. def OAI.DFVSGames.Inverse.Shortcode.matrixWeight line 251
  19. theorem OAI.DFVSGames.Inverse.Shortcode.matrixWeight_probability line 254
  20. def OAI.DFVSGames.Inverse.Shortcode.matrixKernel line 263
  21. theorem OAI.DFVSGames.Inverse.Shortcode.matrixKernel_nonneg line 267
  22. theorem OAI.DFVSGames.Inverse.Shortcode.matrixKernel_probability line 275
  23. theorem OAI.DFVSGames.Inverse.Shortcode.matrixKernel_equality line 288
  24. theorem OAI.DFVSGames.Inverse.Shortcode.equalityAcceptance_eq_kernel line 301
  25. theorem OAI.DFVSGames.Inverse.Shortcode.exists_output_fiber line 319
  26. def OAI.DFVSGames.Inverse.FactorSampling.fullAverage line 339
  27. def OAI.DFVSGames.Inverse.FactorSampling.nonzeroFlow line 342
  28. def OAI.DFVSGames.Inverse.FactorSampling.zeroMass line 345
  29. theorem OAI.DFVSGames.Inverse.FactorSampling.boundary_indicator_inline_FactorSampling line 349
  30. theorem OAI.DFVSGames.Inverse.FactorSampling.boundary_mass line 355
  31. theorem OAI.DFVSGames.Inverse.FactorSampling.fullAverage_eq_zeroMass_add_nonzeroFlow line 376
  32. def OAI.DFVSGames.Inverse.FactorSampling.conditionedRetention line 403
  33. theorem OAI.DFVSGames.Inverse.FactorSampling.fullAverage_eq_mixture line 406
  34. theorem OAI.DFVSGames.Inverse.FactorSampling.conditionedRetention_ge_half line 417
  35. theorem OAI.DFVSGames.Inverse.FactorSampling.zeroMass_binary_uniform line 429
  36. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.matrixKernel_average line 444
  37. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.fiberMass_eq_card line 455
  38. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.fiberMass_pos_iff line 468
  39. def OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.fiberFactorRetention line 476
  40. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.fiberFlow_eq line 480
  41. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.fiber_retention_eq_factor_average line 496
  42. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.fiberFactorRetention_zero_left line 518
  43. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.fiberFactorRetention_zero_right line 529
  44. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.exists_output_fiber_factor_retention line 540
  45. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.uniform_pair_mixture line 556
  46. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.vector_card_real_inline_ShortcodeFiberConditioning line 628
  47. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.binary_zero_mass_nonneg_inline_ShortcodeFiberConditioning line 632
  48. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.conditioned_output_fiber line 642
  49. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.chartFiberRetention line 677
  50. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.inversePrinciple_of_expansion line 688
  51. theorem OAI.DFVSGames.Inverse.ShortcodeTheorem.inversePrinciple line 698
  52. theorem OAI.DFVSGames.Decoder.MatrixGap.exists_parameters line 706