KMSAnalyticHybridEnergyTransportSmall.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Small-component pullback under ambient coordinate equivalences

The small domain stays fixed while the ambient embedding and primal codomain are transported together. These are exact identities for the actual Fourier coefficients and synthesized functions; they require no analytic estimate.

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.basisInvariant_pullback line 33
Source documentation
Ambient coordinate pullback preserves invariance under every domain basis change, by transporting that change through the domain equivalence.
```
theorem basisInvariant_pullback (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (f : (E' →ₗ[F2] F') → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f) :
    KMSBasisInvariant.IsBasisInvariant
      (fun M => f (LinearEquiv.arrowCongr a b M)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.surjective_comp_symm_iff line 48

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.smallCoeff_pullback line 66

Source documentation

Exact small Fourier coefficient transport. The embedding need not be injective, and the observable need not be basis invariant.

theorem smallCoeff_pullback (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (ι : I →ₗ[F2] E) (f : (E' →ₗ[F2] F') → ℝ) (T : F →ₗ[F2] I) :
    smallCoeff ι (fun M => f (LinearEquiv.arrowCongr a b M)) T =
      smallCoeff (a.toLinearMap.comp ι) f (T.comp b.symm.toLinearMap) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.smallComponent_pullback line 83

Source documentation

The actual synthesized small component commutes with ambient pullback, with the small domain fixed and the primal codomain transported by b.

theorem smallComponent_pullback (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (ι : I →ₗ[F2] E) (f : (E' →ₗ[F2] F') → ℝ) :
    smallComponent ι (fun M => f (LinearEquiv.arrowCongr a b M)) =
      fun X => smallComponent (a.toLinearMap.comp ι) f (b.toLinearMap.comp X) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.smallComponent_pullback_apply line 102