OAI/Analysis/MarkovType/FiniteCoupling.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MarkovSuperreflexivity.FiniteCoupling line 24
  2. theorem OAI.MarkovSuperreflexivity.FiniteCoupling.weight_le_row line 36
  3. theorem OAI.MarkovSuperreflexivity.FiniteCoupling.weight_le_col line 41
  4. theorem OAI.MarkovSuperreflexivity.FiniteCoupling.weight_eq_zero_of_row line 46
  5. theorem OAI.MarkovSuperreflexivity.FiniteCoupling.weight_eq_zero_of_col line 50
  6. def OAI.MarkovSuperreflexivity.FiniteCoupling.transpose line 54
  7. def OAI.MarkovSuperreflexivity.FiniteCoupling.average line 60
  8. def OAI.MarkovSuperreflexivity.finitePushforward line 72
  9. theorem OAI.MarkovSuperreflexivity.finitePushforward_nonneg line 76
  10. theorem OAI.MarkovSuperreflexivity.finitePushforward_sum line 86
  11. theorem OAI.MarkovSuperreflexivity.weight_le_finitePushforward line 93
  12. def OAI.MarkovSuperreflexivity.finiteTotalVariation line 106
  13. def OAI.MarkovSuperreflexivity.finiteOverlap line 109
  14. def OAI.MarkovSuperreflexivity.finiteResidualMass line 111
  15. theorem OAI.MarkovSuperreflexivity.residual_left_sum line 114
  16. theorem OAI.MarkovSuperreflexivity.residual_right_sum line 120
  17. theorem OAI.MarkovSuperreflexivity.finiteResidualMass_nonneg line 126
  18. theorem OAI.MarkovSuperreflexivity.residual_product_zero line 131
  19. theorem OAI.MarkovSuperreflexivity.finiteTotalVariation_eq_residual line 137
  20. def OAI.MarkovSuperreflexivity.maximalFiniteCouplingWeight line 153
  21. theorem OAI.MarkovSuperreflexivity.maximalFiniteCouplingWeight_nonneg line 159
  22. theorem OAI.MarkovSuperreflexivity.maximalFiniteCouplingWeight_row line 173
  23. theorem OAI.MarkovSuperreflexivity.maximalFiniteCouplingWeight_transpose line 199
  24. def OAI.MarkovSuperreflexivity.maximalFiniteCoupling line 213
  25. theorem OAI.MarkovSuperreflexivity.maximalFiniteCoupling_diagonal line 223
  26. theorem OAI.MarkovSuperreflexivity.maximalFiniteCoupling_matching_mass line 229
  27. theorem OAI.MarkovSuperreflexivity.finiteCoupling_matching_mass_le line 237
  28. def OAI.MarkovSuperreflexivity.finiteConditional line 247
  29. theorem OAI.MarkovSuperreflexivity.finiteConditional_nonneg line 252
  30. theorem OAI.MarkovSuperreflexivity.finiteConditional_sum line 262
  31. theorem OAI.MarkovSuperreflexivity.finiteConditional_weighted line 277
  32. theorem OAI.MarkovSuperreflexivity.finiteConditional_reconstruct line 296
  33. def OAI.MarkovSuperreflexivity.liftFiniteCouplingWeight line 304
  34. def OAI.MarkovSuperreflexivity.liftFiniteCoupling line 311
  35. theorem OAI.MarkovSuperreflexivity.finiteConditional_feature_sum line 353
  36. theorem OAI.MarkovSuperreflexivity.finiteCoupling_conditional_feature_sum line 367
  37. theorem OAI.MarkovSuperreflexivity.liftFiniteCoupling_feature_expectation line 378
  38. theorem OAI.MarkovSuperreflexivity.liftFiniteCoupling_matching_mass line 436
  39. def OAI.MarkovSuperreflexivity.maximalFeatureCoupling line 448
  40. theorem OAI.MarkovSuperreflexivity.maximalFeatureCoupling_matching_mass line 458