OAI/Computability/MaxCut/Games/KMSAnalyticHybridEnergyImageSplit.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Partition frequencies by their actual image

A map with image W is uniquely a surjection onto W, followed by the subspace inclusion. Consequently a sum over rank-q frequencies splits exactly over dimension-q image subspaces and surjections onto each image. The identities hold for arbitrary real weights and use no analytic estimate.

  1. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.range_subtype_comp_of_surjective line 26

    Source documentation

    The inclusion of the target subspace preserves the prescribed image of a surjective map.

    theorem range_subtype_comp_of_surjective (W : Submodule R U)
    (z : B →ₗ[R] W) (hz : Function.Surjective z) :
    (W.subtype.comp z).range = W := by
…
  2. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.fixedImageEquivSurjection line 38

    Source documentation

    The full fixed-image fiber, with its canonical surjective coordinates.

    def fixedImageEquivSurjection (W : Submodule R U) :
    {z : B →ₗ[R] U // z.range = W} ≃
      {z : B →ₗ[R] W // Function.Surjective z} where
…
  3. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.fixedImageEquivSurjection_symm_val line 59
  4. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.fixedImageEquivSurjection_apply_coe line 63
  5. abbrev OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency line 68

    Source documentation

    Frequencies of an exact rank.

    abbrev ImageRankFrequency (q : ℕ) :=
…
  6. abbrev OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.RankImage line 72

    Source documentation

    Actual image subspaces of the required dimension.

    abbrev RankImage (R U : Type*) [Ring R] [AddCommGroup U] [Module R U] (q : ℕ) :=
…
  7. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.frequencyImage line 76

    Source documentation

    The image classification of an exact-rank frequency.

    def frequencyImage (q : ℕ) (z : ImageRankFrequency (R := R) (B := B) (U := U) q) :
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency

  8. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.frequencyImageFiberEquiv line 80

    Source documentation

    Removing the redundant rank certificate from a fixed-image fiber.

    def frequencyImageFiberEquiv (q : ℕ) (W : RankImage R U q) :
    {z : ImageRankFrequency (R := R) (B := B) (U := U) q // frequencyImage q z = W} ≃
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.RankImage, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.frequencyImage

  9. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.rankFrequencyImageEquiv line 90

    Source documentation

    Exact rank frequencies are in bijection with a choice of actual image and a surjective map onto it.

    def rankFrequencyImageEquiv (q : ℕ) :
    ImageRankFrequency (R := R) (B := B) (U := U) q ≃
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency

  10. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.rankFrequencyImageEquiv_symm_val line 97
  11. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sum_fixedImage_eq_sum_surjection line 108

    Source documentation

    Exact fixed-image reindexing for arbitrary real weights.

    theorem sum_fixedImage_eq_sum_surjection (W : Submodule R U)
    (weight : (B →ₗ[R] U) → ℝ) :
    (∑ z : {z : B →ₗ[R] U // z.range = W}, weight z.val) =
      ∑ z : {z : B →ₗ[R] W // Function.Surjective z}, weight (W.subtype.comp z.val) := by
…
  12. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sum_rankFrequency_eq_sum_image line 118

    Source documentation

    Partition the exact-rank frequency sum by the actual image subspace.

    theorem sum_rankFrequency_eq_sum_image (q : ℕ) (weight : (B →ₗ[R] U) → ℝ) :
    (∑ z : ImageRankFrequency (R := R) (B := B) (U := U) q, weight z.val) =
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.ImageRankFrequency

  13. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sum_filter_rank_eq_sum_image line 135

    Source documentation

    The same partition in filtered-sum form, convenient for Fourier support conditions that are expressed as vanishing away from one rank.

    theorem sum_filter_rank_eq_sum_image (q : ℕ) (weight : (B →ₗ[R] U) → ℝ) :
    (∑ z : B →ₗ[R] U with Module.finrank R z.range = q, weight z) =
      ∑ W : RankImage R U q,
        ∑ z : {z : B →ₗ[R] W.val // Function.Surjective z},
          weight (W.val.subtype.comp z.val) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.RankImage

  14. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sum_eq_sum_image_of_rank_support line 147

    Source documentation

    If a weight vanishes outside rank q, the full sum has the same exact image partition. No positivity assumption on the weight is needed.

    theorem sum_eq_sum_image_of_rank_support (q : ℕ) (weight : (B →ₗ[R] U) → ℝ)
    (hsupport : ∀ z, Module.finrank R z.range ≠ q → weight z = 0) :
    (∑ z : B →ₗ[R] U, weight z) =
      ∑ W : RankImage R U q,
        ∑ z : {z : B →ₗ[R] W.val // Function.Surjective z},
          weight (W.val.subtype.comp z.val) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.RankImage

  15. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageCoordinates line 165

    Source documentation

    Coordinates adapted to a prescribed image and any chosen complement.

    def imageCoordinates (W D : Submodule K V) (h : IsCompl W D) : V ≃ₗ[K] (W × D) :=
…
  16. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageCoordinates_subtype line 169

    Source documentation

    Vectors in the prescribed image have zero complementary coordinate.

    @[simp] theorem imageCoordinates_subtype (W D : Submodule K V) (h : IsCompl W D)
    (w : W) : imageCoordinates W D h (w : V) = (w, 0) :=
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageCoordinates

  17. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageCoordinates_frequency line 175

    Source documentation

    Each fixed-image frequency has exactly the block form used by the compressed Hybrid-coordinate parametrization.

    theorem imageCoordinates_frequency {X : Type*} [AddCommGroup X] [Module K X]
    (W D : Submodule K V) (h : IsCompl W D) (z : X →ₗ[K] W) :
    (imageCoordinates W D h).toLinearMap.comp (W.subtype.comp z) =
      z.prod (0 : X →ₗ[K] D) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageCoordinates

  18. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageCoordinates_finrank line 184

    Source documentation

    A complement contributes exactly the remaining ambient dimension.

    theorem imageCoordinates_finrank [FiniteDimensional K V]
    (W D : Submodule K V) (h : IsCompl W D) :
    Module.finrank K W + Module.finrank K D = Module.finrank K V := by
…
  19. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.exists_imageCoordinates line 190

    Source documentation

    Every image subspace admits the required product coordinates.

    theorem exists_imageCoordinates (W : Submodule K V) :
    ∃ D : Submodule K V, ∃ e : V ≃ₗ[K] (W × D), ∀ w : W, e (w : V) = (w, 0) := by
…
  20. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.compressBlock line 207

    Source documentation

    The chosen block compression: restrict to B, then forget A.

    def compressBlock (S : (B × C) →ₗ[R] (A × (W × D))) : B →ₗ[R] (W × D) :=
…
  21. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.compressBlock_apply line 210
  22. structure OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.Coordinates line 215

    Source documentation

    Coordinates of a map whose compression is (z,0).

    structure Coordinates (z : B →ₗ[R] W) where
…
  23. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.Coordinates.ext line 221
  24. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.assemble line 231

    Source documentation

    Assemble the three blocks. The last coordinate vanishes on B.

    def assemble {z : B →ₗ[R] W} (p : Coordinates (A := A) (D := D) (C := C) z) :
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.Coordinates

  25. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.assemble_apply line 235
  26. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.compressBlock_assemble line 239
  27. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.extract line 249

    Source documentation

    Extract the unique coordinates from an actual compressed-fiber element.

    def extract (z : B →ₗ[R] W)
    (S : {S : (B × C) →ₗ[R] (A × (W × D)) //
      compressBlock S = z.prod (0 : B →ₗ[R] D)}) :
    Coordinates (A := A) (D := D) (C := C) z where
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.compressBlock, OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.Coordinates

  28. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.assemble_extract line 262
  29. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.extract_assemble line 281
  30. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.compressedFiberEquiv line 296

    Source documentation

    An exact compressed-fiber parametrization, valid over any ring.

    def compressedFiberEquiv (z : B →ₗ[R] W) :
    {S : (B × C) →ₗ[R] (A × (W × D)) //
      compressBlock S = z.prod (0 : B →ₗ[R] D)} ≃
      Coordinates (A := A) (D := D) (C := C) z where
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.compressBlock, OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.Coordinates

  31. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.assemble_injective line 307

    Source documentation

    Equality of assembled maps forces equality of every chosen coordinate; there are no hidden change-of-basis fibers in this parametrization.

    theorem assemble_injective (z : B →ₗ[R] W) :
    Function.Injective (assemble (R := R) (A := A) (D := D) (C := C) (z := z)) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.assemble

  32. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.psi_split_inline_KMSAnalyticHybridCoordinatesConditions line 334
  33. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.hybrid_assemble_iff line 347

    Source documentation

    The genuine hybrid selector is exactly the two independent coordinate conditions. In particular the full-rank coordinate condition does not depend on the chosen injective map into the complementary target.

    theorem hybrid_assemble_iff {z : B →ₗ[R] W}
    (p : Coordinates (A := A) (D := D) (C := C) z)
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.Coordinates

  34. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.fullCoordinates line 431

    Source documentation

    The small frequency map before its last coordinate is embedded into D.

    def fullCoordinates {z : B →ₗ[R] W}
    (p : Coordinates (A := A) (D := D) (C := C) z) :
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.Coordinates

  35. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.embedLast line 437

    Source documentation

    The injection chosen by the last block, keeping the first two blocks fixed.

    def embedLast (v : C →ₗ[R] D) : (A × (W × C)) →ₗ[R] (A × (W × D)) :=
…
  36. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.embedLast_apply line 440
  37. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.embedLast_injective line 443
  38. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.assemble_eq_embedLast_comp line 453
  39. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.range_assemble_of_fullCoordinates_surjective line 460
  40. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.finrank_assemble line 467
  41. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.ker_assemble line 474
  42. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.hybridFiberEquiv line 498

    Source documentation

    The exact coordinate parametrization after imposing the genuine hybrid selector. The two remaining conditions are ordinary injectivity and surjectivity of displayed linear maps.

    def hybridFiberEquiv (z : B →ₗ[R] W) (hz : Function.Surjective z) :
    {S : (B × C) →ₗ[R] (A × (W × D)) //
      compressBlock S = z.prod (0 : B →ₗ[R] D) ∧
        LinearIdentities.Hybrid S
          (LinearMap.range (LinearMap.inl R A (W × D)))
          (LinearMap.range (LinearMap.inl R B C))} ≃
      {p : Coordinates (A := A) (D := D) (C := C) z //
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.compressBlock, OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.Coordinates

  43. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.hybridFiber_finrank line 520

    Source documentation

    Every map in the actual fiber has the prescribed small rank.

    theorem hybridFiber_finrank (z : B →ₗ[R] W) (hz : Function.Surjective z)
    (S : (B × C) →ₗ[R] (A × (W × D)))
    (hc : compressBlock S = z.prod (0 : B →ₗ[R] D))
    (hh : LinearIdentities.Hybrid S
      (LinearMap.range (LinearMap.inl R A (W × D)))
      (LinearMap.range (LinearMap.inl R B C))) :
    Module.finrank R S.range = Module.finrank R (A × (W × C)) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridCoordinates.compressBlock

  44. def OAI.MaxCutGames.Inverse.KMSAnalytic.smallCoeff line 558

    Source documentation

    The Fourier array of the small full-rank component.

    def smallCoeff (ι : I →ₗ[F2] E) (f : (E →ₗ[F2] F) → ℝ)
    (T : F →ₗ[F2] I) : ℝ :=
…
  45. def OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent line 564

    Source documentation

    A genuine function on the small primal matrix space, synthesized in its own orthonormal trace-character basis.

    def smallComponent (ι : I →ₗ[F2] E) (f : (E →ₗ[F2] F) → ℝ) :
    (I →ₗ[F2] F) → ℝ := synthesis (smallCoeff ι f)
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.synthesis, OAI.MaxCutGames.Inverse.KMSAnalytic.smallCoeff

  46. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.coeff_smallComponent line 568
  47. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.coeff_smallComponent_of_surjective line 574
  48. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.coeff_smallComponent_of_not_surjective line 581
  49. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_energy line 589

    Source documentation

    Exact normalization: primal expectation equals an unnormalized sum over surjective small-space frequencies.

    theorem smallComponent_energy (ι : I →ₗ[F2] E) (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, smallComponent ι f X ^ 2) =
      ∑ T ∈ Finset.univ.filter (fun T : F →ₗ[F2] I => Function.Surjective T),
        linearCoeff f (ι.comp T) ^ 2 := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent

  50. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.rankComponent_smallComponent line 600

    Source documentation

    Every retained frequency has rank equal to the small domain dimension.

    theorem rankComponent_smallComponent (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) :
    rankComponent (Module.finrank F2 I) (smallComponent ι f) = smallComponent ι f := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.rankComponent, OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent

  51. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.ker_comp_of_injective line 614

    Source documentation

    Composition with an injection preserves the actual kernel.

    theorem ker_comp_of_injective (ι : I →ₗ[F2] E) (hι : Function.Injective ι)
    (T : F →ₗ[F2] I) : (ι.comp T).ker = T.ker :=
…
  52. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallCoeff_eq_of_kernel_coeff_const line 621

    Source documentation

    The small Fourier array is independent of the chosen injection once the large function's actual coefficients are proved constant on kernel classes.

    theorem smallCoeff_eq_of_kernel_coeff_const (ι κ : I →ₗ[F2] E)
    (hι : Function.Injective ι) (hκ : Function.Injective κ)
    (f : (E →ₗ[F2] F) → ℝ)
    (hcoeff : ∀ S T : F →ₗ[F2] E,
      S.ker = T.ker → linearCoeff f S = linearCoeff f T) :
    smallCoeff ι f = smallCoeff κ f := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.smallCoeff

  53. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_eq_of_kernel_coeff_const line 638

    Source documentation

    Equality is of the actual synthesized functions, not merely their norms.

    theorem smallComponent_eq_of_kernel_coeff_const (ι κ : I →ₗ[F2] E)
    (hι : Function.Injective ι) (hκ : Function.Injective κ)
    (f : (E →ₗ[F2] F) → ℝ)
    (hcoeff : ∀ S T : F →ₗ[F2] E,
      S.ker = T.ker → linearCoeff f S = linearCoeff f T) :
    smallComponent ι f = smallComponent κ f :=
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent

  54. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_orthogonal line 649

    Source documentation

    A small component is orthogonal to any small-space function whose full rank coefficients vanish.

    theorem smallComponent_orthogonal (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (g : (I →ₗ[F2] F) → ℝ)
    (hg : ∀ T : F →ₗ[F2] I, Function.Surjective T → linearCoeff g T = 0) :
    (𝔼 X, smallComponent ι f X * g X) = 0 := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent

  55. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_energy_le line 662

    Source documentation

    Injective frequency lifting cannot increase the total squared norm.

    theorem smallComponent_energy_le (ι : I →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, smallComponent ι f X ^ 2) ≤ 𝔼 X, f X ^ 2 := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent