OAI/Combinatorics/Sidorenko/Planted.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SidorenkoCounterexample.reduceSubspace_finrank_general line 12
  2. theorem OAI.SidorenkoCounterexample.reduce_center_intersection_finrank line 35
  3. abbrev OAI.SidorenkoCounterexample.TripleCenterSet line 49
  4. def OAI.SidorenkoCounterexample.tripleCenterIsometryEquiv line 53
  5. theorem OAI.SidorenkoCounterexample.tripleCenter_orbit_card line 66
  6. theorem OAI.SidorenkoCounterexample.tripleCenterOrbit_card line 76

    Source documentation

    A literal finite disintegration over an ACTUAL ordered orbit, the exact density-ratio identity behind the local planted bound.

     theorem tripleCenterOrbit_card [Finite E] (r : ℕ) (L M N : Submodule K E) :
    Nat.card (Σ P : OrderedTripleOrbit ω L M N, TripleCenterSet ω r P.val.1 P.val.2.1 P.val.2.2) =
      Nat.card (OrderedTripleOrbit ω L M N) * Nat.card (TripleCenterSet ω r L M N) := by
…

    Mentions: OAI.SidorenkoCounterexample.OrderedTripleOrbit, OAI.SidorenkoCounterexample.TripleCenterSet

  7. abbrev OAI.SidorenkoCounterexample.SymplecticCenterStratum line 96
  8. abbrev OAI.SidorenkoCounterexample.SymplecticCenterProfile line 98
  9. theorem OAI.SidorenkoCounterexample.exists_center_coordinates line 105
  10. theorem OAI.SidorenkoCounterexample.map_pair_finrank line 125
  11. theorem OAI.SidorenkoCounterexample.map_common_zero_iff line 130
  12. def OAI.SidorenkoCounterexample.symplecticCenterStratumEquiv line 140
  13. def OAI.SidorenkoCounterexample.symplecticCenterProfileEquiv line 150
  14. theorem OAI.SidorenkoCounterexample.symplectic_center_profile_probability_bound line 165
  15. theorem OAI.SidorenkoCounterexample.symplectic_profile_pair_sum_le line 178
  16. abbrev OAI.SidorenkoCounterexample.CommonCenterSet line 194
  17. theorem OAI.SidorenkoCounterexample.commonCenter_card_upper line 197
  18. theorem OAI.SidorenkoCounterexample.commonCenter_cost_bound line 239
  19. abbrev OAI.SidorenkoCounterexample.FixedCommonCenterProfile line 271
  20. def OAI.SidorenkoCounterexample.generalReductionLagrangian line 277
  21. theorem OAI.SidorenkoCounterexample.fixedCommonCenter_injection line 282
  22. def OAI.SidorenkoCounterexample.reducedPlantedSum line 347
  23. theorem OAI.SidorenkoCounterexample.reducedPlantedSum_nonneg line 350
  24. theorem OAI.SidorenkoCounterexample.symplectic_center_profile_card_upper line 361
  25. theorem OAI.SidorenkoCounterexample.fixedCommonCenter_card_upper line 400
  26. abbrev OAI.SidorenkoCounterexample.CommonParameters line 426
  27. instance OAI.SidorenkoCounterexample.(instance at line 427) line 427
  28. abbrev OAI.SidorenkoCounterexample.ProfileCenterSet line 428
  29. abbrev OAI.SidorenkoCounterexample.PlantedCommonData line 430
  30. theorem OAI.SidorenkoCounterexample.profileCenter_injection line 434
  31. theorem OAI.SidorenkoCounterexample.unweight_count_bound line 483
  32. theorem OAI.SidorenkoCounterexample.fixedCommonCenter_card_rpow_upper line 493
  33. theorem OAI.SidorenkoCounterexample.commonData_fixed_card_upper line 504
  34. def OAI.SidorenkoCounterexample.commonPlantedTerm line 546
  35. theorem OAI.SidorenkoCounterexample.commonPlantedTerm_nonneg line 551
  36. theorem OAI.SidorenkoCounterexample.profileCenter_card_upper line 561
  37. theorem OAI.SidorenkoCounterexample.normalized_count_ratio_bound line 593
  38. theorem OAI.SidorenkoCounterexample.orbit_member_profile line 620
  39. theorem OAI.SidorenkoCounterexample.orbitCenter_profile_injection line 636
  40. theorem OAI.SidorenkoCounterexample.orbit_center_count_le_profile line 662
  41. def OAI.SidorenkoCounterexample.tripleFaceDensity line 678
  42. theorem OAI.SidorenkoCounterexample.tripleFaceDensity_nonneg line 684
  43. theorem OAI.SidorenkoCounterexample.symplectic_center_stratum_card_pos line 687
  44. theorem OAI.SidorenkoCounterexample.tripleFaceDensity_profile_bound line 697
  45. theorem OAI.SidorenkoCounterexample.tripleFaceDensity_full_bound line 733