OAI/Computability/UniqueGames/Inverse/KMSAnalyticBlockFrequenciesLemmas.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Compatible block frequencies

A compatible surjection on B × F2 has a unique old surjection and a new vector in the kernel of the partial projection. The new vector does not change its kernel. Consequently actual basis-invariant Fourier coefficients are constant along this fiber, yielding its exact energy multiplicity.

  1. def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.blockFrequency line 32

    Source documentation

    Adjoin a new identity coordinate and an arbitrary off-diagonal vector.

    def blockFrequency (z : B →ₗ[F2] J) (w : J) : (B × F2) →ₗ[F2] (J × F2) :=
…
  2. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.blockFrequency_apply line 35
  3. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.blockFrequency_surjective_iff line 38
  4. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.ker_blockFrequency line 53

    Source documentation

    The kernel is independent of the off-diagonal vector, without any surjectivity assumption.

    theorem ker_blockFrequency (z : B →ₗ[F2] J) (w : J) :
    (blockFrequency z w).ker = z.ker.prod (⊥ : Submodule F2 F2) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.blockFrequency

  5. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.blockFrequency_compatible_iff line 64
  6. def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.blockOld line 81
  7. def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.blockNew line 84
  8. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.blockOld_blockFrequency line 86
  9. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.blockNew_blockFrequency line 91
  10. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.blockFrequency_recover line 94
  11. abbrev OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.CompatibleBlockFrequency line 107
  12. abbrev OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.CompatibleOldFrequency line 112
  13. def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.compatibleBlockFrequencyEquiv line 116

    Source documentation

    The actual compatible frequency fiber, with its exact kernel-vector parameter.

    def compatibleBlockFrequencyEquiv (π : J →ₗ[F2] K) (A : B →ₗ[F2] K) :
    CompatibleBlockFrequency π A ≃ CompatibleOldFrequency π A × π.ker where
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.CompatibleBlockFrequency, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.CompatibleOldFrequency

  14. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.coefficient_blockFrequency_eq line 143

    Source documentation

    Actual lifted coefficients are independent of the block vector.

    theorem coefficient_blockFrequency_eq (ι : (J × F2) →ₗ[F2] E)
    (hι : Function.Injective ι) (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (z : B →ₗ[F2] J) (u v : J) :
    linearCoeff f (ι.comp (blockFrequency z u)) =
      linearCoeff f (ι.comp (blockFrequency z v)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.blockFrequency

  15. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_block line 162

    Source documentation

    Exact collapse of the new-coordinate fiber in the prescribed-frequency energy. The multiplier is the actual number of vectors in ker π.

    theorem fixedFrequencyEnergy_block (ι : (J × F2) →ₗ[F2] E)
    (hι : Function.Injective ι) (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (π : J →ₗ[F2] K) (A : B →ₗ[F2] K) :
    fixedFrequencyEnergy ι f (π.prodMap (LinearMap.id : F2 →ₗ[F2] F2))
      (A.prodMap (LinearMap.id : F2 →ₗ[F2] F2)) =
      (Fintype.card π.ker : ℝ) * ∑ z : CompatibleOldFrequency π A,
        linearCoeff f (ι.comp (blockFrequency z.val 0)) ^ 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.CompatibleOldFrequency, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.blockFrequency

  16. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_energy_base_bound line 227
  17. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_zero_dim_bound line 255

    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.UniqueGamesTheorem.Inverse.KMSAnalytic.HomogeneousRestrictionBound, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy

  18. def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.codomainTransport line 297
  19. def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.codomainFrequencyEquiv line 301

    Source documentation

    Actual dual frequencies are reindexed by precomposition with the inverse.

    def codomainFrequencyEquiv (e : F ≃ₗ[F2] F') : (F →ₗ[F2] I) ≃ (F' →ₗ[F2] I) where
…
  20. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.codomainFrequencyEquiv_apply line 307
  21. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.codomainFrequency_cancel line 310
  22. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.surjective_comp_codomainEquiv_iff line 313
  23. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.linearCoeff_codomainTransport line 330

    Source documentation

    The Fourier pullback fiber of a codomain equivalence has a single term.

    theorem linearCoeff_codomainTransport (e : F ≃ₗ[F2] F')
    (f : (E →ₗ[F2] F) → ℝ) (S' : F' →ₗ[F2] E) :
    linearCoeff (codomainTransport e f) S' = linearCoeff f (S'.comp e.toLinearMap) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.codomainTransport

  24. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.basisInvariant_codomainTransport line 352

    Source documentation

    Codomain transport preserves the original basis invariance.

    theorem basisInvariant_codomainTransport (e : F ≃ₗ[F2] F')
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f) :
    KMSBasisInvariant.IsBasisInvariant (codomainTransport e f) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.codomainTransport

  25. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallCoeff_codomainTransport line 368
  26. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_codomainTransport line 380

    Source documentation

    The synthesized small component itself commutes with codomain transport.

    theorem smallComponent_codomainTransport (e : F ≃ₗ[F2] F') (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) :
    smallComponent ι (codomainTransport e f) =
      codomainTransport e (smallComponent ι f) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.codomainTransport

  27. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_codomainTransport line 393

    Source documentation

    Transport the prescribed partial frequency together with the primal codomain; the normalized energy remains exactly unchanged.

    theorem fixedFrequencyEnergy_codomainTransport (e : F ≃ₗ[F2] F') (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) :
    fixedFrequencyEnergy ι (codomainTransport e f) π (A.comp e.symm.toLinearMap) =
      fixedFrequencyEnergy ι f π A := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.codomainTransport

  28. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend_old_injective line 433

    Source documentation

    Fixing the new coordinate still allows recovery of the entire old map.

    theorem hyperplaneExtend_old_injective (w : J) :
    Function.Injective (fun z : B →ₗ[F2] J => hyperplaneExtend z w) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend

  29. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend_surjective line 441

    Source documentation

    A surjective old frequency stays surjective after any new coordinate.

    theorem hyperplaneExtend_surjective {z : B →ₗ[F2] J}
    (hz : Function.Surjective z) (w : J) :
    Function.Surjective (hyperplaneExtend z w) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend

  30. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.comp_hyperplaneExtend line 450

    Source documentation

    The fixed partial frequency extends by its actual projected new value.

    theorem comp_hyperplaneExtend (π : J →ₗ[F2] K) (z : B →ₗ[F2] J) (w : J) :
    π.comp (hyperplaneExtend z w) = hyperplaneExtend (π.comp z) (π w) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend

  31. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.dependent_extension_energy_le line 466

    Source documentation

    Each fixed dependent extension branch is bounded by the genuine restricted small-component energy. There is no hidden cardinality factor.

    theorem dependent_extension_energy_le
    (ι : J →ₗ[F2] E) (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (π : J →ₗ[F2] K) (A0 : B →ₗ[F2] K) (w : J) :
    (∑ z : B →ₗ[F2] J with π.comp z = A0 ∧ Function.Surjective z,
      linearCoeff f (ι.comp (hyperplaneExtend z w)) ^ 2) ≤
        fixedFrequencyEnergy ι f π (hyperplaneExtend A0 (π w)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy

  32. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.HomogeneousRestrictionBound.mono line 520
  33. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.HomogeneousRestrictionBound.codomain_equiv line 526
  34. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_postcomp_injective line 545
  35. def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallFrequencyEquiv line 592

    Source documentation

    Reindex the actual dual frequency maps by an equivalence of their targets.

    def smallFrequencyEquiv (e : I ≃ₗ[F2] I') : (F →ₗ[F2] I) ≃ (F →ₗ[F2] I') where
…
  36. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallFrequencyEquiv_apply line 598
  37. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.surjective_smallFrequencyEquiv_iff line 601
  38. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallFrequency_transport_comp line 615

    Source documentation

    Transporting the outer map in the opposite direction cancels the frequency-coordinate change.

    theorem smallFrequency_transport_comp (e : I ≃ₗ[F2] I') (π : I →ₗ[F2] J)
    (T : F →ₗ[F2] I) :
    (π.comp e.symm.toLinearMap).comp (e.toLinearMap.comp T) = π.comp T := by
…
  39. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallCoeff_transport line 633

    Source documentation

    Exact coefficient transport; the embedding need not be injective and the original function need not be basis invariant.

    theorem smallCoeff_transport (e : I ≃ₗ[F2] I') (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (T : F →ₗ[F2] I) :
    smallCoeff (ι.comp e.symm.toLinearMap) f (e.toLinearMap.comp T) =
      smallCoeff ι f T := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallCoeff

  40. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_transport line 645

    Source documentation

    Prescribed partial-frequency energy is unchanged when its projection and embedding are both transported to the new small space.

    theorem fixedFrequencyEnergy_transport (e : I ≃ₗ[F2] I') (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) :
    fixedFrequencyEnergy (ι.comp e.symm.toLinearMap) f
      (π.comp e.symm.toLinearMap) A = fixedFrequencyEnergy ι f π A := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy

  41. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_transport line 662

    Source documentation

    The actual small-space functions agree under the corresponding primal coordinate pullback.

    theorem smallComponent_transport (e : I ≃ₗ[F2] I') (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (X : I' →ₗ[F2] F) :
    smallComponent (ι.comp e.symm.toLinearMap) f X =
      smallComponent ι f (X.comp e.toLinearMap) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent

  42. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_precomp_equiv line 678

    Source documentation

    The same function identity with the new embedding written as ι ∘ g.

    theorem smallComponent_precomp_equiv (g : I ≃ₗ[F2] I') (ι : I' →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (X : I →ₗ[F2] F) :
    smallComponent (ι.comp g.toLinearMap) f X =
      smallComponent ι f (X.comp g.symm.toLinearMap) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent

  43. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.sum_dependentRows line 708
  44. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.sum_rows_split line 720
  45. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.coeff_dependent_extension line 737

    Source documentation

    A dependent row changes the embedding, but not its frequency kernel.

    theorem coeff_dependent_extension (ι : J →ₗ[F2] E)
    (hι : Function.Injective ι) (f : ((E × F2) →ₗ[F2] F) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : F →ₗ[F2] J) (φ : J →ₗ[F2] F2) :
    linearCoeff f ((ι.comp T).prod (φ.comp T)) =
      linearCoeff f ((pointPad ι).comp T) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointPad

  46. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.point_row_recursion line 759

    Source documentation

    The precise rowwise identity before Fourier synthesis.

    theorem point_row_recursion (ι : J →ₗ[F2] E) (hι : Function.Injective ι)
    (f : ((E × F2) →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : F →ₗ[F2] J) (hT : Function.Surjective T)
    (X : J →ₗ[F2] F) (a : F) :
    (∑ ell : F →ₗ[F2] F2,
      linearCoeff f ((ι.comp T).prod ell) * (binarySign (ell a)).re) *
        (linearTraceCharacter T X).re =
      (∑ ell : F →ₗ[F2] F2,
        (if Function.Surjective (T.prod ell)
          then linearCoeff f ((ι.comp T).prod ell) else 0) *
            (linearTraceCharacter (T.prod ell) (pointAppend X a)).re) +
      ∑ φ : J →ₗ[F2] F2, linearCoeff f ((pointPad ι).comp T) *
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointAppend, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointPad

  47. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.point_restriction_recursion_add line 801

    Source documentation

    One-column point restriction, with the dependent-row correction added back. This identity applies in every dimension, including zero.

    theorem point_restriction_recursion_add (ι : J →ₗ[F2] E)
    (hι : Function.Injective ι) (f : ((E × F2) →ₗ[F2] F) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (X : J →ₗ[F2] F) (a : F) :
    smallComponent ι (pointRestrict f a) X =
      smallComponent (pointLift ι) f (pointAppend X a) +
        ∑ φ : J →ₗ[F2] F2, smallComponent (pointPad ι) f (X + φ.smulRight a) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointRestrict, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointLift, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointAppend, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointPad

  48. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.point_restriction_recursion line 825

    Source documentation

    KMS Lemma 3.8: the full-rank component after adjoining one coordinate is the restricted component minus the sum of all dependent graph terms.

    theorem point_restriction_recursion (ι : J →ₗ[F2] E)
    (hι : Function.Injective ι) (f : ((E × F2) →ₗ[F2] F) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (X : J →ₗ[F2] F) (a : F) :
    smallComponent (pointLift ι) f (pointAppend X a) =
      smallComponent ι (pointRestrict f a) X -
        ∑ φ : J →ₗ[F2] F2, smallComponent (pointPad ι) f (X + φ.smulRight a) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointLift, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointAppend, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointRestrict, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointPad