OAI/Computability/MaxCut/Games/KMSAnalyticHybridEnergyImageTransportCore.lean

GitHub source file

33 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.

  1. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageAmbientEquiv line 31

    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) :=
…
  2. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imagePullback line 36

    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)) : ℝ :=
…
  3. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageTranslate line 42

    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) :=
…
  4. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageAmbientEquiv_leftRange line 47
  5. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.image_hybrid_iff line 58
  6. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.image_compression_eq_iff line 78
  7. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.image_character line 106
  8. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.image_rank_coefficient line 116
  9. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.image_coefficient_sum_transport line 130

    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)))
…
  10. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.image_fiber_coefficient_transport line 183

    Source documentation

    The original image contribution is the actual adapted fiber coefficient used by the mixed-slice estimate.

    theorem image_fiber_coefficient_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)) :
    (∑ 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 (Module.finrank F2 (A × (W × C))) f) S *
        (linearTraceCharacter S T).re else 0) =
      adaptedFiberCoefficient z (imagePullback W D h f) (imageTranslate W D h T) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imagePullback, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageTranslate

  11. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.basisInvariant_pullback line 241

    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.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant

  12. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.surjective_comp_symm_iff_inline_KMSAnalyticHybridEnergyTransportSmall line 256
  13. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.smallCoeff_pullback line 278

    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
…
  14. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.smallComponent_pullback line 297

    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
…
  15. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.smallComponent_pullback_apply line 318
  16. def OAI.MaxCutGames.Inverse.KMSAnalytic.ambientPrimalEquiv line 346

    Source documentation

    Reindex primal matrices by changing the ambient domain.

    def ambientPrimalEquiv (h : E ≃ₗ[F2] E') :
    (E' →ₗ[F2] F) ≃ (E →ₗ[F2] F) where
…
  17. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.ambient_character_transport line 353
  18. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.ambient_basisInvariant_transport line 360

    Source documentation

    The actual invariance property is independent of the ambient coordinates.

    theorem ambient_basisInvariant_transport (h : E ≃ₗ[F2] E')
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f) :
    KMSBasisInvariant.IsBasisInvariant (fun X : E' →ₗ[F2] F =>
      f (X.comp h.toLinearMap)) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant

  19. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.ambient_coeff_transport line 377

    Source documentation

    Normalized Fourier coefficients are preserved by ambient reindexing.

    theorem ambient_coeff_transport (h : E ≃ₗ[F2] E')
    (f : (E →ₗ[F2] F) → ℝ) (S : F →ₗ[F2] E) :
    linearCoeff (fun X : E' →ₗ[F2] F => f (X.comp h.toLinearMap))
      (h.toLinearMap.comp S) = linearCoeff f S := by
…
  20. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallCoeff_ambient_transport line 394
  21. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_ambient_transport line 406

    Source documentation

    Changing the large coordinate space does not change the actual small function when both the injection and the input function are transported.

    theorem smallComponent_ambient_transport (h : E ≃ₗ[F2] E') (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) :
    smallComponent (h.toLinearMap.comp ι)
      (fun X : E' →ₗ[F2] F => f (X.comp h.toLinearMap)) = smallComponent ι f := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent

  22. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.ProductMixedSliceBound line 462

    Source documentation

    The actual mixed-slice hypothesis in all coordinates adapted to the compressed image. It is a bound on smallComponent, with the original function and translate transported by the explicit product equivalence.

    def ProductMixedSliceBound (i : ℕ)
    (f : ((A × U) →ₗ[F2] (B × C)) → ℝ)
    (T : (A × U) →ₗ[F2] (B × C)) (L : ℝ) : Prop :=
…
  23. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.productFiberCoefficient line 479

    Source documentation

    The selected coefficient at one ordinary product-compressed frequency.

    def productFiberCoefficient (i : ℕ)
    (f : ((A × U) →ₗ[F2] (B × C)) → ℝ)
    (T : (A × U) →ₗ[F2] (B × C)) (Z : B →ₗ[F2] U) : ℝ :=
…
  24. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.productFiberCoefficient_imageTransport line 490

    Source documentation

    The original coefficient wrapper agrees with the adapted coefficient at the exact dimension of the small comparison space.

    theorem productFiberCoefficient_imageTransport
    (W D : Submodule F2 U) (hD : IsCompl W D) (z : B →ₗ[F2] W)
    (f : ((A × U) →ₗ[F2] (B × C)) → ℝ)
    (T : (A × U) →ₗ[F2] (B × C)) (i : ℕ)
    (hi : Module.finrank F2 (A × (W × C)) = i) :
    productFiberCoefficient i f T (W.subtype.comp z) =
      adaptedFiberCoefficient z (imagePullback W D hD f) (imageTranslate W D hD T) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.productFiberCoefficient, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imagePullback, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.imageTranslate

  25. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.product_energy_eq_filter_coefficient line 501

    Source documentation

    The exact energy identity using the product coefficient wrapper.

    theorem product_energy_eq_filter_coefficient
    (T : (A × U) →ₗ[F2] (B × C))
    (f : ((A × U) →ₗ[F2] (B × C)) → ℝ) (i : ℕ) :
    (𝔼 N, hybridDerivative (LinearMap.range (LinearMap.inl F2 A U))
      (LinearMap.range (LinearMap.inl F2 B C)) T (rankComponent i f) N ^ 2) =
      ∑ Z : B →ₗ[F2] U with
        Module.finrank F2 Z.range = i - (Module.finrank F2 A + Module.finrank F2 C),
        productFiberCoefficient i f T Z ^ 2 := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.productFiberCoefficient

  26. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.product_image_energy_le_of_mixed line 521

    Source documentation

    One actual compressed-image contribution follows from the uniform mixed-slice premise, retaining the exact finite-coordinate cost.

    theorem product_image_energy_le_of_mixed
    (i : ℕ) (f : ((A × U) →ₗ[F2] (B × C)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : (A × U) →ₗ[F2] (B × C)) (L : ℝ)
    (hi : i ≤ Module.finrank F2 (A × U))
    (ho : Module.finrank F2 A + Module.finrank F2 C ≤ i)
    (hMixed : ProductMixedSliceBound i f T L)
    (W : RankImage F2 U (i - (Module.finrank F2 A + Module.finrank F2 C))) :
    (∑ z : {z : B →ₗ[F2] W.val // Function.Surjective z},
      productFiberCoefficient i f T (W.val.subtype.comp z.val) ^ 2) ≤
      ((2 : ℝ) ^ (Module.finrank F2 C * (Module.finrank F2 U -
        (i - (Module.finrank F2 A + Module.finrank F2 C))))) ^ 2 *
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.ProductMixedSliceBound, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.RankImage, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.productFiberCoefficient

  27. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.product_hybrid_energy_le_of_mixed line 597

    Source documentation

    Actual product Hybrid derivative energy follows from the actual mixed slice estimate. Orders above the selected rank are included automatically.

    theorem product_hybrid_energy_le_of_mixed
    (i : ℕ) (f : ((A × U) →ₗ[F2] (B × C)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : (A × U) →ₗ[F2] (B × C)) (L : ℝ) (hL : 0 ≤ L)
    (hi : i ≤ Module.finrank F2 (A × U))
    (hMixed : ProductMixedSliceBound i f T L) :
    (𝔼 N, hybridDerivative (LinearMap.range (LinearMap.inl F2 A U))
      (LinearMap.range (LinearMap.inl F2 B C)) T (rankComponent i f) N ^ 2) ≤ L := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.ProductMixedSliceBound

  28. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.partialRestrict_codomain_pullback line 701

    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
…
  29. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.arrowCongr_refl_left_apply_inline_KMSAnalyticHybridEnergyTransportSmallMixed line 714
  30. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.arrowCongr_refl_right_apply_inline_KMSAnalyticHybridEnergyTransportSmallMixed line 719
  31. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.linearCoeff_postcomp_equiv line 733

    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
…
  32. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sliceEnergy_codomain_pullback line 743

    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
…
  33. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sliceEnergy_partialRestrict_smallComponent_pullback line 777

    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
…