OAI/Probability/SpanningForest/FactorAssembly.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem336.FactorAssembly.EdgeField line 14
  2. abbrev OAI.Problem336.FactorAssembly.GraphDrift line 15
  3. abbrev OAI.Problem336.FactorAssembly.GraphNoise line 16
  4. def OAI.Problem336.FactorAssembly.DriftBorel line 18
  5. def OAI.Problem336.FactorAssembly.NoiseBorel line 21
  6. def OAI.Problem336.FactorAssembly.DriftEquivariant line 24
  7. def OAI.Problem336.FactorAssembly.NoiseEquivariant line 28
  8. def OAI.Problem336.FactorAssembly.decodedSlope line 32
  9. def OAI.Problem336.FactorAssembly.rule line 36
  10. theorem OAI.Problem336.FactorAssembly.measurable_decodedPath line 41
  11. theorem OAI.Problem336.FactorAssembly.measurable_decodedSlope line 51
  12. theorem OAI.Problem336.FactorAssembly.measurable_rule_edge line 57
  13. theorem OAI.Problem336.FactorAssembly.ruleBorel_of_coordinate_measurable line 68
  14. theorem OAI.Problem336.FactorAssembly.rule_borel line 79
  15. theorem OAI.Problem336.FactorAssembly.decodedPath_relabel line 83
  16. theorem OAI.Problem336.FactorAssembly.rule_equivariant line 93