OAI/NumberTheory/PrimePackets/KernelEntropy.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.kernel_cond_le line 50
  2. theorem OAI.PrimeDegreePackets.zero_entropy_component_collection_null line 67
  3. lemma OAI.PrimeDegreePackets.measurable_kernel_entropyRate line 109
  4. lemma OAI.PrimeDegreePackets.observationEntropyRate_kernel_zero line 119
  5. theorem OAI.PrimeDegreePackets.positive_entropy_components_ae line 151
  6. theorem OAI.PrimeDegreePackets.fixedPoint_mem_closed_convex_orbit line 227
  7. theorem OAI.PrimeDegreePackets.exists_convex_orbit_approximants line 260
  8. def OAI.PrimeDegreePackets.actionInvariantSigma line 278
  9. lemma OAI.PrimeDegreePackets.actionInvariantSigma_le line 281
  10. lemma OAI.PrimeDegreePackets.measurable_actionInvariantSigma line 285
  11. theorem OAI.PrimeDegreePackets.exists_pointwise_invariant_representative line 297
  12. def OAI.PrimeDegreePackets.orbitConvexHull line 335
  13. lemma OAI.PrimeDegreePackets.orbitConvexHull_measurable line 338
  14. lemma OAI.PrimeDegreePackets.orbitConvexHull_interval line 349
  15. lemma OAI.PrimeDegreePackets.orbitConvexHull_integral line 361
  16. lemma OAI.PrimeDegreePackets.orbitConvexHull_setIntegral line 379
  17. lemma OAI.PrimeDegreePackets.lp_convex_orbit_representative line 395
  18. theorem OAI.PrimeDegreePackets.exists_invariant_orbit_average_limit line 419
  19. lemma OAI.PrimeDegreePackets.orbitConvexHull_aeSetIntegral line 456
  20. lemma OAI.PrimeDegreePackets.invariant_set_independent_of_orbit_indicator_limit line 469
  21. theorem OAI.PrimeDegreePackets.ergodicSMul_of_orbit_indicator_limits line 511