OAI/Computability/MaxCut/Games/KMSInjectionCountBounds.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Elementary dimension bounds for the actual injection count. The lower bound is intentionally loose; its exponent suffices for the KMS norm ratio.

  1. theorem OAI.MaxCutGames.Inverse.KMSInjectionCount.binary_factor_lower line 13
  2. theorem OAI.MaxCutGames.Inverse.KMSInjectionCount.beta_le_pow line 29
  3. theorem OAI.MaxCutGames.Inverse.KMSInjectionCount.beta_ge_pow line 39
  4. theorem OAI.MaxCutGames.Inverse.KMSInjectionCount.beta_positive line 52
  5. theorem OAI.MaxCutGames.Inverse.KMSInjectionCount.beta_self_le line 56
  6. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_energy_cross_mul line 97

    Source documentation

    The exact ratio is cross-multiplied, so the identity also covers zero components without any nonzero-energy premise.

    theorem smallComponent_energy_cross_mul (ι : I →ₗ[F2] E)
    (hι : Function.Injective ι) (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) :
    (beta I E : ℝ) * (𝔼 X, smallComponent ι f X ^ 2) =
      (beta I I : ℝ) * (𝔼 X, rankComponent (Module.finrank F2 I) f X ^ 2) := by
…

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

  7. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_energy_ratio line 129

    Source documentation

    Dividing by the positive, explicitly counted injection multiplicity gives the normalized small-space energy exactly.

    theorem smallComponent_energy_ratio (ι : I →ₗ[F2] E)
    (hι : Function.Injective ι) (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) :
    (𝔼 X, smallComponent ι f X ^ 2) =
      (beta I I : ℝ) / (beta I E : ℝ) *
        (𝔼 X, rankComponent (Module.finrank F2 I) f X ^ 2) := by
…

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

  8. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_energy_pow_bound line 147

    Source documentation

    An explicit dimension-only norm comparison obtained from the actual injection counts. The loose constant is sufficient for the analytic argument.

    theorem smallComponent_energy_pow_bound (ι : I →ₗ[F2] E)
    (hι : Function.Injective ι) (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) :
    (2 : ℝ) ^ (Module.finrank F2 I * (Module.finrank F2 E - Module.finrank F2 I)) *
        (𝔼 X, smallComponent ι f X ^ 2) ≤
      (2 : ℝ) ^ (Module.finrank F2 I * Module.finrank F2 I) *
        (𝔼 X, rankComponent (Module.finrank F2 I) f X ^ 2) := by
…

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

  9. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_energy_le_of_energy_le line 175

    Source documentation

    The zero-fixed-character case uses only the original function's squared norm bound. In particular it applies to a pseudorandom indicator of density at most ε, without assuming any restricted Fourier inequality.

    theorem smallComponent_energy_le_of_energy_le (ι : I →ₗ[F2] E)
    (hι : Function.Injective ι) (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) (ε : ℝ) (hε : (𝔼 X, f X ^ 2) ≤ ε) :
    (2 : ℝ) ^ (Module.finrank F2 I * (Module.finrank F2 E - Module.finrank F2 I)) *
        (𝔼 X, smallComponent ι f X ^ 2) ≤
      (2 : ℝ) ^ (Module.finrank F2 I * Module.finrank F2 I) * ε := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent

  10. theorem OAI.MaxCutGames.Inverse.KMSInjectionCount.pow_dim_mul_le_pow_sq_mul_beta line 202

    Source documentation

    A subtraction-free form of the lower injection count.

    theorem pow_dim_mul_le_pow_sq_mul_beta
    (hdim : Module.finrank F2 I ≤ Module.finrank F2 E) :
    (2 : ℝ) ^ (Module.finrank F2 I * Module.finrank F2 E) ≤
      (2 : ℝ) ^ (Module.finrank F2 I * Module.finrank F2 I) * (beta I E : ℝ) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSInjectionCount.F2, OAI.MaxCutGames.Inverse.KMSInjectionCount.beta

  11. theorem OAI.MaxCutGames.Inverse.KMSInjectionCount.beta_ratio_le_pow line 220

    Source documentation

    The small-to-ambient injection ratio, with the full ambient exponent.

    theorem beta_ratio_le_pow [Finite I]
    (hdim : Module.finrank F2 I ≤ Module.finrank F2 E) :
    (beta I I : ℝ) / (beta I E : ℝ) ≤
      (2 : ℝ) ^ (2 * (Module.finrank F2 I * Module.finrank F2 I)) /
        (2 : ℝ) ^ (Module.finrank F2 I * Module.finrank F2 E) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSInjectionCount.F2, OAI.MaxCutGames.Inverse.KMSInjectionCount.beta

  12. theorem OAI.MaxCutGames.Inverse.KMSInjectionCount.pow_mul_le_of_beta_cross_mul line 247

    Source documentation

    Convert a count-weighted energy identity into a clean dimension bound.

    theorem pow_mul_le_of_beta_cross_mul [Finite I]
    (hdim : Module.finrank F2 I ≤ Module.finrank F2 E)
    {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y)
    (hcross : (beta I E : ℝ) * x = (beta I I : ℝ) * y) :
    (2 : ℝ) ^ (Module.finrank F2 I * Module.finrank F2 E) * x ≤
      (2 : ℝ) ^ (2 * (Module.finrank F2 I * Module.finrank F2 I)) * y := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSInjectionCount.F2, OAI.MaxCutGames.Inverse.KMSInjectionCount.beta

  13. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_energy_base_bound line 298
  14. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_zero_dim_bound line 325

    Source documentation

    In a zero-dimensional partial codomain every prescribed frequency is the unique one, so the base sum is exactly the small-component squared norm.

    theorem fixedFrequencyEnergy_zero_dim_bound (ι : I →ₗ[F2] E)
    (hι : Function.Injective ι) (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) (ε : ℝ)
    (hg : HomogeneousRestrictionBound (Module.finrank F2 I) ε f)
    (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) (hJ : Module.finrank F2 J = 0) :
    (2 : ℝ) ^ ((Module.finrank F2 I + Module.finrank F2 J) * Module.finrank F2 E) *
        fixedFrequencyEnergy ι f π A ≤
      (2 : ℝ) ^ (4 * Module.finrank F2 I * Module.finrank F2 I) * ε := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound, OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy

  15. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.character_codomain_composition line 362

    Source documentation

    Restricting the codomain of a primal map restricts the domain of its dual frequency. This identity is independent of the choice of bases.

    theorem character_codomain_composition (J : B →ₗ[F2] F)
    (S : F →ₗ[F2] E) (X : E →ₗ[F2] B) :
    linearTraceCharacter S (J.comp X) = linearTraceCharacter (S.comp J) X := by
…
  16. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.coefficient_codomain_pullback line 377

    Source documentation

    Coefficients of the actual restricted function are the unnormalized sum over exactly those original frequencies whose restriction is the new one. The statement allows arbitrary linear J; injections are the KMS use case.

    theorem coefficient_codomain_pullback (J : B →ₗ[F2] F)
    (f : (E →ₗ[F2] F) → ℝ) (T : B →ₗ[F2] E) :
    linearCoeff (fun X => f (J.comp X)) T =
      ∑ S : F →ₗ[F2] E, if S.comp J = T then linearCoeff f S else 0 := by
…
  17. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.coefficient_codomain_pullback_fiber line 398

    Source documentation

    The same merging identity on the actual fiber type. This form is ready for the hyperplane extension bijection, without changing normalization.

    theorem coefficient_codomain_pullback_fiber (J : B →ₗ[F2] F)
    (f : (E →ₗ[F2] F) → ℝ) (T : B →ₗ[F2] E) :
    linearCoeff (fun X => f (J.comp X)) T =
      ∑ S : {S : F →ₗ[F2] E // S.comp J = T}, linearCoeff f S.val := by
…
  18. def OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend line 439

    Source documentation

    Extend a frequency by specifying its value on the new coordinate.

    def hyperplaneExtend (z : B →ₗ[F2] E) (v : E) : (B × F2) →ₗ[F2] E :=
…
  19. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend_apply line 442
  20. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend_comp_inl line 445
  21. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend_new_coordinate line 449
  22. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend_recover line 453

    Source documentation

    Recover a linear map from its old coordinates and its new-coordinate value.

    theorem hyperplaneExtend_recover (S : (B × F2) →ₗ[F2] E) :
    hyperplaneExtend (S.comp (LinearMap.inl F2 B F2)) (S (0, 1)) = S := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend

  23. def OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtensionEquiv line 462

    Source documentation

    Exact parametrization of a restriction fiber, including dependent extensions.

    def hyperplaneExtensionEquiv (z : B →ₗ[F2] E) :
    E ≃ {S : (B × F2) →ₗ[F2] E // S.comp (LinearMap.inl F2 B F2) = z} where
…
  24. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend_injective line 472
  25. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.range_hyperplaneExtend line 478

    Source documentation

    The range is the old range plus the span of the new vector.

    theorem range_hyperplaneExtend (z : B →ₗ[F2] E) (v : E) :
    (hyperplaneExtend z v).range = z.range ⊔ Submodule.span F2 {v} := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend

  26. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.range_hyperplaneExtend_of_mem line 482
  27. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.ker_hyperplaneExtend_of_notMem line 488

    Source documentation

    All outside-range extensions have the same actual kernel.

    theorem ker_hyperplaneExtend_of_notMem (z : B →ₗ[F2] E) {v : E}
    (hv : v ∉ z.range) :
    (hyperplaneExtend z v).ker = z.ker.prod (⊥ : Submodule F2 F2) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend

  28. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.coefficient_hyperplaneExtend_eq line 500
  29. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.card_hyperplaneExtension_outside line 512

    Source documentation

    The number of outside choices is exactly the ambient cardinality minus the old range cardinality.

    theorem card_hyperplaneExtension_outside (z : B →ₗ[F2] E) :
    (Finset.univ.filter (fun v : E => v ∉ z.range)).card =
      Fintype.card E - Fintype.card z.range := by
…
  30. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.card_hyperplaneExtension_outside_pow line 519
  31. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.sum_hyperplaneExtend_outside line 527

    Source documentation

    Exact sum of the common coefficient over all outside-range extensions.

    theorem sum_hyperplaneExtend_outside (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (z : B →ₗ[F2] E)
    {v : E} (hv : v ∉ z.range) :
    (∑ u with u ∉ z.range, linearCoeff f (hyperplaneExtend z u)) =
      ((Fintype.card E - Fintype.card z.range : ℕ) : ℝ) *
        linearCoeff f (hyperplaneExtend z v) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend

  32. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.sum_hyperplaneExtend line 542

    Source documentation

    Split the full extension fiber into dependent and independent choices.

    theorem sum_hyperplaneExtend (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (z : B →ₗ[F2] E)
    {v : E} (hv : v ∉ z.range) :
    (∑ u : E, linearCoeff f (hyperplaneExtend z u)) =
      (∑ u with u ∈ z.range, linearCoeff f (hyperplaneExtend z u)) +
      ((Fintype.card E - Fintype.card z.range : ℕ) : ℝ) *
        linearCoeff f (hyperplaneExtend z v) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend

  33. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.coefficient_hyperplaneExtend_recursion line 554

    Source documentation

    Solve the extension sum for the coefficient of an independent extension.

    theorem coefficient_hyperplaneExtend_recursion (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (z : B →ₗ[F2] E)
    {v : E} (hv : v ∉ z.range) :
    linearCoeff f (hyperplaneExtend z v) =
      ((∑ u : E, linearCoeff f (hyperplaneExtend z u)) -
        ∑ u with u ∈ z.range, linearCoeff f (hyperplaneExtend z u)) /
      ((Fintype.card E - Fintype.card z.range : ℕ) : ℝ) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend

  34. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.coefficient_hyperplane_restriction line 598

    Source documentation

    Exact codomain-restriction coefficient, reindexed by the extension vector. The sum has no cardinality normalization.

    theorem coefficient_hyperplane_restriction
    (f : (E →ₗ[F2] (B × F2)) → ℝ) (z : B →ₗ[F2] E) :
    linearCoeff (fun X => f ((LinearMap.inl F2 B F2).comp X)) z =
      ∑ u : E, linearCoeff f (hyperplaneExtend z u) := by
…
  35. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.coefficient_zoomOut_recursion line 609

    Source documentation

    KMS's genuine zoom-out recurrence, in product coordinates. The denominator is the exact number of independent extension vectors. Basis invariance is used to prove their Fourier coefficients coincide.

    theorem coefficient_zoomOut_recursion
    (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (z : B →ₗ[F2] E)
    {v : E} (hv : v ∉ z.range) :
    linearCoeff f (hyperplaneExtend z v) =
      (linearCoeff (fun X => f ((LinearMap.inl F2 B F2).comp X)) z -
        ∑ u with u ∈ z.range, linearCoeff f (hyperplaneExtend z u)) /
      ((Fintype.card E - Fintype.card z.range : ℕ) : ℝ) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant

  36. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.coefficient_zoomOut_mul line 621

    Source documentation

    A denominator-free form convenient for squared-norm estimates.

    theorem coefficient_zoomOut_mul
    (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (z : B →ₗ[F2] E)
    {v : E} (hv : v ∉ z.range) :
    ((Fintype.card E - Fintype.card z.range : ℕ) : ℝ) *
        linearCoeff f (hyperplaneExtend z v) =
      linearCoeff (fun X => f ((LinearMap.inl F2 B F2).comp X)) z -
        ∑ u with u ∈ z.range, linearCoeff f (hyperplaneExtend z u) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant

  37. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.sub_sum_sq_le_card_mul line 650

    Source documentation

    Cauchy--Schwarz with the distinguished scalar included as one extra summand. This form also handles an empty dependent branch.

    theorem sub_sum_sq_le_card_mul {C : Type*} [Fintype C]
    (x : ℝ) (a : C → ℝ) :
    (x - ∑ c, a c) ^ 2 ≤
      ((Fintype.card C : ℝ) + 1) * (x ^ 2 + ∑ c, a c ^ 2) := by
…
  38. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.coefficient_zoomOut_sq_bound line 669

    Source documentation

    An actual independent extension coefficient is controlled by its homogeneous restriction coefficient and every dependent extension.

    theorem coefficient_zoomOut_sq_bound
    (f : (E →ₗ[F2] (B × F2)) → ℝ) (hf : IsBasisInvariant f)
    (z : B →ₗ[F2] E) {v : E} (hv : v ∉ z.range) :
    (((Fintype.card E - Fintype.card z.range : ℕ) : ℝ) ^ 2) *
        linearCoeff f (hyperplaneExtend z v) ^ 2 ≤
      ((Fintype.card z.range : ℝ) + 1) *
        (linearCoeff (fun X => f ((LinearMap.inl F2 B F2).comp X)) z ^ 2 +
          ∑ u : z.range, linearCoeff f (hyperplaneExtend z u.val) ^ 2) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend

  39. def OAI.MaxCutGames.Inverse.KMSAnalytic.leftEmbedding line 701
  40. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.leftEmbedding_injective line 704
  41. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.lastVector_not_mem_left_range line 710
  42. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.range_left_comp_of_surjective line 716
  43. def OAI.MaxCutGames.Inverse.KMSAnalytic.liftedRangeEquiv line 728

    Source documentation

    The dependent extensions are enumerated exactly once by the small space.

    def liftedRangeEquiv (ι : (J × F2) →ₗ[F2] E) (hι : Function.Injective ι)
    (z : B →ₗ[F2] J) (hz : Function.Surjective z) :
    J ≃ ((leftEmbedding ι).comp z).range :=
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.leftEmbedding

  44. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.liftedRangeEquiv_val line 742
  45. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.card_lifted_range line 746
  46. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.sum_lifted_range line 752
  47. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend_left_comp line 759