KMSAnalyticHybridEnergyImageTransportLemmas.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Product Hybrid energy from actual mixed slices

The derivative's exact rank support is partitioned by its actual compressed image. Each image is put in complement coordinates, and the proved coefficient factorization bounds that contribution by an actual mixed slice. The finite image, extension, and complementary-map counts fit the mixed denominator. The sole analytic premise is the displayed uniform bound on actual slices.

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.image_fiber_coefficient_transport line 31

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.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imagePullback, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageTranslate

def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.ProductMixedSliceBound line 116
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 :=
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.productFiberCoefficient line 133
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) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.productFiberCoefficient_imageTransport line 144
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.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.productFiberCoefficient, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imagePullback, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.imageTranslate

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.product_energy_eq_filter_coefficient line 155

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.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.productFiberCoefficient

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.product_image_energy_le_of_mixed line 174

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.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.ProductMixedSliceBound, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.RankImage, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.productFiberCoefficient

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

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.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.ProductMixedSliceBound