OAI/Computability/UniqueGames/Inverse/KMSAnalyticCharacterInduction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The full fixed-character induction for the actual KMS small component. The only local hypothesis bounds squared norms of homogeneous restrictions; all Fourier recursions, multiplicities and coordinate changes are proved.

  1. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_bound_induction line 29
  2. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_le_of_homogeneous line 105

    Source documentation

    KMS's fixed-character estimate, with actual homogeneous restriction control. The injection is the only ambient-dimension assumption.

    theorem fixedFrequencyEnergy_le_of_homogeneous
    {F : Type v} [AddCommGroup F] [Module F2 F]
    [FiniteDimensional F2 F] [Fintype F]
    {I : Type w} [AddCommGroup I] [Module F2 I]
    [FiniteDimensional F2 I] [Fintype I]
    {J : Type x} [AddCommGroup J] [Module F2 J]
    [FiniteDimensional F2 J] [Fintype J]
    (ι : I →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] F) → ℝ) (hf : IsBasisInvariant f)
    (ε : ℝ) (hg : HomogeneousRestrictionBound (Module.finrank F2 I) ε f)
    (π : I →ₗ[F2] J) (hπ : Function.Surjective π) (A : F →ₗ[F2] J) :
    (2 : ℝ) ^ ((Module.finrank F2 I + Module.finrank F2 J) * Module.finrank F2 E) *
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.HomogeneousRestrictionBound