KMSAnalyticHybridEnergyTransportSmallMixed.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact transport of mixed small-component slices

A codomain equivalence transports the fixed primal coordinates and the prescribed partial frequency together. The frequency reindexing is bijective, so the actual slice energy has no multiplicity or normalization factor.

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.partialRestrict_codomain_pullback line 34

Source documentation

Transport of the fixed block and the free block commutes with the actual partial restriction.

theorem partialRestrict_codomain_pullback (b : F ≃ₗ[F2] F')
    (g : ((A × I) →ₗ[F2] F') → ℝ) (u : A →ₗ[F2] F) :
    partialRestrict (fun Y => g (b.toLinearMap.comp Y)) u =
      fun X => partialRestrict g (b.toLinearMap.comp u) (b.toLinearMap.comp X) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.arrowCongr_refl_left_apply line 47
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.arrowCongr_refl_right_apply line 52

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

Source documentation

Exact coefficient transport for a function pulled back only in its primal codomain.

theorem linearCoeff_postcomp_equiv (b : F ≃ₗ[F2] F')
    (g : (I →ₗ[F2] F') → ℝ) (T : F →ₗ[F2] I) :
    linearCoeff (fun X => g (b.toLinearMap.comp X)) T =
      linearCoeff g (T.comp b.symm.toLinearMap) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sliceEnergy_codomain_pullback line 76

Source documentation

Transport the prescribed frequency with the codomain. This identity requires no surjectivity of the prescribed-frequency projection.

theorem sliceEnergy_codomain_pullback (b : F ≃ₗ[F2] F')
    (g : (I →ₗ[F2] F') → ℝ) (π : I →ₗ[F2] J) (ν : F →ₗ[F2] J) :
    sliceEnergy (fun T : F →ₗ[F2] I => π.comp T = ν)
      (fun X => g (b.toLinearMap.comp X)) =
      sliceEnergy (fun T : F' →ₗ[F2] I => π.comp T = ν.comp b.symm.toLinearMap) g := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.sliceEnergy_partialRestrict_smallComponent_pullback line 110

Source documentation

The actual mixed small-component energy is invariant when its ambient coordinates, embedding, fixed primal map, and prescribed frequency are all transported together.

theorem sliceEnergy_partialRestrict_smallComponent_pullback
    (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (ι : (A × I) →ₗ[F2] E) (f : (E' →ₗ[F2] F') → ℝ)
    (π : I →ₗ[F2] J) (ν : F →ₗ[F2] J) (u : A →ₗ[F2] F) :
    sliceEnergy (fun T : F →ₗ[F2] I => π.comp T = ν)
      (partialRestrict (smallComponent ι
        (fun M => f (LinearEquiv.arrowCongr a b M))) u) =
      sliceEnergy (fun T : F' →ₗ[F2] I => π.comp T = ν.comp b.symm.toLinearMap)
        (partialRestrict (smallComponent (a.toLinearMap.comp ι) f)
          (b.toLinearMap.comp u)) := by
…