OAI/Computability/MaxCut/Games/CoordinateTransport.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Exact compression fibers for arbitrary binary linear maps

This is the general cardinality assertion in Lemma A.2, with the actual kernel restriction and range quotient. The map X is arbitrary; no chosen-coordinate or fixed-dimension hypothesis occurs in card_fiber.

  1. def OAI.MaxCutGames.Appendix.CoordinateTransport.complementRangeEquiv line 14

    Source documentation

    A complement to the kernel maps isomorphically onto the range.

    def complementRangeEquiv (X : E โ†’โ‚—[๐•œ] F) (P : Submodule ๐•œ E)
    (hP : IsCompl X.ker P) : P โ‰ƒโ‚—[๐•œ] X.range :=
โ€ฆ
  2. theorem OAI.MaxCutGames.Appendix.CoordinateTransport.complementRangeEquiv_apply line 18
  3. def OAI.MaxCutGames.Appendix.CoordinateTransport.domainEquiv line 24

    Source documentation

    Domain coordinates, with the first coordinate literally in range X.

    def domainEquiv (X : E โ†’โ‚—[๐•œ] F) (P : Submodule ๐•œ E)
    (hP : IsCompl X.ker P) : (X.range ร— X.ker) โ‰ƒโ‚—[๐•œ] E :=
โ€ฆ
  4. theorem OAI.MaxCutGames.Appendix.CoordinateTransport.apply_domainEquiv line 30

    Source documentation

    The domain equivalence exhibits precisely the image coordinate of X.

    @[simp] theorem apply_domainEquiv (X : E โ†’โ‚—[๐•œ] F)
    (P : Submodule ๐•œ E) (hP : IsCompl X.ker P) (u : X.range) (k : X.ker) :
    X (domainEquiv X P hP (u, k)) = (u : F) := by
โ€ฆ

    Mentions: OAI.MaxCutGames.Appendix.CoordinateTransport.domainEquiv

  5. def OAI.MaxCutGames.Appendix.CoordinateTransport.codomainEquiv line 40

    Source documentation

    Codomain coordinates split the range off from a chosen complement.

    def codomainEquiv (X : E โ†’โ‚—[๐•œ] F) (C : Submodule ๐•œ F)
    (hC : IsCompl X.range C) : (X.range ร— C) โ‰ƒโ‚—[๐•œ] F :=
โ€ฆ
  6. theorem OAI.MaxCutGames.Appendix.CoordinateTransport.canonical_block line 45

    Source documentation

    An arbitrary map has the canonical compression-fiber block form.

    theorem canonical_block (X : E โ†’โ‚—[๐•œ] F) (P : Submodule ๐•œ E)
    (hP : IsCompl X.ker P) (C : Submodule ๐•œ F)
    (hC : IsCompl X.range C) (u : X.range) (k : X.ker) :
    (codomainEquiv X C hC).symm (X (domainEquiv X P hP (u, k))) = (u, 0) := by
โ€ฆ

    Mentions: OAI.MaxCutGames.Appendix.CoordinateTransport.codomainEquiv, OAI.MaxCutGames.Appendix.CoordinateTransport.domainEquiv

  7. theorem OAI.MaxCutGames.Appendix.CoordinateTransport.exists_canonical_coordinates line 54

    Source documentation

    Choice of complements is available over every field; this is an actual normal-form existence result, including zero-dimensional kernel/range cases.

    theorem exists_canonical_coordinates (X : E โ†’โ‚—[๐•œ] F) :
    โˆƒ (P : Submodule ๐•œ E) (C : Submodule ๐•œ F)
      (hP : IsCompl X.ker P) (hC : IsCompl X.range C),
      โˆ€ (u : X.range) (k : X.ker),
        (codomainEquiv X C hC).symm (X (domainEquiv X P hP (u, k))) = (u, 0) := by
โ€ฆ

    Mentions: OAI.MaxCutGames.Appendix.CoordinateTransport.codomainEquiv, OAI.MaxCutGames.Appendix.CoordinateTransport.domainEquiv

  8. theorem OAI.MaxCutGames.Appendix.CoordinateTransport.domainEquiv_zero_left line 63
  9. theorem OAI.MaxCutGames.Appendix.CoordinateTransport.quotient_coordinates line 69
  10. def OAI.MaxCutGames.Appendix.CoordinateTransport.toBlocks line 76

    Source documentation

    Re-express all maps in the chosen domain/codomain coordinates at once.

    def toBlocks (X : E โ†’โ‚—[๐•œ] F) (P : Submodule ๐•œ E)
    (hP : IsCompl X.ker P) (C : Submodule ๐•œ F) (hC : IsCompl X.range C) :
    (E โ†’โ‚—[๐•œ] F) โ‰ƒโ‚—[๐•œ] ((X.range ร— X.ker) โ†’โ‚—[๐•œ] (X.range ร— C)) :=
โ€ฆ
  11. theorem OAI.MaxCutGames.Appendix.CoordinateTransport.toBlocks_apply line 81
  12. theorem OAI.MaxCutGames.Appendix.CoordinateTransport.compressed_toBlocks line 90

    Source documentation

    The lower-right block is exactly the original quotient restriction, transported through the quotient/complement equivalence.

    theorem compressed_toBlocks (X Y : E โ†’โ‚—[๐•œ] F) (P : Submodule ๐•œ E)
    (hP : IsCompl X.ker P) (C : Submodule ๐•œ F) (hC : IsCompl X.range C)
    (k : X.ker) :
    (toBlocks X P hP C hC Y (0, k)).2 =
      X.range.quotientEquivOfIsCompl C hC (X.range.mkQ (Y k)) := by
โ€ฆ

    Mentions: OAI.MaxCutGames.Appendix.CoordinateTransport.toBlocks

  13. theorem OAI.MaxCutGames.Appendix.CoordinateTransport.toBlocks_base line 97
  14. def OAI.MaxCutGames.Appendix.CoordinateTransport.rangeTransport line 111

    Source documentation

    Changing coordinates induces a genuine linear equivalence on ranges.

    def rangeTransport (e : E โ‰ƒโ‚—[๐•œ] U) (f : F โ‰ƒโ‚—[๐•œ] V) (Y : E โ†’โ‚—[๐•œ] F) :
    Y.range โ‰ƒโ‚—[๐•œ] (LinearEquiv.arrowCongr e f Y).range where
โ€ฆ
  15. theorem OAI.MaxCutGames.Appendix.CoordinateTransport.finrank_range_transport line 126
  16. theorem OAI.MaxCutGames.Appendix.CoordinateTransport.finrank_toBlocks line 134
  17. theorem OAI.MaxCutGames.Appendix.CoordinateTransport.finrank_comp_equiv line 140
  18. def OAI.MaxCutGames.Appendix.FullCompression.compression line 167

    Source documentation

    Restrict a dual map to ker X and then quotient by range X.

    def compression (X Y : E โ†’โ‚—[F2] F) : X.ker โ†’โ‚—[F2] (F โงธ X.range) :=
โ€ฆ
  19. theorem OAI.MaxCutGames.Appendix.FullCompression.compression_apply line 171
  20. def OAI.MaxCutGames.Appendix.FullCompression.Fiber line 176

    Source documentation

    The genuine rank-additive compression fiber. In characteristic two, Y - X and Y + X are equal.

    def Fiber (X : E โ†’โ‚—[F2] F) (Z : X.ker โ†’โ‚—[F2] (F โงธ X.range)) :=
โ€ฆ
  21. theorem OAI.MaxCutGames.Appendix.FullCompression.fiber_condition_iff line 181
  22. def OAI.MaxCutGames.Appendix.FullCompression.fiberEquiv line 218

    Source documentation

    Coordinate transport is a bijection on the complete rank-additive fibers.

    def fiberEquiv (X : E โ†’โ‚—[F2] F) (Z : X.ker โ†’โ‚—[F2] (F โงธ X.range))
    (P : Submodule F2 E) (hP : IsCompl X.ker P)
    (C : Submodule F2 F) (hC : IsCompl X.range C) :
    Fiber X Z โ‰ƒ CompressionCount.Fiber (U := X.range)
โ€ฆ

    Mentions: OAI.MaxCutGames.Appendix.FullCompression.Fiber, OAI.MaxCutGames.Appendix.CompressionCount.Fiber

  23. theorem OAI.MaxCutGames.Appendix.FullCompression.card_fiber line 229

    Source documentation

    Lemma A.2: every compressed rank-r map has exactly 2^(2*k*r) rank-additive lifts above an arbitrary rank-k map X.

    theorem card_fiber (X : E โ†’โ‚—[F2] F) (Z : X.ker โ†’โ‚—[F2] (F โงธ X.range)) :
    Nat.card (Fiber X Z) = 2 ^ (2 * finrank F2 X.range * finrank F2 Z.range) := by
โ€ฆ

    Mentions: OAI.MaxCutGames.Appendix.FullCompression.Fiber

  24. theorem OAI.MaxCutGames.Appendix.FullCompression.fiber_rank line 238

    Source documentation

    Every member of a compression fiber has rank rank X + rank Z.

    theorem fiber_rank (X : E โ†’โ‚—[F2] F)
    (Z : X.ker โ†’โ‚—[F2] (F โงธ X.range)) (Y : Fiber X Z) :
    finrank F2 Y.val.range = finrank F2 X.range + finrank F2 Z.range := by
โ€ฆ

    Mentions: OAI.MaxCutGames.Appendix.FullCompression.Fiber

  25. theorem OAI.MaxCutGames.Appendix.FiberEnergy.finite_fiber_energy line 272

    Source documentation

    The energy of a sum of merged coefficients is bounded by the largest fiber size times the original coefficient energy. Signs and cancellations are unrestricted; no injectivity assumption is made.

    theorem finite_fiber_energy (s : Finset ฮฑ) (compress : ฮฑ โ†’ ฮฒ) (a : ฮฑ โ†’ R)
    (bound : R) (hbound : โˆ€ z,
      ((s.filter (fun y => compress y = z)).card : R) โ‰ค bound) :
    (โˆ‘ z, (โˆ‘ y โˆˆ s.filter (fun y => compress y = z), a y) ^ 2) โ‰ค
      bound * โˆ‘ y โˆˆ s, a y ^ 2 := by
โ€ฆ
  26. theorem OAI.MaxCutGames.Appendix.DerivativeEnergy.supported_fiber_energy line 313
  27. theorem OAI.MaxCutGames.Appendix.DerivativeEnergy.coefficient_energy line 361

    Source documentation

    The precise merged-coefficient form of (A.10). Coefficients are arbitrary real numbers with the stated degree support, not assumed nonnegative.

    theorem coefficient_energy (X : E โ†’โ‚—[F2] F)
    [Fintype (X.ker โ†’โ‚—[F2] (F โงธ X.range))]
    (a : (E โ†’โ‚—[F2] F) โ†’ โ„) (d : Nat)
    (hdegree : โˆ€ Y, d < finrank F2 Y.range โ†’ a Y = 0) :
    (โˆ‘ Z, (โˆ‘ Y, if RankBelow X Y โˆง FullCompression.compression X Y = Z
      then a Y else 0)^2) โ‰ค
      (2 : โ„)^(2 * finrank F2 X.range * (d - finrank F2 X.range)) *
        โˆ‘ Y, if RankBelow X Y then a Y^2 else 0 := by
โ€ฆ

    Mentions: OAI.MaxCutGames.Appendix.FullCompression.compression

  28. def OAI.MaxCutGames.Appendix.SubspaceCounting.generators line 410
  29. theorem OAI.MaxCutGames.Appendix.SubspaceCounting.span_generators line 414
  30. theorem OAI.MaxCutGames.Appendix.SubspaceCounting.card_subspaces_rank_le line 422

    Source documentation

    A k-subspace is determined by a chosen ordered k-tuple of spanning vectors.

    theorem card_subspaces_rank_le [Finite V] (k : โ„•) :
    Nat.card {S : Submodule K V // finrank K S = k} โ‰ค Nat.card V ^ k := by
โ€ฆ
  31. theorem OAI.MaxCutGames.Appendix.SubspaceCounting.card_subspaces_rank_le_field_power line 438

    Source documentation

    General finite-field form of the image-choice estimate in A.4.

    theorem card_subspaces_rank_le_field_power [Finite K] (k : โ„•) :
    Nat.card {S : Submodule K V // finrank K S = k} โ‰ค
      Nat.card K ^ (finrank K V * k) := by
โ€ฆ
  32. theorem OAI.MaxCutGames.Appendix.SubspaceCounting.card_binary_subspaces_rank_le line 448

    Source documentation

    Binary specialization: the ambient dimension is the dimension of Y's image, not the potentially much larger original vector space.

    theorem card_binary_subspaces_rank_le
    {V : Type*} [AddCommGroup V] [Module (ZMod 2) V] [Module.Finite (ZMod 2) V]
    (d k : โ„•) (hd : finrank (ZMod 2) V โ‰ค d) :
    Nat.card {S : Submodule (ZMod 2) V // finrank (ZMod 2) S = k} โ‰ค
      2 ^ (d * k) := by
โ€ฆ
  33. theorem OAI.MaxCutGames.Appendix.SubspaceCounting.card_linearMaps_le line 464

    Source documentation

    Evaluating on a basis bounds the number of linear maps without counting arbitrary functions on every vector.

    theorem card_linearMaps_le [Finite V] :
    Nat.card (U โ†’โ‚—[K] V) โ‰ค Nat.card V ^ finrank K U := by
โ€ฆ
  34. theorem OAI.MaxCutGames.Appendix.SubspaceCounting.exists_rank_factorization line 476

    Source documentation

    Every rank-k map factors through the actual coordinate vector space K^k.

    theorem exists_rank_factorization (f : U โ†’โ‚—[K] V) (k : โ„•)
    (hk : finrank K (LinearMap.range f) = k) :
    โˆƒ (a : (Fin k โ†’ K) โ†’โ‚—[K] V) (b : U โ†’โ‚—[K] (Fin k โ†’ K)), a.comp b = f := by
โ€ฆ
  35. theorem OAI.MaxCutGames.Appendix.SubspaceCounting.card_rank_maps_le line 488

    Source documentation

    Rank-k maps between r- and s-dimensional spaces number at most |K|^((r+s)k). This is a general finite-field bound, proved by selecting the preceding factorization and injecting into the pair of factor maps.

    theorem card_rank_maps_le [Finite K] (k : โ„•) :
    Nat.card {f : U โ†’โ‚—[K] V // finrank K (LinearMap.range f) = k} โ‰ค
      Nat.card K ^ ((finrank K U + finrank K V) * k) := by
โ€ฆ
  36. def OAI.MaxCutGames.Appendix.SubspaceCounting.quotientImageMap line 528

    Source documentation

    Factor a map whose kernel contains ker Y and whose image lies in range Y through the effective domain and codomain.

    def quotientImageMap (Y X : U โ†’โ‚—[K] V)
    (hker : LinearMap.ker Y โ‰ค LinearMap.ker X)
    (himage : LinearMap.range X โ‰ค LinearMap.range Y) :
    (U โงธ LinearMap.ker Y) โ†’โ‚—[K] LinearMap.range Y :=
โ€ฆ
  37. theorem OAI.MaxCutGames.Appendix.SubspaceCounting.quotientImageMap_mk line 538
  38. theorem OAI.MaxCutGames.Appendix.SubspaceCounting.rank_quotientImageMap line 544
  39. theorem OAI.MaxCutGames.Appendix.SubspaceCounting.card_constrained_maps_le line 557

    Source documentation

    General ambient-independent rank-k bound for maps constrained by the image and kernel of Y. This counts actual linear maps; neither cardinality nor rank-additive predecessor estimates are supplied as hypotheses.

    theorem card_constrained_maps_le [Finite K] (Y : U โ†’โ‚—[K] V) (k : โ„•) :
    Nat.card {X : U โ†’โ‚—[K] V // finrank K (LinearMap.range X) = k โˆง
      LinearMap.ker Y โ‰ค LinearMap.ker X โˆง LinearMap.range X โ‰ค LinearMap.range Y} โ‰ค
      Nat.card K ^ (2 * finrank K (LinearMap.range Y) * k) := by
โ€ฆ
  40. theorem OAI.MaxCutGames.Appendix.SubspaceCounting.binary_add_cancel line 601
  41. theorem OAI.MaxCutGames.Appendix.SubspaceCounting.card_binary_predecessors_le line 609
  42. lemma OAI.MaxCutGames.Appendix.WeightedFourthMoment.half_cancel_inline_WeightedFourthMoment line 673
  43. lemma OAI.MaxCutGames.Appendix.WeightedFourthMoment.half_sum_identity_inline_WeightedFourthMoment line 678
  44. lemma OAI.MaxCutGames.Appendix.WeightedFourthMoment.half_sum_le_inline_WeightedFourthMoment line 687
  45. lemma OAI.MaxCutGames.Appendix.WeightedFourthMoment.finite_level_sum_inline_WeightedFourthMoment line 693
  46. abbrev OAI.MaxCutGames.Appendix.WeightedFourthMoment.rank line 750
  47. def OAI.MaxCutGames.Appendix.WeightedFourthMoment.vectorFintype line 752
  48. def OAI.MaxCutGames.Appendix.WeightedFourthMoment.compressedFintype line 756
  49. def OAI.MaxCutGames.Appendix.WeightedFourthMoment.energy line 763

    Source documentation

    Energy of the actual merged derivative coefficients.

    def energy (a : (E โ†’โ‚—[F2] F) โ†’ โ„) (X : E โ†’โ‚—[F2] F) : โ„ := by
โ€ฆ
  50. theorem OAI.MaxCutGames.Appendix.WeightedFourthMoment.predecessor_weight_sum line 770

    Source documentation

    Sum of predecessor weights, using the actual binary linear-map count.

    theorem predecessor_weight_sum (Y : E โ†’โ‚—[F2] F) (d : โ„•) (hd : rank Y โ‰ค d) :
    (โˆ‘ X โˆˆ Finset.univ.filter (fun X => RankBelow X Y),
      ((2:โ„)โปยน)^(4*d*rank X)) โ‰ค 2 := by
โ€ฆ

    Mentions: OAI.MaxCutGames.Appendix.WeightedFourthMoment.rank

  51. theorem OAI.MaxCutGames.Appendix.WeightedFourthMoment.weighted_fourth_coefficient_energy line 800

    Source documentation

    Corrected Appendix A.4, in exact coefficient form, for arbitrary real coefficients supported on maps of rank at most d.

    theorem weighted_fourth_coefficient_energy (a : (E โ†’โ‚—[F2] F) โ†’ โ„) (d : โ„•)
    (hdegree : โˆ€ Y, d < rank Y โ†’ a Y = 0) :
    (โˆ‘ X, ((2:โ„)โปยน)^(8*d*rank X)*(energy a X)^2) โ‰ค 2*(โˆ‘ Y, a Y^2)^2 := by
โ€ฆ

    Mentions: OAI.MaxCutGames.Appendix.WeightedFourthMoment.rank, OAI.MaxCutGames.Appendix.WeightedFourthMoment.energy