OAI/Combinatorics/MatchingEntropy/FractionalReduction.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.Refined.FractionalVertex line 16
  2. instance OAI.MatchingEntropyBounds.Refined.fractionalVertexDecidable line 19
  3. instance OAI.MatchingEntropyBounds.Refined.fractionalEdgeDecidable line 21
  4. def OAI.MatchingEntropyBounds.Refined.fractionalGraph line 23
  5. def OAI.MatchingEntropyBounds.Refined.fractionalMean line 29
  6. def OAI.MatchingEntropyBounds.Refined.fractionalExtension line 31
  7. def OAI.MatchingEntropyBounds.Refined.fixedFace line 39
  8. theorem OAI.MatchingEntropyBounds.Refined.fractionalExtension_apply_fractional line 43
  9. theorem OAI.MatchingEntropyBounds.Refined.fractionalExtension_apply_fixed line 48
  10. theorem OAI.MatchingEntropyBounds.Refined.fractionalExtension_mean line 53
  11. theorem OAI.MatchingEntropyBounds.Refined.fractionalExtension_injective line 59
  12. theorem OAI.MatchingEntropyBounds.Refined.fractionalLinear_injective line 66
  13. theorem OAI.MatchingEntropyBounds.Refined.fractional_incident line 74
  14. theorem OAI.MatchingEntropyBounds.Refined.fixed_or_zero line 80
  15. theorem OAI.MatchingEntropyBounds.Refined.incident_forced_zero line 89
  16. theorem OAI.MatchingEntropyBounds.Refined.fractional_no_forced line 99
  17. theorem OAI.MatchingEntropyBounds.Refined.positive_incident line 108
  18. theorem OAI.MatchingEntropyBounds.Refined.fixed_at_vertex line 122
  19. def OAI.MatchingEntropyBounds.Refined.fractionalAdd line 133
  20. theorem OAI.MatchingEntropyBounds.Refined.mem_fractionalAdd line 167
  21. theorem OAI.MatchingEntropyBounds.Refined.mem_fractionalAdd_fractional line 183
  22. theorem OAI.MatchingEntropyBounds.Refined.fractionalAdd_injective line 196
  23. def OAI.MatchingEntropyBounds.Refined.FixedMatching line 203
  24. def OAI.MatchingEntropyBounds.Refined.fractionalRemove line 206
  25. theorem OAI.MatchingEntropyBounds.Refined.fractionalAdd_range line 221
  26. theorem OAI.MatchingEntropyBounds.Refined.law_zero_of_mean_zero line 239
  27. theorem OAI.MatchingEntropyBounds.Refined.fractional_law_support line 247
  28. theorem OAI.MatchingEntropyBounds.Refined.fiberMass_injective_apply line 263
  29. theorem OAI.MatchingEntropyBounds.Refined.fiberMass_outside line 269
  30. theorem OAI.MatchingEntropyBounds.Refined.fiberMass_pullback line 275
  31. theorem OAI.MatchingEntropyBounds.Refined.simplex_of_fiberMass line 285
  32. theorem OAI.MatchingEntropyBounds.Refined.fractionalAdd_indicator line 294
  33. theorem OAI.MatchingEntropyBounds.Refined.fractional_mean_push line 307
  34. theorem OAI.MatchingEntropyBounds.Refined.fractional_pull_feasible line 321
  35. theorem OAI.MatchingEntropyBounds.Refined.fractional_feasible_iff line 338
  36. theorem OAI.MatchingEntropyBounds.Refined.fractional_image_eq line 350
  37. theorem OAI.MatchingEntropyBounds.Refined.fractionalMean_mem line 371
  38. theorem OAI.MatchingEntropyBounds.Refined.fixedFace_extreme line 380
  39. theorem OAI.MatchingEntropyBounds.Refined.extreme_affine_image line 407
  40. theorem OAI.MatchingEntropyBounds.Refined.extreme_affine_preimage line 416
  41. theorem OAI.MatchingEntropyBounds.Refined.minimalFace_map line 430
  42. theorem OAI.MatchingEntropyBounds.Refined.faceDimension_map line 445
  43. theorem OAI.MatchingEntropyBounds.Refined.fractional_minimalFace line 455
  44. theorem OAI.MatchingEntropyBounds.Refined.fractional_dimension line 462
  45. theorem OAI.MatchingEntropyBounds.Refined.fractional_entropy_terms line 470
  46. theorem OAI.MatchingEntropyBounds.Refined.fractional_maxEntropy line 485
  47. theorem OAI.MatchingEntropyBounds.Refined.fractional_laws line 499
  48. theorem OAI.MatchingEntropyBounds.Refined.fractional_reduction line 515