OAI/Computability/UniqueGames/Inverse/KMSFourthMomentMixedEnergyLemmas.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Exact Fourier slice energies and their one-point KMS recurrence. The energy is an unnormalized sum of actual squared coefficients. Translation changes only a unit sign, so the dependent graph terms in the point recursion have identical slice energies, without an ambient-cardinality loss.

  1. def OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy line 33

    Source documentation

    An arbitrary actual Fourier slice; in the mixed estimate P fixes selected frequency coordinates.

    def sliceEnergy (P : (F →ₗ[F2] E) → Prop) (f : (E →ₗ[F2] F) → ℝ) : ℝ :=
…
  2. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy_nonneg line 37
  3. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.coeff_translate line 42

    Source documentation

    Translation acts on each actual coefficient by its trace-character sign.

    theorem coeff_translate (f : (E →ₗ[F2] F) → ℝ) (Z : E →ₗ[F2] F)
    (T : F →ₗ[F2] E) :
    linearCoeff (fun X => f (X + Z)) T =
      linearCoeff f T * (linearTraceCharacter T Z).re := by
…
  4. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy_translate line 60

    Source documentation

    No loss from translating a function before taking a fixed Fourier slice.

    theorem sliceEnergy_translate (P : (F →ₗ[F2] E) → Prop)
    (f : (E →ₗ[F2] F) → ℝ) (Z : E →ₗ[F2] F) :
    sliceEnergy P (fun X => f (X + Z)) = sliceEnergy P f := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy

  5. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy_sub_sum_le line 75

    Source documentation

    A finite difference of functions costs only the number of summands in its Fourier slice energy. No pointwise bound on those functions is used.

    theorem sliceEnergy_sub_sum_le {J : Type*} [Fintype J]
    (P : (F →ₗ[F2] E) → Prop) (f : (E →ₗ[F2] F) → ℝ)
    (g : J → (E →ₗ[F2] F) → ℝ) :
    sliceEnergy P (fun X => f X - ∑ j, g j X) ≤
      2 * (sliceEnergy P f + (Fintype.card J : ℝ) * ∑ j, sliceEnergy P (g j)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy

  6. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy_sub_translates_le line 108

    Source documentation

    A sum of arbitrary translates has the same quadratic slice bound with the square of the number of translates.

    theorem sliceEnergy_sub_translates_le {J : Type*} [Fintype J]
    (P : (F →ₗ[F2] E) → Prop) (f g : (E →ₗ[F2] F) → ℝ)
    (Z : J → E →ₗ[F2] F) :
    sliceEnergy P (fun X => f X - ∑ j, g (X + Z j)) ≤
      2 * (sliceEnergy P f + (Fintype.card J : ℝ) ^ 2 * sliceEnergy P g) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy

  7. def OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict line 144

    Source documentation

    Fix the first product block, leaving the second block free.

    def partialRestrict (f : ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F) :
    (I →ₗ[F2] F) → ℝ := fun X => f (a.coprod X)
  8. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict_apply line 147
  9. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.coprod_add_shift line 152

    Source documentation

    The two coordinate shifts reassemble to the original full-map shift.

    theorem coprod_add_shift (a : A →ₗ[F2] F) (X : I →ₗ[F2] F)
    (Z : (A × I) →ₗ[F2] F) :
    a.coprod X + Z =
      (a + Z.comp (LinearMap.inl F2 A I)).coprod
        (X + Z.comp (LinearMap.inr F2 A I)) := by
…
  10. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict_translate line 168

    Source documentation

    Restriction of a translate shifts the fixed and the free blocks.

    theorem partialRestrict_translate
    (f : ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F)
    (Z : (A × I) →ₗ[F2] F) :
    partialRestrict (fun Y => f (Y + Z)) a =
      fun X => partialRestrict f (a + Z.comp (LinearMap.inl F2 A I))
        (X + Z.comp (LinearMap.inr F2 A I)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict

  11. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict_sub_sum line 181

    Source documentation

    Partial restriction commutes exactly with a finite difference.

    theorem partialRestrict_sub_sum {J : Type*} [Fintype J]
    (f : ((A × I) →ₗ[F2] F) → ℝ)
    (g : J → ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F) :
    partialRestrict (fun Y => f Y - ∑ j, g j Y) a =
      fun X => partialRestrict f a X - ∑ j, partialRestrict (g j) a X := rfl
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict

  12. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy_partialRestrict_translate line 192

    Source documentation

    The free-block translation has unit Fourier phase, leaving only the shift of the fixed block in the slice energy.

    theorem sliceEnergy_partialRestrict_translate
    (P : (F →ₗ[F2] I) → Prop)
    (f : ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F)
    (Z : (A × I) →ₗ[F2] F) :
    sliceEnergy P (partialRestrict (fun Y => f (Y + Z)) a) =
      sliceEnergy P (partialRestrict f (a + Z.comp (LinearMap.inl F2 A I))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict

  13. theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy_partialRestrict_sub_translates_le line 202

    Source documentation

    The exact finite Cauchy bound after fixing a product block. Each correction function is evaluated at its own translated fixed block.

    theorem sliceEnergy_partialRestrict_sub_translates_le {J : Type*} [Fintype J]
    (P : (F →ₗ[F2] I) → Prop)
    (f : ((A × I) →ₗ[F2] F) → ℝ)
    (g : J → ((A × I) →ₗ[F2] F) → ℝ)
    (a : A →ₗ[F2] F) (Z : J → (A × I) →ₗ[F2] F) :
    sliceEnergy P (partialRestrict (fun Y => f Y - ∑ j, g j (Y + Z j)) a) ≤
      2 * (sliceEnergy P (partialRestrict f a) +
        (Fintype.card J : ℝ) * ∑ j, sliceEnergy P
          (partialRestrict (g j) (a + (Z j).comp (LinearMap.inl F2 A I)))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict

  14. def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.frequencyBlockEquiv line 244

    Source documentation

    Splitting the fixed and free frequency blocks is an exact bijection.

    def frequencyBlockEquiv : ((F →ₗ[F2] A) × (F →ₗ[F2] I)) ≃
    (F →ₗ[F2] (A × I)) where
…
  15. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sum_frequency_blocks line 253

    Source documentation

    The free frequency can be summed first, with no multiplicity factor.

    theorem sum_frequency_blocks {M : Type*} [AddCommMonoid M]
    [Fintype (F →ₗ[F2] A)] [Fintype (F →ₗ[F2] I)]
    [Fintype (F →ₗ[F2] (A × I))]
    (g : (F →ₗ[F2] (A × I)) → M) :
    ∑ S, g S = ∑ T : F →ₗ[F2] I, ∑ alpha : F →ₗ[F2] A, g (alpha.prod T) := by
…
  16. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.partialRestrict_eq_synthesis line 269

    Source documentation

    Fixing a primal block merges exactly its dual frequency block.

    theorem partialRestrict_eq_synthesis
    (h : ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F) :
    partialRestrict h a = synthesis (fun T : F →ₗ[F2] I =>
      ∑ alpha : F →ₗ[F2] A,
        linearCoeff h (alpha.prod T) * (linearTraceCharacter alpha a).re) := by
…
  17. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.coeff_partialRestrict line 288

    Source documentation

    The actual partial-restriction coefficient is an unnormalized frequency merge; normalized Fourier expectation introduces no additional factor.

    theorem coeff_partialRestrict
    (h : ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F)
    (T : F →ₗ[F2] I) :
    linearCoeff (partialRestrict h a) T =
      ∑ alpha : F →ₗ[F2] A,
        linearCoeff h (alpha.prod T) * (linearTraceCharacter alpha a).re := by
…
  18. def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.coordinateOfData line 319
  19. def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.primalA line 324
  20. def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.primalW line 327
  21. def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.primalD line 330
  22. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sum_compressedFiber line 336
  23. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sum_alpha_hybrid_term line 363

    Source documentation

    One sum over the fixed frequency block is precisely the Fourier coefficient of the actual partially restricted small component.

    theorem sum_alpha_hybrid_term (z : B →ₗ[F2] W) (hz : Function.Surjective z)
    (κ : (A × (W × C)) →ₗ[F2] (A × (W × D))) (hκ : Function.Injective κ)
    (f : ((A × (W × D)) →ₗ[F2] (B × C)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : (A × (W × D)) →ₗ[F2] (B × C))
    (ψ : Extension (C := C) z) (v : C →ₗ[F2] D) :
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.Extension

  24. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybrid_fiber_coefficient_factorization line 397

    Source documentation

    Exact phase/frequency factorization in the adapted fiber. Every coefficient on the right belongs to the actual mixed partial restriction.

    theorem hybrid_fiber_coefficient_factorization
    (z : B →ₗ[F2] W) (hz : Function.Surjective z)
    (κ : (A × (W × C)) →ₗ[F2] (A × (W × D))) (hκ : Function.Injective κ)
    (f : ((A × (W × D)) →ₗ[F2] (B × C)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : (A × (W × D)) →ₗ[F2] (B × C)) :
    (∑ S : {S : (B × C) →ₗ[F2] (A × (W × D)) //
        compressBlock S = z.prod (0 : B →ₗ[F2] D)},
      (if LinearIdentities.Hybrid S.val
          (LinearMap.range (LinearMap.inl F2 A (W × D)))
          (LinearMap.range (LinearMap.inl F2 B C)) then
        linearCoeff (rankComponent (Module.finrank F2 (A × (W × C))) f) S.val else 0) *
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant

  25. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sliceEnergy_fixed_snd line 464

    Source documentation

    An actual slice fixing the last frequency block is parametrized by all first blocks, with no multiplicity or normalization factor.

    theorem sliceEnergy_fixed_snd (ν : F →ₗ[F2] C)
    (g : ((W × C) →ₗ[F2] F) → ℝ) :
    sliceEnergy (fun T => (LinearMap.snd F2 W C).comp T = ν) g =
      ∑ ψ : F →ₗ[F2] W, linearCoeff g (ψ.prod ν) ^ 2 := by
…
  26. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sliceEnergy_snd_eq_sum line 495
  27. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sum_extensions_eq_filter line 513

    Source documentation

    Summing over actual extensions is exactly the corresponding filtered frequency sum. This identity applies to phases and squared coefficients.

    theorem sum_extensions_eq_filter (z : B →ₗ[R] W)
    [Fintype (Extension (C := C) z)] (H : ((B × C) →ₗ[R] W) → M) :
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.Extension

  28. def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient line 556
  29. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.traceCharacter_re_sq line 571
  30. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.adapted_image_energy_le_mixed line 579

    Source documentation

    The contribution of all surjective compressed maps onto one fixed image is bounded by the actual mixed-slice energy, with its exact extension count.

    theorem adapted_image_energy_le_mixed
    (κ : (A × (W × C)) →ₗ[F2] (A × (W × D))) (hκ : Function.Injective κ)
    (f : ((A × (W × D)) →ₗ[F2] (B × C)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : (A × (W × D)) →ₗ[F2] (B × C)) :
    (∑ z ∈ Finset.univ.filter (fun z : B →ₗ[F2] W => Function.Surjective z), adaptedFiberCoefficient z f T ^ 2) ≤
      (Fintype.card (C →ₗ[F2] D) : ℝ) ^ 2 * (Fintype.card (C →ₗ[F2] W) : ℝ) *
        sliceEnergy (fun U : (B × C) →ₗ[F2] (W × C) =>
          (LinearMap.snd F2 W C).comp U = LinearMap.snd F2 B C)
          (partialRestrict (smallComponent κ f) (primalA T)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.primalA

  31. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.adapted_image_energy_le_of_mixed line 639

    Source documentation

    The conditional analytic step uses an actual mixed-slice bound as its only analytic hypothesis.

    theorem adapted_image_energy_le_of_mixed
    (κ : (A × (W × C)) →ₗ[F2] (A × (W × D))) (hκ : Function.Injective κ)
    (f : ((A × (W × D)) →ₗ[F2] (B × C)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : (A × (W × D)) →ₗ[F2] (B × C)) (H : ℝ)
    (hH : sliceEnergy (fun U : (B × C) →ₗ[F2] (W × C) =>
        (LinearMap.snd F2 W C).comp U = LinearMap.snd F2 B C)
      (partialRestrict (smallComponent κ f) (primalA T)) ≤ H) :
    (∑ z ∈ Finset.univ.filter (fun z : B →ₗ[F2] W => Function.Surjective z), adaptedFiberCoefficient z f T ^ 2) ≤
      (Fintype.card (C →ₗ[F2] D) : ℝ) ^ 2 * (Fintype.card (C →ₗ[F2] W) : ℝ) * H := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.primalA, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient

  32. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.exists_injective_last_of_finrank_le line 683

    Source documentation

    Finite-dimensional comparison constructs an actual complementary map.

    theorem exists_injective_last_of_finrank_le
    [FiniteDimensional R C] [FiniteDimensional R D]
    (hdim : Module.finrank R C ≤ Module.finrank R D) :
    ∃ v : C →ₗ[R] D, Function.Injective v :=
…
  33. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.exists_injective_small_embedding_of_finrank_le line 691

    Source documentation

    Keep the first two coordinates and embed the complementary coordinate. This provides the fixed injection needed to define the small component.

    theorem exists_injective_small_embedding_of_finrank_le
    [FiniteDimensional R C] [FiniteDimensional R D]
    (hdim : Module.finrank R C ≤ Module.finrank R D) :
    ∃ κ : (A × (W × C)) →ₗ[R] (A × (W × D)), Function.Injective κ := by
…
  34. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.exists_injective_last_of_hybrid line 700

    Source documentation

    The actual hybrid selector itself witnesses a complementary injection. No arbitrary embedding is postulated when the compressed fiber is used.

    theorem exists_injective_last_of_hybrid (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))) :
    ∃ v : C →ₗ[R] D, Function.Injective v := by
…
  35. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.no_injective_last_of_finrank_lt line 710
  36. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient_eq_zero_of_no_injective_last line 737

    Source documentation

    An impossible complementary injection makes every term in an onto compressed coefficient vanish through its genuine hybrid selector.

    theorem adaptedFiberCoefficient_eq_zero_of_no_injective_last
    (z : B →ₗ[F2] W) (hz : Function.Surjective z)
    (f : ((A × (W × D)) →ₗ[F2] (B × C)) → ℝ)
    (T : (A × (W × D)) →ₗ[F2] (B × C))
    (hno : ∀ v : C →ₗ[F2] D, ¬ Function.Injective v) :
    adaptedFiberCoefficient z f T = 0 := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient

  37. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient_eq_zero_of_finrank_lt line 755
  38. theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.adapted_image_energy_eq_zero_of_no_injective_last line 768

    Source documentation

    The entire fixed-image contribution is zero in the impossible dimension case, so no small-space embedding is needed in that branch.

    theorem adapted_image_energy_eq_zero_of_no_injective_last
    [Fintype (B →ₗ[F2] W)]
    (f : ((A × (W × D)) →ₗ[F2] (B × C)) → ℝ)
    (T : (A × (W × D)) →ₗ[F2] (B × C))
    (hno : ∀ v : C →ₗ[F2] D, ¬ Function.Injective v) :
    (∑ z ∈ Finset.univ.filter (fun z : B →ₗ[F2] W => Function.Surjective z),
      adaptedFiberCoefficient z f T ^ 2) = 0 := by
…

    Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient