OAI/Probability/ThreeState/RegularCritical.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Entropy bounds and non-reconstruction at the positive regular-tree threshold.

  1. lemma OAI.ThreeState.regular_fixedpoint_degree_nu line 13
  2. lemma OAI.ThreeState.partial_nu_le_regular line 24
  3. lemma OAI.ThreeState.correlationEntropy_sum line 30
  4. lemma OAI.ThreeState.scalar_sqrt_projection_bound line 43
  5. lemma OAI.ThreeState.regular_increment_bound line 49
  6. lemma OAI.ThreeState.sum_range_real line 92
  7. lemma OAI.ThreeState.sum_range_factorial_two line 97
  8. lemma OAI.ThreeState.reciprocal_tangent line 103
  9. lemma OAI.ThreeState.regular_rational_sum line 108
  10. lemma OAI.ThreeState.regular_sqrt_sum_sq line 148
  11. lemma OAI.ThreeState.regular_sqrt_sum line 167
  12. lemma OAI.ThreeState.regular_correlation_bound line 198
  13. lemma OAI.ThreeState.entropyF_sourceF line 222
  14. lemma OAI.ThreeState.continuous_entropyF_edge line 227
  15. lemma OAI.ThreeState.integral_entropyF_radial line 233
  16. lemma OAI.ThreeState.regular_entropy_bound line 253
  17. lemma OAI.ThreeState.critical_moment_nu_bound line 290
  18. lemma OAI.ThreeState.regular_positive_critical_uniform line 309
  19. lemma OAI.ThreeState.messageX_zero_tv line 334
  20. lemma OAI.ThreeState.integral_tv_zero_of_mu_zero line 344
  21. lemma OAI.ThreeState.observed_tendsto_zero_of_uniform_fixedpoints line 351
  22. theorem OAI.ThreeState.regular_positive_critical_nonreconstruction line 365