KMSAnalyticHybridEnergyImageTransportCoreLemmas.lean`

54 declarations, 0 contain sorry, 0 declared as axioms

Transport of a prescribed compressed image to adapted coordinates

The complement is an arbitrary actual complement to the image subspace. The resulting coordinate change carries each original Fourier fiber to the adapted fiber, preserving coefficients, phases, and the actual selector.

def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageAmbientEquiv line 38
Source documentation
Keep the selected first factor and split the remaining space along its prescribed compressed image.
```
def imageAmbientEquiv (W D : Submodule F2 U) (h : IsCompl W D) :
    (A × (W × D)) ≃ₗ[F2] (A × U) :=
…
```

def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imagePullback line 43

Source documentation

The original function expressed in the adapted primal coordinates.

def imagePullback (W D : Submodule F2 U) (h : IsCompl W D)
    (f : ((A × U) →ₗ[F2] (B × C)) → ℝ)
    (X : (A × (W × D)) →ₗ[F2] (B × C)) : ℝ :=
…

def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageTranslate line 49
Source documentation
The same affine translate expressed in adapted coordinates.
```
def imageTranslate (W D : Submodule F2 U) (h : IsCompl W D)
    (T : (A × U) →ₗ[F2] (B × C)) :
    (A × (W × D)) →ₗ[F2] (B × C) :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageAmbientEquiv_leftRange line 54
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.image_hybrid_iff line 65
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.image_compression_eq_iff line 85
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.image_character line 113
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.image_rank_coefficient line 123

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.image_coefficient_sum_transport line 137

Source documentation

Exact reindexing of a selected coefficient at a prescribed compressed image. No rank, surjectivity, or basis-invariance assumption is needed.

theorem image_coefficient_sum_transport (W D : Submodule F2 U) (h : IsCompl W D)
    [Fintype ((A × (W × D)) →ₗ[F2] (B × C))]
    [Fintype ((B × C) →ₗ[F2] (A × (W × D)))]
    (z : B →ₗ[F2] W) (f : ((A × U) →ₗ[F2] (B × C)) → ℝ)
    (T : (A × U) →ₗ[F2] (B × C)) (i : ℕ) :
    (∑ S : (B × C) →ₗ[F2] (A × U),
      if LinearIdentities.Hybrid S (LinearMap.range (LinearMap.inl F2 A U))
          (LinearMap.range (LinearMap.inl F2 B C)) ∧
          (LinearMap.snd F2 A U).comp (S.comp (LinearMap.inl F2 B C)) = W.subtype.comp z
      then linearCoeff (rankComponent i f) S * (linearTraceCharacter S T).re else 0) =
    ∑ S : (B × C) →ₗ[F2] (A × (W × D)),
      if LinearIdentities.Hybrid S (LinearMap.range (LinearMap.inl F2 A (W × D)))
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.rankComponent_eq_zero_of_finrank_lt line 201
Source documentation
No dual frequency has image dimension larger than the primal domain.
```
theorem rankComponent_eq_zero_of_finrank_lt
    (f : (E →ₗ[F2] F) → ℝ) (i : ℕ) (hi : Module.finrank F2 E < i) :
    rankComponent i f = 0 := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.rankComponent_eq_zero_of_codomain_finrank_lt line 213
Source documentation
The dual frequency rank is also bounded by its domain, the primal codomain. This includes rectangular spaces in either orientation.
```
theorem rankComponent_eq_zero_of_codomain_finrank_lt
    (f : (E →ₗ[F2] F) → ℝ) (i : ℕ) (hi : Module.finrank F2 F < i) :
    rankComponent i f = 0 := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_zero line 226
Source documentation
The zero function remains zero under the actual hybrid projection and affine restriction. No enumeration of quotient frequencies is required.
```
theorem hybridDerivative_zero (A : Submodule F2 E) (B : Submodule F2 F)
    (T : E →ₗ[F2] F) :
    hybridDerivative A B T (0 : (E →ₗ[F2] F) → ℝ) = 0 := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_eq_zero_of_finrank_lt line 232
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_eq_zero_of_codomain_finrank_lt line 240

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_energy_eq_zero_of_finrank_lt line 250

Source documentation

Finite primal restriction domains suffice to evaluate the zero energy; there is no additional Fintype requirement on the compressed dual space.

theorem hybridDerivative_rankComponent_energy_eq_zero_of_finrank_lt
    [Finite E] [Finite F]
    (A : Submodule F2 E) (B : Submodule F2 F)
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) (i : ℕ)
    (hi : Module.finrank F2 E < i) :
    (𝔼 N, hybridDerivative A B T (rankComponent i f) N ^ 2) = 0 := by
…

def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallCoeff line 290
Source documentation
The Fourier array of the small full-rank component.
```
def smallCoeff (ι : I →ₗ[F2] E) (f : (E →ₗ[F2] F) → ℝ)
    (T : F →ₗ[F2] I) : ℝ :=
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent line 296
Source documentation
A genuine function on the small primal matrix space, synthesized in its own orthonormal trace-character basis.
```
def smallComponent (ι : I →ₗ[F2] E) (f : (E →ₗ[F2] F) → ℝ) :
    (I →ₗ[F2] F) → ℝ := synthesis (smallCoeff ι f)
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.synthesis, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallCoeff
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.coeff_smallComponent line 300
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.coeff_smallComponent_of_surjective line 306
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.coeff_smallComponent_of_not_surjective line 313
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_energy line 321
Source documentation
Exact normalization: primal expectation equals an unnormalized sum over surjective small-space frequencies.
```
theorem smallComponent_energy (ι : I →ₗ[F2] E) (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, smallComponent ι f X ^ 2) =
      ∑ T ∈ Finset.univ.filter (fun T : F →ₗ[F2] I => Function.Surjective T),
        linearCoeff f (ι.comp T) ^ 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent_smallComponent line 332
Source documentation
Every retained frequency has rank equal to the small domain dimension.
```
theorem rankComponent_smallComponent (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) :
    rankComponent (Module.finrank F2 I) (smallComponent ι f) = smallComponent ι f := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.ker_comp_of_injective line 348
Source documentation
Composition with an injection preserves the actual kernel.
```
theorem ker_comp_of_injective (ι : I →ₗ[F2] E) (hι : Function.Injective ι)
    (T : F →ₗ[F2] I) : (ι.comp T).ker = T.ker :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallCoeff_eq_of_kernel_coeff_const line 356
Source documentation
The small Fourier array is independent of the chosen injection once the large function's actual coefficients are proved constant on kernel classes.
```
theorem smallCoeff_eq_of_kernel_coeff_const (ι κ : I →ₗ[F2] E)
    (hι : Function.Injective ι) (hκ : Function.Injective κ)
    (f : (E →ₗ[F2] F) → ℝ)
    (hcoeff : ∀ S T : F →ₗ[F2] E,
      S.ker = T.ker → linearCoeff f S = linearCoeff f T) :
    smallCoeff ι f = smallCoeff κ f := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallCoeff

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_eq_of_kernel_coeff_const line 373

Source documentation

Equality is of the actual synthesized functions, not merely their norms.

theorem smallComponent_eq_of_kernel_coeff_const (ι κ : I →ₗ[F2] E)
    (hι : Function.Injective ι) (hκ : Function.Injective κ)
    (f : (E →ₗ[F2] F) → ℝ)
    (hcoeff : ∀ S T : F →ₗ[F2] E,
      S.ker = T.ker → linearCoeff f S = linearCoeff f T) :
    smallComponent ι f = smallComponent κ f :=
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_orthogonal line 384
Source documentation
A small component is orthogonal to any small-space function whose full rank coefficients vanish.
```
theorem smallComponent_orthogonal (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (g : (I →ₗ[F2] F) → ℝ)
    (hg : ∀ T : F →ₗ[F2] I, Function.Surjective T → linearCoeff g T = 0) :
    (𝔼 X, smallComponent ι f X * g X) = 0 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_energy_le line 397
Source documentation
Injective frequency lifting cannot increase the total squared norm.
```
theorem smallComponent_energy_le (ι : I →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, smallComponent ι f X ^ 2) ≤ 𝔼 X, f X ^ 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent
abbrev OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.SmallEmbedding line 449
Source documentation
The actual injective maps from the comparison space.
```
abbrev SmallEmbedding (I E : Type*) [AddCommGroup I] [Module F2 I]
    [AddCommGroup E] [Module F2 E] :=
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.factorThroughSurjection line 454
Source documentation
A map with the same kernel as a surjection descends to its target.
```
def factorThroughSurjection (S : F →ₗ[F2] E) (T : F →ₗ[F2] I)
    (hT : Function.Surjective T) (hker : T.ker = S.ker) : I →ₗ[F2] E :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.factorThroughSurjection_apply line 458
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.factorThroughSurjection_comp line 463
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.factorThroughSurjection_injective line 469
def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.factorFrequency line 476
Source documentation
Compose the two factors and retain the proved rank.
```
def factorFrequency (p : SmallEmbedding I E × FullFrequency F I) : RankFrequency F E I :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.SmallEmbedding
def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.factorizationFiberEquivFullKernel line 482
Source documentation
Once the surjective factor is fixed, the injective factor is unique.
```
def factorizationFiberEquivFullKernel (S : RankFrequency F E I) :
    {p : SmallEmbedding I E × FullFrequency F I // factorFrequency p = S} ≃
      {T : FullFrequency F I // fullKernel T = rankKernel S} where
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.SmallEmbedding, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.factorFrequency
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.factorization_fiber_card line 531
Source documentation
The exact multiplicity in the embedding expansion is the square injection count, independent of the ambient frequency.
```
theorem factorization_fiber_card (S : RankFrequency F E I) :
    (Finset.univ.filter (fun p : SmallEmbedding I E × FullFrequency F I =>
      factorFrequency p = S)).card = KMSInjectionCount.beta I I := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.SmallEmbedding, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.factorFrequency, OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_apply_fullFrequency line 545
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent_apply_rankFrequency line 561
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.sum_smallComponent_embeddings line 578
Source documentation
Exact pointwise orbit synthesis. No basis-invariance assumption is required: every small component retains the coefficients from its own embedding.
```
theorem sum_smallComponent_embeddings (f : (E →ₗ[F2] F) → ℝ)
    (X : E →ₗ[F2] F) :
    (∑ ι : SmallEmbedding I E, smallComponent ι.val f (X.comp ι.val)) =
      (KMSInjectionCount.beta I I : ℝ) * rankComponent (Module.finrank F2 I) f X := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.SmallEmbedding, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent, OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent
def OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.primalChange line 636
Source documentation
The invertible change of the ordered domain basis.
```
def primalChange (g : E ≃ₗ[F2] E) : (E →ₗ[F2] F) ≃ (E →ₗ[F2] F) where
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.frequencyChange line 643
Source documentation
The contragredient reindexing used in the trace pairing.
```
def frequencyChange (g : E ≃ₗ[F2] E) : (F →ₗ[F2] E) ≃ (F →ₗ[F2] E) where
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant line 649
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.character_change line 652
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.coefficient_change line 661
Source documentation
Invariance of the function transfers to its actual normalized coefficients.
```
theorem coefficient_change (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) (g : E ≃ₗ[F2] E) (S : F →ₗ[F2] E) :
    linearCoeff f (g.toLinearMap.comp S) = linearCoeff f S := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant
def OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.frequencyRank line 672
Source documentation
The degree is the rank of the actual dual linear map.
```
def frequencyRank (S : F →ₗ[F2] E) : ℕ := Module.finrank F2 (LinearMap.range S)
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.frequencyRank_change line 675
def OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.rankProjection line 683
Source documentation
Exact rank projection, defined directly by trace characters.
```
def rankProjection (i : ℕ) (f : (E →ₗ[F2] F) → ℝ) (X : E →ₗ[F2] F) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.rankProjection_invariant line 687
Source documentation
Each rank projection preserves basis invariance.
```
theorem rankProjection_invariant (i : ℕ) (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) : IsBasisInvariant (rankProjection i f) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.rankProjection
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent_eq_rankProjection line 725
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent_invariant line 735
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent_coeff_eq_zero_of_ne line 741
Source documentation
The degree bound follows from the literal coefficient filter.
```
theorem rankComponent_coeff_eq_zero_of_ne (i : ℕ)
    (f : (E →ₗ[F2] F) → ℝ) (S : F →ₗ[F2] E)
    (hS : Module.finrank F2 S.range ≠ i) :
    linearCoeff (rankComponent i f) S = 0 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.rankComponent
def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.HomogeneousRestrictionBound line 779
Source documentation
Every homogeneous output restriction of codimension at most r has the stated actual normalized squared norm. The dimension inequality avoids truncated subtraction in the restriction-composition step.
```
def HomogeneousRestrictionBound (r : ℕ) (ε : ℝ) (f : (E →ₗ[F2] F) → ℝ) : Prop :=
…
```

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.HomogeneousRestrictionBound.codomain_pullback line 788

Source documentation

Restricting to codimension s leaves the remaining budget r. The proof uses only composition of actual injections and addition of dimensions.

theorem HomogeneousRestrictionBound.codomain_pullback
    [FiniteDimensional F2 B] (r s : ℕ) (ε : ℝ)
    (f : (E →ₗ[F2] F) → ℝ)
    (hf : HomogeneousRestrictionBound (r + s) ε f)
    (J : B →ₗ[F2] F) (hJ : Function.Injective J)
    (hcodim : Module.finrank F2 F ≤ Module.finrank F2 B + s) :
    HomogeneousRestrictionBound r ε (fun X : E →ₗ[F2] B => f (J.comp X)) := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.HomogeneousRestrictionBound

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.HomogeneousRestrictionBound.energy_le line 800
Source documentation
The unrestricted squared norm is included by the identity presentation.
```
theorem HomogeneousRestrictionBound.energy_le
    [FiniteDimensional F2 F] [Fintype (E →ₗ[F2] F)]
    (r : ℕ) (ε : ℝ) (f : (E →ₗ[F2] F) → ℝ)
    (hf : HomogeneousRestrictionBound r ε f) : (𝔼 X, f X ^ 2) ≤ ε := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.HomogeneousRestrictionBound
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.basisInvariant_codomain_pullback line 809
Source documentation
A homogeneous output restriction retains the original domain-basis invariance, as required at every step of the fixed-character induction.
```
theorem basisInvariant_codomain_pullback (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBasisInvariant f) (J : B →ₗ[F2] F) :
    IsBasisInvariant (fun X : E →ₗ[F2] B => f (J.comp X)) := by
…
```