OAI/Combinatorics/Sidorenko/Configurations.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SidorenkoCounterexample.triple_pairs_disjoint line 10
  2. theorem OAI.SidorenkoCounterexample.triple_own_avoidance line 22
  3. theorem OAI.SidorenkoCounterexample.reduction_intersection_of_split_kernel line 37
  4. def OAI.SidorenkoCounterexample.orderedTransversePairEquiv line 70
  5. theorem OAI.SidorenkoCounterexample.symplectic_orderedTransversePair_card line 85
  6. theorem OAI.SidorenkoCounterexample.symplectic_transverseTriple_card_lower line 98
  7. theorem OAI.SidorenkoCounterexample.symplectic_transverseTriple_probability_lower line 124
  8. theorem OAI.SidorenkoCounterexample.reduceSubspace_eq_bot_of_le line 153
  9. theorem OAI.SidorenkoCounterexample.triplePairSum_split line 159
  10. theorem OAI.SidorenkoCounterexample.triplePairSum_reduce_pair line 168
  11. theorem OAI.SidorenkoCounterexample.triplePairSum_reductions_transverse line 176
  12. abbrev OAI.SidorenkoCounterexample.LagTripleOrbit line 203
  13. theorem OAI.SidorenkoCounterexample.orderedTripleOrbit_lagrangians line 206
  14. def OAI.SidorenkoCounterexample.lagTripleOrbitEquiv line 214
  15. def OAI.SidorenkoCounterexample.avoidanceTripleReduction line 229
  16. theorem OAI.SidorenkoCounterexample.avoidanceTripleReduction_uniform line 237
  17. abbrev OAI.SidorenkoCounterexample.AvoidanceOrbitFiber line 252
  18. theorem OAI.SidorenkoCounterexample.avoidanceOrbitFiber_card_identity line 260
  19. theorem OAI.SidorenkoCounterexample.avoidanceOrbitFiber_card_lower line 287
  20. theorem OAI.SidorenkoCounterexample.containmentOrbitFiber_card_lower line 318
  21. theorem OAI.SidorenkoCounterexample.exists_isotropic_isometry_extension line 372

    Source documentation

    A prescribed linear isomorphism of isotropic spaces extends to an actual symplectic automorphism, not only to a dimension-preserving correspondence.

     theorem exists_isotropic_isometry_extension (h2 : (2 : K) ≠ 0) (ha : ω.IsAlt)
    (hω : ω.Nondegenerate) (S T : Submodule K E)
    (hS : S ≤ ω.orthogonal S) (hT : T ≤ ω.orthogonal T) (g : S ≃ₗ[K] T) :
    ∃ e : E ≃ₗ[K] E, (∀ x y, ω (e x) (e y) = ω x y) ∧
      ∀ x : S, e x.val = (g x).val := by
…
  22. abbrev OAI.SidorenkoCounterexample.FixedPairTripleOrbit line 417
  23. theorem OAI.SidorenkoCounterexample.triplePair_inter_own line 422
  24. theorem OAI.SidorenkoCounterexample.triplePairSum_split_all line 430
  25. theorem OAI.SidorenkoCounterexample.triplePair_inter_all line 440
  26. def OAI.SidorenkoCounterexample.tripleResidualLagrangian line 453
  27. abbrev OAI.SidorenkoCounterexample.OwnAvoidanceOrbitFiber line 459
  28. theorem OAI.SidorenkoCounterexample.ownAvoidanceOrbitFiber_pairs line 468
  29. def OAI.SidorenkoCounterexample.ownAvoidanceOrbitFiberEmbedding line 492
  30. theorem OAI.SidorenkoCounterexample.subspace_map_extension line 530
  31. theorem OAI.SidorenkoCounterexample.subtype_map_comap_of_le line 540
  32. theorem OAI.SidorenkoCounterexample.subspace_comap_sup_of_le line 545
  33. theorem OAI.SidorenkoCounterexample.triple_subspace_orbit_injection line 553
  34. theorem OAI.SidorenkoCounterexample.fullTripleOrbit_fixedPair_injection line 620
  35. theorem OAI.SidorenkoCounterexample.fullTripleOrbit_fixedPair_card_lower line 671
  36. theorem OAI.SidorenkoCounterexample.triple_isotropic_orbit_card_lower line 686
  37. theorem OAI.SidorenkoCounterexample.fixedPairTripleOrbit_card_lower line 748
  38. theorem OAI.SidorenkoCounterexample.pair_cost_cancellation line 788
  39. theorem OAI.SidorenkoCounterexample.common_cost_cancellation line 806
  40. theorem OAI.SidorenkoCounterexample.finrank_sup_of_disjoint line 821
  41. theorem OAI.SidorenkoCounterexample.triplePairSum_finrank line 827
  42. theorem OAI.SidorenkoCounterexample.triplePairSum_inter_finrank line 833
  43. def OAI.SidorenkoCounterexample.pairOrbitConstant line 838
  44. theorem OAI.SidorenkoCounterexample.pairOrbitConstant_pos line 841
  45. theorem OAI.SidorenkoCounterexample.commonZeroOrbit_card_lower line 848