OAI/Computability/PerfectCompleteness/Sampling/UniformLatentSupportLemmas.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.UniformLatentSupport.latentKernel_weight_zero_of_tag_ne line 23
  2. theorem OAI.PerfectCompleteness.UniformLatentSupport.latentKernel_tag line 33
  3. theorem OAI.PerfectCompleteness.UniformLatentSupport.projectedKernel_weight_inr line 38
  4. theorem OAI.PerfectCompleteness.UniformLatentSupport.projectedKernel_tag line 45
  5. def OAI.PerfectCompleteness.UniformLatentSupport.childLaw line 70
  6. theorem OAI.PerfectCompleteness.UniformLatentSupport.childLaw_weight line 77
  7. theorem OAI.PerfectCompleteness.UniformLatentSupport.childLaw_projected_tag line 86
  8. theorem OAI.PerfectCompleteness.UniformLatentSupport.childrenLaw_child_weight_ne_zero line 98
  9. theorem OAI.PerfectCompleteness.UniformLatentSupport.childrenLaw_projected_tag line 109
  10. theorem OAI.PerfectCompleteness.UniformLatentSupport.conditioned_childrenLaw_projected_tag line 119
  11. abbrev OAI.PerfectCompleteness.NativeTaggedUniform.Raw line 143
  12. def OAI.PerfectCompleteness.NativeTaggedUniform.sourceTag line 145
  13. def OAI.PerfectCompleteness.NativeTaggedUniform.kernel line 155
  14. theorem OAI.PerfectCompleteness.NativeTaggedUniform.kernel_weight_zero_of_tag_ne line 159
  15. theorem OAI.PerfectCompleteness.NativeTaggedUniform.kernel_tag line 169
  16. theorem OAI.PerfectCompleteness.NativeTaggedUniform.projectedKernel_weight_inl line 182
  17. theorem OAI.PerfectCompleteness.NativeTaggedUniform.projectedKernel_sourceTag line 189
  18. theorem OAI.PerfectCompleteness.NativeTaggedUniform.childLaw_sourceTag line 219
  19. theorem OAI.PerfectCompleteness.NativeTaggedUniform.childrenLaw_sourceTag line 230
  20. theorem OAI.PerfectCompleteness.NativeTaggedUniform.childrenLaw_native_tag line 241
  21. theorem OAI.PerfectCompleteness.NativeTaggedUniform.conditioned_childrenLaw_sourceTag line 252
  22. theorem OAI.PerfectCompleteness.QuarterBalance.nonzero_linear_surjective line 280
  23. theorem OAI.PerfectCompleteness.QuarterBalance.uniform_bit_probability line 293
  24. theorem OAI.PerfectCompleteness.QuarterBalance.uniform_sign_expectation_eq_zero line 302
  25. theorem OAI.PerfectCompleteness.QuarterBalance.uniform_balanced line 307
  26. theorem OAI.PerfectCompleteness.RecursiveSamplerBias.sign_sum line 330
  27. theorem OAI.PerfectCompleteness.RecursiveSamplerBias.abs_expectation_sign_le_one line 340
  28. def OAI.PerfectCompleteness.RecursiveSamplerBias.ordinaryCharacterMean line 351
  29. def OAI.PerfectCompleteness.RecursiveSamplerBias.pairCharacterMean line 362
  30. theorem OAI.PerfectCompleteness.RecursiveSamplerBias.law_step_character line 370
  31. theorem OAI.PerfectCompleteness.RecursiveSamplerBias.abs_ordinaryCharacterMean_le_one line 439
  32. theorem OAI.PerfectCompleteness.RecursiveSamplerBias.ordinaryCharacterMean_eq_zero line 456
  33. theorem OAI.PerfectCompleteness.RecursiveSamplerBias.law_step_bias_le line 469
  34. def OAI.PerfectCompleteness.RecursiveSamplerBias.RepetitionsBalanced line 491
  35. theorem OAI.PerfectCompleteness.RecursiveSamplerBias.repetitionsBalanced_of_six_le line 494
  36. theorem OAI.PerfectCompleteness.RecursiveSamplerBias.law_balanced line 502
  37. theorem OAI.PerfectCompleteness.RecursiveSamplerBias.law_bias_le line 522
  38. theorem OAI.PerfectCompleteness.RecursiveSamplerBias.law_bias_le_height line 533
  39. theorem OAI.PerfectCompleteness.RecursiveSamplerBias.tape_bias_le line 545