OAI/Combinatorics/Sidorenko/SubspaceCounts.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SidorenkoCounterexample.symplecticLagrangianEquiv line 12
2. theorem OAI.SidorenkoCounterexample.symplecticLagrangian_card_bounds line 25
3. theorem OAI.SidorenkoCounterexample.symplecticLagrangian_card_pos line 41
4. theorem OAI.SidorenkoCounterexample.isotropic_finrank_le_half line 48
5. theorem OAI.SidorenkoCounterexample.containingLagrangian_card_bounds line 55
6. abbrev OAI.SidorenkoCounterexample.IsotropicDimspace line 78
7. def OAI.SidorenkoCounterexample.isotropicIncidenceEquiv line 81
8. theorem OAI.SidorenkoCounterexample.isotropic_incidence_card line 109
9. def OAI.SidorenkoCounterexample.isotropicExponent line 121

   Source documentation

   The exponent 2Dc-(3c²-c)/2, written without truncated half-integers.

   def isotropicExponent (D c : ℕ) : ℕ :=
   …

10. theorem OAI.SidorenkoCounterexample.isotropicExponent_add line 124
11. theorem OAI.SidorenkoCounterexample.isotropic_card_bounds line 134
12. theorem OAI.SidorenkoCounterexample.lagrangianConstant_mono line 220
13. theorem OAI.SidorenkoCounterexample.lagrangian_bad_intersection_card line 232

    Source documentation

    The elementary line union bound, expressed before taking probabilities.

    theorem lagrangian_bad_intersection_card (h2 : (2 : K) ≠ 0)
        (ha : ω.IsAlt) (hω : ω.Nondegenerate) (D : ℕ) (hD : 2*D = finrank K E)
        (S : Submodule K E) (hS : S ≤ ω.orthogonal S) (hpos : 0 < finrank K S) :
        (Nat.card {L : SymplecticLagrangian ω // ¬ Disjoint L.val S} : ℝ) ≤
          (2*(Fintype.card K : ℝ)^(finrank K S-1)) *
            (lagrangianConstant (D-1)*(Fintype.card K : ℝ)^((D-1+1).choose 2)) := by
    …

    Mentions: OAI.SidorenkoCounterexample.SymplecticLagrangian, OAI.SidorenkoCounterexample.lagrangianConstant

14. theorem OAI.SidorenkoCounterexample.lagrangian_bad_intersection_scaled line 284

    Source documentation

    For fixed dimension, failure of avoiding an isotropic space is O(1/q). No transversality statement is used as a probabilistic assumption.

    theorem lagrangian_bad_intersection_scaled (h2 : (2 : K) ≠ 0)
        (ha : ω.IsAlt) (hω : ω.Nondegenerate) (D : ℕ) (hD : 2*D = finrank K E)
        (S : Submodule K E) (hS : S ≤ ω.orthogonal S) :
        (Nat.card {L : SymplecticLagrangian ω // ¬ Disjoint L.val S} : ℝ) *
          Fintype.card K ≤ 2*lagrangianConstant D*Nat.card (SymplecticLagrangian ω) := by
    …

    Mentions: OAI.SidorenkoCounterexample.SymplecticLagrangian, OAI.SidorenkoCounterexample.lagrangianConstant

15. theorem OAI.SidorenkoCounterexample.lagrangian_disjoint_card_lower line 326
16. theorem OAI.SidorenkoCounterexample.reduceSubspace_isotropic line 355
17. def OAI.SidorenkoCounterexample.containmentAvoidanceEquiv line 363

    Source documentation

    Containment and exact intersection become ordinary avoidance in the containment quotient. This is a literal equivalence of finite sample spaces.

    noncomputable def containmentAvoidanceEquiv (ha : ω.IsAlt)
        (A S : Submodule K E) (hAS : A ≤ S) (hS : S ≤ ω.orthogonal S) :
        AvoidanceSpace ω S A ≃
          {L : SymplecticLagrangian (symplecticReductionForm ω A ha) //
            Disjoint L.val (reduceSubspace ω A S)} := by
    …

    Mentions: OAI.SidorenkoCounterexample.AvoidanceSpace, OAI.SidorenkoCounterexample.SymplecticLagrangian, OAI.SidorenkoCounterexample.symplecticReductionForm, OAI.SidorenkoCounterexample.reduceSubspace

18. theorem OAI.SidorenkoCounterexample.avoidance_card_lower line 402
19. theorem OAI.SidorenkoCounterexample.triple_containing_isometry_lift line 440

    Source documentation

    An isometry of three containing reductions lifts to a simultaneous isometry of the actual Lagrangians, fixing their common space pointwise.

    theorem triple_containing_isometry_lift (ha : ω.IsAlt) (hω : ω.Nondegenerate)
        (_hS : S ≤ ω.orthogonal S) (L M N L' M' N' : Submodule K E)
        (hL : ω.orthogonal L = L) (hM : ω.orthogonal M = M) (hN : ω.orthogonal N = N)
        (hL' : ω.orthogonal L' = L') (hM' : ω.orthogonal M' = M') (hN' : ω.orthogonal N' = N')
        (hSL : S ≤ L) (hSM : S ≤ M) (hSN : S ≤ N)
        (hSL' : S ≤ L') (hSM' : S ≤ M') (hSN' : S ≤ N')
        (hres : TripleIsometry (symplecticReductionForm ω S ha) (symplecticReductionForm ω S ha)
          (reduceSubspace ω S L) (reduceSubspace ω S M) (reduceSubspace ω S N)
          (reduceSubspace ω S L') (reduceSubspace ω S M') (reduceSubspace ω S N')) :
        TripleIsometry ω ω L M N L' M' N' := by
    …

    Mentions: OAI.SidorenkoCounterexample.TripleIsometry, OAI.SidorenkoCounterexample.symplecticReductionForm, OAI.SidorenkoCounterexample.reduceSubspace

20. abbrev OAI.SidorenkoCounterexample.PairLinearOrbit line 482
21. abbrev OAI.SidorenkoCounterexample.PairLinearStabilizer line 486
22. def OAI.SidorenkoCounterexample.pairLinearOrbitMap line 489
23. theorem OAI.SidorenkoCounterexample.submodule_map_trans line 492
24. theorem OAI.SidorenkoCounterexample.submodule_map_symm_cancel line 496
25. def OAI.SidorenkoCounterexample.pairLinearOrbitFiberEquiv line 501
26. def OAI.SidorenkoCounterexample.pairLinearStabilizerRestriction line 535
27. theorem OAI.SidorenkoCounterexample.pairLinearStabilizerRestriction_bijective line 539
28. theorem OAI.SidorenkoCounterexample.pairLinearOrbit_card_identity line 595
29. theorem OAI.SidorenkoCounterexample.linearAut_card_upper line 610
30. theorem OAI.SidorenkoCounterexample.pairLinearOrbit_card_bounds line 620

    Source documentation

    Ordered complementary decompositions have q^(2uv) choices up to a positive fixed-dimension constant; proved from their exact stabilizer.

    theorem pairLinearOrbit_card_bounds (U V : Submodule K E) (hUV : IsCompl U V) :
        (Fintype.card K : ℝ)^(2*finrank K U*finrank K V) ≤
          2^(finrank K E)*(Nat.card (PairLinearOrbit U V) : ℝ) ∧
        (Nat.card (PairLinearOrbit U V) : ℝ) ≤
          2^(finrank K E)*(Fintype.card K : ℝ)^(2*finrank K U*finrank K V) := by
    …

    Mentions: OAI.SidorenkoCounterexample.PairLinearOrbit

31. def OAI.SidorenkoCounterexample.tripleSumEquiv line 668

    Source documentation

    Literal coordinates for an ordered direct sum of three subspaces.

    noncomputable def tripleSumEquiv (U V W : Submodule K E)
        (hU : IsCompl U (V ⊔ W)) (hVW : Disjoint V W) : (U × (V × W)) ≃ₗ[K] E := by
    …

32. theorem OAI.SidorenkoCounterexample.tripleSumEquiv_apply line 683
33. abbrev OAI.SidorenkoCounterexample.TripleLinearOrbit line 687
34. abbrev OAI.SidorenkoCounterexample.TripleLinearStabilizer line 691
35. def OAI.SidorenkoCounterexample.tripleLinearOrbitMap line 694
36. def OAI.SidorenkoCounterexample.tripleLinearOrbitFiberEquiv line 697
37. def OAI.SidorenkoCounterexample.tripleLinearStabilizerRestriction line 739
38. theorem OAI.SidorenkoCounterexample.map_eq_of_restriction_aut line 744
39. theorem OAI.SidorenkoCounterexample.tripleLinearStabilizerRestriction_bijective line 756
40. theorem OAI.SidorenkoCounterexample.tripleLinearOrbit_card_identity line 803
41. theorem OAI.SidorenkoCounterexample.tripleLinearOrbit_card_bounds line 822
42. def OAI.SidorenkoCounterexample.prodFiberEquiv line 875
43. theorem OAI.SidorenkoCounterexample.uniform_prod_card line 883
44. theorem OAI.SidorenkoCounterexample.uniform_preimage_card line 896
45. theorem OAI.SidorenkoCounterexample.avoidance_exact_intersection line 916