OAI/Combinatorics/Sidorenko/Lagrangian.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SidorenkoCounterexample.canonicalSymplectic line 11
2. theorem OAI.SidorenkoCounterexample.canonicalSymplectic_apply line 32
3. theorem OAI.SidorenkoCounterexample.canonicalSymplectic_alt line 35
4. theorem OAI.SidorenkoCounterexample.canonicalSymplectic_nondegenerate line 39
5. abbrev OAI.SidorenkoCounterexample.Lagrangian line 60

   Source documentation

   Lagrangians are self-orthogonal subspaces, equivalently isotropic subspaces of half the ambient dimension.

   abbrev Lagrangian := {L : Submodule K (V × Module.Dual K V) //
   …

6. theorem OAI.SidorenkoCounterexample.lagrangian_finrank line 63
7. def OAI.SidorenkoCounterexample.formGraph line 72

   Source documentation

   The graph over a subspace, with its free vertical annihilator retained.

   def formGraph (U : Submodule K V) (B : LinearMap.BilinForm K U) :
       Submodule K (V × Module.Dual K V) where
   …

8. theorem OAI.SidorenkoCounterexample.formGraph_fst_range line 90
9. theorem OAI.SidorenkoCounterexample.formGraph_isotropic line 103
10. def OAI.SidorenkoCounterexample.formGraphProjection line 112
11. theorem OAI.SidorenkoCounterexample.formGraphProjection_surj line 119
12. def OAI.SidorenkoCounterexample.graphVerticalEquiv line 125
13. theorem OAI.SidorenkoCounterexample.surjective_finrank_eq line 154
14. theorem OAI.SidorenkoCounterexample.formGraph_finrank line 162
15. def OAI.SidorenkoCounterexample.graphLagrangian line 169
16. theorem OAI.SidorenkoCounterexample.graphLagrangian_form_injective line 176
17. theorem OAI.SidorenkoCounterexample.lagrangian_pairing_zero line 191
18. theorem OAI.SidorenkoCounterexample.graphLagrangian_surjective line 199

    Source documentation

    Every Lagrangian is the graph of a unique symmetric form over its first-coordinate projection. This includes nontransverse charts.

     theorem graphLagrangian_surjective :
        Function.Surjective (fun S : Σ U : Submodule K V, SymForm K U => graphLagrangian S.1 S.2) := by
    …

    Mentions: OAI.SidorenkoCounterexample.SymForm, OAI.SidorenkoCounterexample.graphLagrangian

19. def OAI.SidorenkoCounterexample.lagrangianGraphEquiv line 238
20. theorem OAI.SidorenkoCounterexample.lagrangian_card_sum line 253

    Source documentation

    Exact chart decomposition count: the vertical-annihilator stratum is retained rather than discarded as a negligible exceptional event.

     theorem lagrangian_card_sum [Fintype K] [Finite V] :
        letI := Fintype.ofFinite (Submodule K V)
    …

21. def OAI.SidorenkoCounterexample.symplecticProjection line 271
22. theorem OAI.SidorenkoCounterexample.symplecticProjection_apply line 274
23. theorem OAI.SidorenkoCounterexample.symplecticProjection_surjective line 277
24. theorem OAI.SidorenkoCounterexample.symplecticProjection_ker line 291
25. theorem OAI.SidorenkoCounterexample.exists_isotropic_section line 308

    Source documentation

    A section of the projection can be corrected by half its alternating Gram form, retaining its projection and making its image isotropic.

     theorem exists_isotropic_section (h2 : (2 : K) ≠ 0) (ha : ω.IsAlt)
        (hω : ω.Nondegenerate) (hL : ω.orthogonal L = L) :
        ∃ s : Module.Dual K L →ₗ[K] E,
          (symplecticProjection ω L).comp s = LinearMap.id ∧
          ∀ f g, ω (s f) (s g) = 0 := by
    …

    Mentions: OAI.SidorenkoCounterexample.symplecticProjection

26. theorem OAI.SidorenkoCounterexample.exists_lagrangian_coordinates line 342

    Source documentation

    Relative Darboux coordinates for any fixed Lagrangian. No transitivity or symplectic basis theorem is assumed.

     theorem exists_lagrangian_coordinates (h2 : (2 : K) ≠ 0) (ha : ω.IsAlt)
        (hω : ω.Nondegenerate) (hL : ω.orthogonal L = L) :
        ∃ e : (L × Module.Dual K L) ≃ₗ[K] E,
          (∀ l : L, e (l,0) = l.val) ∧
          ∀ x y, ω (e x) (e y) = canonicalSymplectic x y := by
    …

    Mentions: OAI.SidorenkoCounterexample.canonicalSymplectic

27. theorem OAI.SidorenkoCounterexample.self_orthogonal_twice_finrank line 394
28. theorem OAI.SidorenkoCounterexample.lagrangian_transitivity line 403

    Source documentation

    Isometries act transitively on Lagrangians, proved by the corrected sections above. This is needed to use uniform pair laws in the planted model.

     theorem lagrangian_transitivity (h2 : (2 : K) ≠ 0) (ha : ω.IsAlt)
        (hω : ω.Nondegenerate) (hL : ω.orthogonal L = L)
        (M : Submodule K E) (hM : ω.orthogonal M = M) :
        ∃ e : E ≃ₗ[K] E, (∀ x y, ω (e x) (e y) = ω x y) ∧ L.map e.toLinearMap = M := by
    …

29. theorem OAI.SidorenkoCounterexample.orthogonal_map_of_isometry line 443

    Source documentation

    Orthogonal complement commutes with any form-preserving equivalence.

     theorem orthogonal_map_of_isometry (e : E ≃ₗ[K] E)
        (he : ∀ x y, ω (e x) (e y) = ω x y) (U : Submodule K E) :
        ω.orthogonal (U.map e.toLinearMap) = (ω.orthogonal U).map e.toLinearMap := by
    …

30. def OAI.SidorenkoCounterexample.lagrangianIsometryEquiv line 458
31. def OAI.SidorenkoCounterexample.verticalSpace line 476
32. theorem OAI.SidorenkoCounterexample.mem_verticalSpace line 480
33. theorem OAI.SidorenkoCounterexample.verticalSpace_graph line 484
34. def OAI.SidorenkoCounterexample.verticalLagrangian line 497
35. def OAI.SidorenkoCounterexample.graphVerticalIntersectionEquiv line 502
36. theorem OAI.SidorenkoCounterexample.graph_vertical_intersection_finrank line 522
37. def OAI.SidorenkoCounterexample.pairStratumEquiv line 531

    Source documentation

    The exact stratum bijection for the intersection with a coordinate Lagrangian: dimension h is neither approximated nor dropped.

    noncomputable def pairStratumEquiv (h : ℕ) (hh : h ≤ finrank K V) :
        (Σ U : {U : Submodule K V // finrank K U = finrank K V-h}, SymForm K U.val) ≃
        {L : Lagrangian (K := K) (V := V) // finrank K ↥(L.val ⊓ verticalSpace (K := K) (V := V)) = h} := by
    …

    Mentions: OAI.SidorenkoCounterexample.SymForm, OAI.SidorenkoCounterexample.Lagrangian, OAI.SidorenkoCounterexample.verticalSpace

38. theorem OAI.SidorenkoCounterexample.vertical_pair_count line 563
39. theorem OAI.SidorenkoCounterexample.pair_stratum_card_congr line 578
40. theorem OAI.SidorenkoCounterexample.lagrangian_pair_count line 595
41. theorem OAI.SidorenkoCounterexample.linear_functional_descend line 614
42. theorem OAI.SidorenkoCounterexample.linear_functional_glue line 631
43. def OAI.SidorenkoCounterexample.graphDifference line 660
44. def OAI.SidorenkoCounterexample.graphPairProjection line 664
45. theorem OAI.SidorenkoCounterexample.graphPairProjection_surjective line 685
46. def OAI.SidorenkoCounterexample.graphPairKernelEquiv line 696
47. theorem OAI.SidorenkoCounterexample.graph_pair_intersection_finrank line 730