OAI/Combinatorics/Progressions/Probability/RawSourceLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.canonicalRawOutput line 14
  2. theorem OAI.Erdos3.canonicalRawOutput_eq line 23
  3. theorem OAI.Erdos3.canonicalRawOutput_joint_map line 36
  4. theorem OAI.Erdos3.canonicalRawOutput_measurable line 51
  5. def OAI.Erdos3.rawSourceOutput line 79
  6. theorem OAI.Erdos3.rawSourceOutput_rescale line 88
  7. theorem OAI.Erdos3.rawSourceOutput_measurable line 101
  8. theorem OAI.Erdos3.rawSourceOutput_integral line 127
  9. theorem OAI.Erdos3.rawSourceOutput_joint_law line 142