KMSKernelOrbitsFourierLemmas.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Basis-invariant matrix functions have constant actual Fourier coefficients on kernel fibers. This uses ambient automorphism transitivity proved from the first isomorphism theorem, followed by the exact change-of-basis identity for the normalized trace-character transform.

theorem OAI.UniqueGamesTheorem.Inverse.KMSKernelOrbitsFourier.coefficient_eq_of_ker_eq line 39
Source documentation
Actual coefficients depend on the kernel, not on the chosen embedding of the quotient into the basis-index space. No coefficient-invariance premise is assumed beyond the original function's basis invariance.
```
theorem coefficient_eq_of_ker_eq (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) (S T : F →ₗ[F2] E) (hker : S.ker = T.ker) :
    linearCoeff f S = linearCoeff f T := by
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend line 75
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 :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend_apply line 78
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend_comp_inl line 81
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend_new_coordinate line 85
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend_recover line 89
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.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend
def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtensionEquiv line 98
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
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend_injective line 108
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.range_hyperplaneExtend line 114
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.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.range_hyperplaneExtend_of_mem line 118
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.ker_hyperplaneExtend_of_notMem line 124
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.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.coefficient_hyperplaneExtend_eq line 137
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.card_hyperplaneExtension_outside line 149
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
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.card_hyperplaneExtension_outside_pow line 156

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.sum_hyperplaneExtend_outside line 164

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.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.sum_hyperplaneExtend line 179

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.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.coefficient_hyperplaneExtend_recursion line 191

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.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend

def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.leftEmbedding line 228
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.leftEmbedding_injective line 231
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.lastVector_not_mem_left_range line 237
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.range_left_comp_of_surjective line 243
def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.liftedRangeEquiv line 255
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.UniqueGamesTheorem.Inverse.KMSAnalytic.leftEmbedding
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.liftedRangeEquiv_val line 269
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.card_lifted_range line 273
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.sum_lifted_range line 279
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.hyperplaneExtend_left_comp line 286
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_energy_cross_mul line 335
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.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_energy_ratio line 371
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.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_energy_pow_bound line 390

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.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_energy_le_of_energy_le line 419

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.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallCoeff_eq_of_basisInvariant line 462
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_eq_of_basisInvariant line 472
Source documentation
Independence is equality of the actual small-space functions.
```
theorem smallComponent_eq_of_basisInvariant (ι κ : I →ₗ[F2] E)
    (hι : Function.Injective ι) (hκ : Function.Injective κ)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f) :
    smallComponent ι f = smallComponent κ f :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.surjective_postcomp_equiv line 481
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallCoeff_postcomp_equiv line 496
Source documentation
The retained coefficient array is invariant under a small-space basis change, with surjectivity and the lifted frequency kernel both preserved.
```
theorem smallCoeff_postcomp_equiv (ι : I →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (g : I ≃ₗ[F2] I) (T : F →ₗ[F2] I) :
    smallCoeff ι f (g.toLinearMap.comp T) = smallCoeff ι f T := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallCoeff
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_invariant line 511
Source documentation
The small component is genuinely invariant as a function on matrices.
```
theorem smallComponent_invariant (ι : I →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f) :
    KMSBasisInvariant.IsBasisInvariant (smallComponent ι f) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent
abbrev OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.Extension line 547
Source documentation
The unnormalized fiber of extensions of one compressed frequency.
```
abbrev Extension (z : B →ₗ[R] W) :=
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.coordinatesDataEquiv line 551
Source documentation
The coordinate record has precisely three independent entries.
```
def coordinatesDataEquiv (z : B →ₗ[R] W) :
    Coordinates (A := A) (D := D) (C := C) z ≃
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.compressedFiberDataEquiv line 559
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.extensionEquiv line 567
Source documentation
Specifying the value on the complementary block gives every extension exactly once. This will give the cardinality factor |Hom(C,W)|.
```
def extensionEquiv (z : B →ₗ[R] W) : Extension (C := C) z ≃ (C →ₗ[R] W) where
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.Extension
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybrid_rank_coeff_assemble line 595
Source documentation
The actual hybrid and rank selectors reduce to the small component's ordinary surjectivity selector. The only remaining geometric selector is injectivity of the complementary block.
```
theorem hybrid_rank_coeff_assemble
    {z : B →ₗ[F2] W} (hz : Function.Surjective z)
    (p : Coordinates (A := A) (D := D) (C := C) z)
…
```

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.card_restriction_fiber_eq line 651

Source documentation

The restriction fiber has exactly as many elements as the maps on its complement, before any finite-field cardinality formula is applied.

theorem card_restriction_fiber_eq {R B C W : Type*} [Ring R]
    [AddCommGroup B] [Module R B] [AddCommGroup C] [Module R C]
    [AddCommGroup W] [Module R W]
    [Fintype ((B × C) →ₗ[R] W)] [Fintype (C →ₗ[R] W)]
    (z : B →ₗ[R] W) :
    (Finset.univ.filter (fun ψ : (B × C) →ₗ[R] W =>
      ψ.comp (LinearMap.inl R B C) = z)).card = Fintype.card (C →ₗ[R] W) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.natCard_extension line 669
Source documentation
The exact number of extensions is independent of the prescribed map.
```
theorem natCard_extension (z : B →ₗ[F2] W) :
    Nat.card (Extension (C := C) z) =
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.Extension

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.card_restriction_fiber line 676

Source documentation

The same exact count in the filtered form used by the fiber Cauchy bound.

theorem card_restriction_fiber [Fintype ((B × C) →ₗ[F2] W)]
    (z : B →ₗ[F2] W) :
    (Finset.univ.filter (fun ψ : (B × C) →ₗ[F2] W =>
      ψ.comp (LinearMap.inl F2 B C) = z)).card =
        2 ^ (Module.finrank F2 C * Module.finrank F2 W) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.card_linearMap_eq line 693
Source documentation
Exact binary cardinality of the unrestricted complementary map space.
```
theorem card_linearMap_eq [Fintype (C →ₗ[F2] D)] :
    Fintype.card (C →ₗ[F2] D) =
      2 ^ (Module.finrank F2 C * Module.finrank F2 D) := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.natCard_injective_le line 701
Source documentation
Ordered independent complementary choices are no more numerous than all maps on the complementary domain; there is no basis-orbit quotient.
```
theorem natCard_injective_le :
    Nat.card {v : C →ₗ[F2] D // Function.Injective v} ≤
      2 ^ (Module.finrank F2 C * Module.finrank F2 D) := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.card_injective_le line 715
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.natCard_rank_subspaces_le line 728
Source documentation
Choose one ordered basis for each image. The resulting encoding gives the dimension-sensitive image count, rather than the count of all subspaces.
```
theorem natCard_rank_subspaces_le (q : ℕ) :
    Nat.card {W : Submodule F2 U // Module.finrank F2 W = q} ≤
      2 ^ (q * Module.finrank F2 U) := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.card_rank_subspaces_le line 735
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.count_exponent_le line 744
Source documentation
The three counting costs leave nonnegative slack in the ambient dimension exponent. The complementary image space has dimension q + d.
```
theorem count_exponent_le (a b q d : ℕ) :
    q * (q + d) + (b * d) * 2 + b * q ≤ (2 * b + q) * (a + q + d) := by
…
```

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.count_budget_le line 753

Source documentation

The actual nonnegative counts fit the mixed Fourier denominator. The bound also permits real-valued upper estimates for those counts.

theorem count_budget_le (a b q d : ℕ) (countW countV extensionFactor : ℝ)
    (hv0 : 0 ≤ countV) (he0 : 0 ≤ extensionFactor)
    (hw : countW ≤ (2 : ℝ) ^ (q * (q + d)))
    (hv : countV ≤ (2 : ℝ) ^ (b * d))
    (he : extensionFactor ≤ (2 : ℝ) ^ (b * q)) :
    countW * countV ^ 2 * extensionFactor ≤
      (2 : ℝ) ^ ((2 * b + q) * (a + q + d)) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.count_budget_le_of_dimension line 776

Source documentation

Ambient-dimension form of the same budget, with the split dimension identity supplied by the adapted coordinates.

theorem count_budget_le_of_dimension (a b q d ell : ℕ)
    (hell : ell = a + q + d) (countW countV extensionFactor : ℝ)
    (hv0 : 0 ≤ countV) (he0 : 0 ≤ extensionFactor)
    (hw : countW ≤ (2 : ℝ) ^ (q * (ell - a)))
    (hv : countV ≤ (2 : ℝ) ^ (b * d))
    (he : extensionFactor ≤ (2 : ℝ) ^ (b * q)) :
    countW * countV ^ 2 * extensionFactor ≤ (2 : ℝ) ^ ((2 * b + q) * ell) := by
…

def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy line 821
Source documentation
Squared small Fourier coefficients whose image under a prescribed linear projection is the fixed partial frequency.
```
def fixedFrequencyEnergy (ι : I →ₗ[F2] E) (f : (E →ₗ[F2] F) → ℝ)
    (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_nonneg line 827

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_eq line 835

Source documentation

The definition retains precisely the surjective compatible frequencies.

theorem fixedFrequencyEnergy_eq (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) :
    fixedFrequencyEnergy ι f π A =
      ∑ T ∈ Finset.univ.filter (fun T : F →ₗ[F2] I => π.comp T = A ∧ Function.Surjective T),
        linearCoeff f (ι.comp T) ^ 2 := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_eq_zero_of_not_surjective line 850

Source documentation

An impossible partial frequency contributes no energy.

theorem fixedFrequencyEnergy_eq_zero_of_not_surjective
    (ι : I →ₗ[F2] E) (f : (E →ₗ[F2] F) → ℝ)
    (π : I →ₗ[F2] J) (hπ : Function.Surjective π)
    (A : F →ₗ[F2] J) (hA : ¬ Function.Surjective A) :
    fixedFrequencyEnergy ι f π A = 0 := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_le line 864
Source documentation
Forgetting the prescribed partial frequency gives the exact full small energy, so every individual restricted sum is bounded by it.
```
theorem fixedFrequencyEnergy_le (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) :
    fixedFrequencyEnergy ι f π A ≤ 𝔼 X, smallComponent ι f X ^ 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_zero line 874
Source documentation
With no fixed characters the restricted sum is exactly the small squared norm; there is no ambient-cardinality normalization in the frequency sum.
```
theorem fixedFrequencyEnergy_zero (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) :
    fixedFrequencyEnergy ι f (0 : I →ₗ[F2] J) 0 =
      𝔼 X, smallComponent ι f X ^ 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy_eq_of_basisInvariant line 885

Source documentation

The fixed-character energy is independent of the chosen small-space embedding for the actual basis-invariant function.

theorem fixedFrequencyEnergy_eq_of_basisInvariant (ι κ : I →ₗ[F2] E)
    (hι : Function.Injective ι) (hκ : Function.Injective κ)
    (f : (E →ₗ[F2] F) → ℝ) (hf : IsBasisInvariant f)
    (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) :
    fixedFrequencyEnergy ι f π A = fixedFrequencyEnergy κ f π A := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.fixedFrequencyEnergy