OAI/LinearAlgebra/MatrixFields/Entropy/InitialLeafRates.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.entropy_two_points line 18
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.weighted_two_points line 37
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticRate line 55
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.binaryEntropyRate line 59
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticLaw_two_real line 62
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticRate_two line 69
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticRate_deterministic line 85
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticRate_zero line 94
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticRate_one line 98
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticRate_three line 102
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticRate_four line 107
  12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.initialRate line 125
  13. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.S0 line 128
  14. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.S1 line 132
  15. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.secondLeafRate line 135
  16. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.S2 line 143
  17. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.S line 147
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.four_shape_max_lt_five line 149
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.four_zero_max line 152
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.four_positive_max line 156
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.second_shapeMax_lt_five line 160
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.secondLeafRate_zero line 164
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.secondLeafRate_positive line 182
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.secondLeafRate_builder_expression line 188
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.list_filter_sum_inline_MatrixMultiplication_AllFieldTerminalRateFormulas line 203
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalRates.initial_zero_history_rate line 210
  27. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.InitialZero line 245
  28. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.PopulationHistory line 248
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.shapeMax_lt line 250
  30. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.shapeIndex line 255
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.card_alphabet line 258
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.card_alphabet_pos line 265
  33. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.Words line 271
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.card_words line 276
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.card_words_pos line 283
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.log_card_words line 289
  37. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.ProductWords line 296
  38. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.volume line 299
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.volume_eq_prod line 302
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.volume_pos line 307
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.log_volume line 312
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.sum_populationHistory_rate line 331
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.log_volume_eq_S0 line 347
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.normalized_log_volume_eq_S0 line 352
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialLeafRates.tendsto_normalized_log_volume line 362