OAI/NumberTheory/PrimePackets/EntropyMixtures.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.negMulLog_sum_le line 48
  2. lemma OAI.PrimeDegreePackets.finiteShannon_mixture_joint line 59
  3. lemma OAI.PrimeDegreePackets.finiteShannon_mixture_bounds line 66
  4. lemma OAI.PrimeDegreePackets.observationEntropy_finite_mixture_bounds line 84
  5. theorem OAI.PrimeDegreePackets.observationEntropyRate_finite_mixture line 103
  6. lemma OAI.PrimeDegreePackets.kernel_comp_real line 140
  7. lemma OAI.PrimeDegreePackets.kernel_mixture_preserving line 148
  8. def OAI.PrimeDegreePackets.kernelCell line 162
  9. instance OAI.PrimeDegreePackets.kernelCell_probability line 165
  10. lemma OAI.PrimeDegreePackets.kernelCell_preserving line 174
  11. lemma OAI.PrimeDegreePackets.weighted_kernelCell line 184
  12. lemma OAI.PrimeDegreePackets.kernel_finite_cells line 195
  13. lemma OAI.PrimeDegreePackets.kernelCell_real line 215
  14. lemma OAI.PrimeDegreePackets.measurable_kernel_real line 223
  15. lemma OAI.PrimeDegreePackets.integrable_kernel_real line 226
  16. lemma OAI.PrimeDegreePackets.finite_measurable_small_fibers line 241
  17. lemma OAI.PrimeDegreePackets.continuous_finiteShannon line 277
  18. lemma OAI.PrimeDegreePackets.measurable_kernel_entropy line 282
  19. lemma OAI.PrimeDegreePackets.integrable_kernel_entropy line 289
  20. lemma OAI.PrimeDegreePackets.ae_nonnull_fiber line 301
  21. lemma OAI.PrimeDegreePackets.kernelCell_real_close line 314
  22. theorem OAI.PrimeDegreePackets.kernel_entropy_finite_approx line 353
  23. lemma OAI.PrimeDegreePackets.integrable_finite_values line 391
  24. lemma OAI.PrimeDegreePackets.integral_finite_values line 402
  25. lemma OAI.PrimeDegreePackets.observationEntropyRate_nonneg line 413
  26. lemma OAI.PrimeDegreePackets.observationEntropyRate_le_block line 424
  27. theorem OAI.PrimeDegreePackets.kernel_entropyRate_le_block line 437
  28. lemma OAI.PrimeDegreePackets.normalized_orbit_entropy_le line 473
  29. lemma OAI.PrimeDegreePackets.observationEntropyRate_eq_zero_of_measureEntropy line 487
  30. theorem OAI.PrimeDegreePackets.measureEntropy_kernel_zero line 499