OAI/Combinatorics/Sidorenko/OrbitBounds.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SidorenkoCounterexample.reduceSubspace_finrank_containing line 12
  2. def OAI.SidorenkoCounterexample.commonReductionLagrangian line 30
  3. theorem OAI.SidorenkoCounterexample.commonOrbit_injection line 35
  4. theorem OAI.SidorenkoCounterexample.commonOrbit_card_lower line 119
  5. def OAI.SidorenkoCounterexample.tripleDefect line 137
  6. theorem OAI.SidorenkoCounterexample.pairOrbitConstant_mono line 142
  7. def OAI.SidorenkoCounterexample.orbitMassConstant line 150
  8. theorem OAI.SidorenkoCounterexample.orbitMassConstant_pos line 152
  9. theorem OAI.SidorenkoCounterexample.tripleOrbit_card_lower line 155
  10. theorem OAI.SidorenkoCounterexample.triple_subspace_orbit_surjection line 243
  11. theorem OAI.SidorenkoCounterexample.triple_subspace_orbit_card_identity line 301
  12. theorem OAI.SidorenkoCounterexample.subspace_map_eq_of_restriction_equiv line 318
  13. theorem OAI.SidorenkoCounterexample.triple_decomposition_equiv line 332
  14. theorem OAI.SidorenkoCounterexample.triple_comap_isCompl line 364
  15. theorem OAI.SidorenkoCounterexample.triple_isotropic_config_transitivity line 377
  16. theorem OAI.SidorenkoCounterexample.triple_isotropic_orbit_card_upper line 421
  17. abbrev OAI.SidorenkoCounterexample.CommonZeroDimProfile line 463
  18. theorem OAI.SidorenkoCounterexample.commonZeroProfile_injection line 471
  19. def OAI.SidorenkoCounterexample.profileMassConstant line 538
  20. theorem OAI.SidorenkoCounterexample.profileMassConstant_pos line 539
  21. theorem OAI.SidorenkoCounterexample.profileMassConstant_mono line 543
  22. theorem OAI.SidorenkoCounterexample.commonZeroProfile_card_upper line 551
  23. abbrev OAI.SidorenkoCounterexample.TripleDimProfile line 623
  24. def OAI.SidorenkoCounterexample.tripleProfileCommon line 629
  25. theorem OAI.SidorenkoCounterexample.reducePair_finrank line 633
  26. theorem OAI.SidorenkoCounterexample.reduceLagrangian_injective line 643
  27. theorem OAI.SidorenkoCounterexample.fixedCommonProfile_injection line 652
  28. theorem OAI.SidorenkoCounterexample.fixedCommonProfile_card_upper line 707
  29. def OAI.SidorenkoCounterexample.fullProfileConstant line 736
  30. theorem OAI.SidorenkoCounterexample.fullProfileConstant_pos line 737
  31. theorem OAI.SidorenkoCounterexample.tripleProfile_card_upper line 740
  32. theorem OAI.SidorenkoCounterexample.symplectic_pair_count line 787
  33. theorem OAI.SidorenkoCounterexample.symplectic_pair_card_bounds line 809
  34. abbrev OAI.SidorenkoCounterexample.OrderedPairDim line 844
  35. def OAI.SidorenkoCounterexample.orderedPairDimEquiv line 846
  36. theorem OAI.SidorenkoCounterexample.orderedPairDim_card_lower line 853
  37. abbrev OAI.SidorenkoCounterexample.PairCompletion line 877
  38. theorem OAI.SidorenkoCounterexample.pairCompletion_card_congr line 882
  39. def OAI.SidorenkoCounterexample.profilePairCompletionEquiv line 902
  40. theorem OAI.SidorenkoCounterexample.tripleProfile_completion_card line 910
  41. theorem OAI.SidorenkoCounterexample.conditionalProfile_card_upper line 926