KMSFourthMomentMixedRestriction.lean`

40 declarations, 0 contain sorry, 0 declared as axioms

Exact partial restrictions in product coordinates. Translating the full map shifts both the fixed and free coordinates. The latter shift preserves every actual Fourier slice energy, so finite differences of translated functions cost only the finite Cauchy factor already present before restriction.

def OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict line 25
Source documentation
Fix the first product block, leaving the second block free.
```
def partialRestrict (f : ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F) :
    (I →ₗ[F2] F) → ℝ := fun X => f (a.coprod X)
```
theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict_apply line 28

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.coprod_add_shift line 33

Source documentation

The two coordinate shifts reassemble to the original full-map shift.

theorem coprod_add_shift (a : A →ₗ[F2] F) (X : I →ₗ[F2] F)
    (Z : (A × I) →ₗ[F2] F) :
    a.coprod X + Z =
      (a + Z.comp (LinearMap.inl F2 A I)).coprod
        (X + Z.comp (LinearMap.inr F2 A I)) := by
…

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict_translate line 49

Source documentation

Restriction of a translate shifts the fixed and the free blocks.

theorem partialRestrict_translate
    (f : ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F)
    (Z : (A × I) →ₗ[F2] F) :
    partialRestrict (fun Y => f (Y + Z)) a =
      fun X => partialRestrict f (a + Z.comp (LinearMap.inl F2 A I))
        (X + Z.comp (LinearMap.inr F2 A I)) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict_sub_sum line 62

Source documentation

Partial restriction commutes exactly with a finite difference.

theorem partialRestrict_sub_sum {J : Type*} [Fintype J]
    (f : ((A × I) →ₗ[F2] F) → ℝ)
    (g : J → ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F) :
    partialRestrict (fun Y => f Y - ∑ j, g j Y) a =
      fun X => partialRestrict f a X - ∑ j, partialRestrict (g j) a X := rfl
…

Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy_partialRestrict_translate line 73
Source documentation
The free-block translation has unit Fourier phase, leaving only the shift of the fixed block in the slice energy.
```
theorem sliceEnergy_partialRestrict_translate
    (P : (F →ₗ[F2] I) → Prop)
    (f : ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F)
    (Z : (A × I) →ₗ[F2] F) :
    sliceEnergy P (partialRestrict (fun Y => f (Y + Z)) a) =
      sliceEnergy P (partialRestrict f (a + Z.comp (LinearMap.inl F2 A I))) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy, OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy_partialRestrict_sub_translates_le line 83

Source documentation

The exact finite Cauchy bound after fixing a product block. Each correction function is evaluated at its own translated fixed block.

theorem sliceEnergy_partialRestrict_sub_translates_le {J : Type*} [Fintype J]
    (P : (F →ₗ[F2] I) → Prop)
    (f : ((A × I) →ₗ[F2] F) → ℝ)
    (g : J → ((A × I) →ₗ[F2] F) → ℝ)
    (a : A →ₗ[F2] F) (Z : J → (A × I) →ₗ[F2] F) :
    sliceEnergy P (partialRestrict (fun Y => f Y - ∑ j, g j (Y + Z j)) a) ≤
      2 * (sliceEnergy P (partialRestrict f a) +
        (Fintype.card J : ℝ) * ∑ j, sliceEnergy P
          (partialRestrict (g j) (a + (Z j).comp (LinearMap.inl F2 A I)))) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy, OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict

def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.frequencyBlockEquiv line 121
Source documentation
Splitting the fixed and free frequency blocks is an exact bijection.
```
def frequencyBlockEquiv : ((F →ₗ[F2] A) × (F →ₗ[F2] I)) ≃
    (F →ₗ[F2] (A × I)) where
…
```

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sum_frequency_blocks line 130

Source documentation

The free frequency can be summed first, with no multiplicity factor.

theorem sum_frequency_blocks {M : Type*} [AddCommMonoid M]
    [Fintype (F →ₗ[F2] A)] [Fintype (F →ₗ[F2] I)]
    [Fintype (F →ₗ[F2] (A × I))]
    (g : (F →ₗ[F2] (A × I)) → M) :
    ∑ S, g S = ∑ T : F →ₗ[F2] I, ∑ alpha : F →ₗ[F2] A, g (alpha.prod T) := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.partialRestrict_eq_synthesis line 146

Source documentation

Fixing a primal block merges exactly its dual frequency block.

theorem partialRestrict_eq_synthesis
    (h : ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F) :
    partialRestrict h a = synthesis (fun T : F →ₗ[F2] I =>
      ∑ alpha : F →ₗ[F2] A,
        linearCoeff h (alpha.prod T) * (linearTraceCharacter alpha a).re) := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.coeff_partialRestrict line 165

Source documentation

The actual partial-restriction coefficient is an unnormalized frequency merge; normalized Fourier expectation introduces no additional factor.

theorem coeff_partialRestrict
    (h : ((A × I) →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F)
    (T : F →ₗ[F2] I) :
    linearCoeff (partialRestrict h a) T =
      ∑ alpha : F →ₗ[F2] A,
        linearCoeff h (alpha.prod T) * (linearTraceCharacter alpha a).re := by
…

def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.coordinateOfData line 190
def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.primalA line 195
def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.primalW line 198
def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.primalD line 201
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sum_compressedFiber line 207

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sum_alpha_hybrid_term line 234

Source documentation

One sum over the fixed frequency block is precisely the Fourier coefficient of the actual partially restricted small component.

theorem sum_alpha_hybrid_term (z : B →ₗ[F2] W) (hz : Function.Surjective z)
    (κ : (A × (W × C)) →ₗ[F2] (A × (W × D))) (hκ : Function.Injective κ)
    (f : ((A × (W × D)) →ₗ[F2] (B × C)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : (A × (W × D)) →ₗ[F2] (B × C))
    (ψ : Extension (C := C) z) (v : C →ₗ[F2] D) :
…

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

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybrid_fiber_coefficient_factorization line 268

Source documentation

Exact phase/frequency factorization in the adapted fiber. Every coefficient on the right belongs to the actual mixed partial restriction.

theorem hybrid_fiber_coefficient_factorization
    (z : B →ₗ[F2] W) (hz : Function.Surjective z)
    (κ : (A × (W × C)) →ₗ[F2] (A × (W × D))) (hκ : Function.Injective κ)
    (f : ((A × (W × D)) →ₗ[F2] (B × C)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : (A × (W × D)) →ₗ[F2] (B × C)) :
    (∑ S : {S : (B × C) →ₗ[F2] (A × (W × D)) //
        compressBlock S = z.prod (0 : B →ₗ[F2] D)},
      (if LinearIdentities.Hybrid S.val
          (LinearMap.range (LinearMap.inl F2 A (W × D)))
          (LinearMap.range (LinearMap.inl F2 B C)) then
        linearCoeff (rankComponent (Module.finrank F2 (A × (W × C))) f) S.val else 0) *
…

Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.phase_weighted_sum_sq_le line 317

Source documentation

Unit-bounded squared phases cost at most the number of summands in the finite Cauchy--Schwarz inequality.

theorem phase_weighted_sum_sq_le {Ψ : Type*} (s : Finset Ψ)
    (b H : Ψ → ℝ) (hb : ∀ ψ ∈ s, b ψ ^ 2 ≤ 1) :
    (∑ ψ ∈ s, b ψ * H ψ) ^ 2 ≤ (s.card : ℝ) * ∑ ψ ∈ s, H ψ ^ 2 := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.phase_sum_sq_le_card_sq line 329
Source documentation
A finite sum of phases has square at most the squared cardinality. The statement also covers an empty indexing type.
```
theorem phase_sum_sq_le_card_sq {V : Type*} [Fintype V]
    (a : V → ℝ) (ha : ∀ v, a v ^ 2 ≤ 1) :
    (∑ v, a v) ^ 2 ≤ (Fintype.card V : ℝ) ^ 2 := by
…
```

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sum_fiber_phase_sq_le line 339

Source documentation

Summing the Cauchy--Schwarz bounds over the disjoint restriction fibers loses only the largest fiber cardinality.

theorem sum_fiber_phase_sq_le {Ψ Z : Type*} [Fintype Ψ] [Fintype Z]
    (r : Ψ → Z) (b H : Ψ → ℝ) (maxFiber : ℕ)
    (hb : ∀ ψ, b ψ ^ 2 ≤ 1)
    (hcard : ∀ z, (Finset.univ.filter (fun ψ => r ψ = z)).card ≤ maxFiber) :
    (∑ z, (∑ ψ with r ψ = z, b ψ * H ψ) ^ 2) ≤
      (maxFiber : ℝ) * ∑ ψ, H ψ ^ 2 := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sum_fiber_product_sq_le line 364

Source documentation

The hybrid coefficient factorization has energy bounded by the squared number of complementary choices times the extension-fiber size and the original mixed coefficient energy. No phase cancellation is assumed.

theorem sum_fiber_product_sq_le {V Ψ Z : Type*}
    [Fintype V] [Fintype Ψ] [Fintype Z]
    (r : Ψ → Z) (a : V → ℝ) (b H : Ψ → ℝ) (maxFiber : ℕ)
    (ha : ∀ v, a v ^ 2 ≤ 1) (hb : ∀ ψ, b ψ ^ 2 ≤ 1)
    (hcard : ∀ z, (Finset.univ.filter (fun ψ => r ψ = z)).card ≤ maxFiber) :
    (∑ z, ((∑ v, a v) * (∑ ψ with r ψ = z, b ψ * H ψ)) ^ 2) ≤
      (Fintype.card V : ℝ) ^ 2 * (maxFiber : ℝ) * ∑ ψ, H ψ ^ 2 := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.card_restriction_fiber_eq line 402

Source documentation

The restriction fiber has exactly as many elements as the maps on its complement, before any finite-field cardinality formula is applied.

theorem card_restriction_fiber_eq {R B C W : Type*} [Ring R]
    [AddCommGroup B] [Module R B] [AddCommGroup C] [Module R C]
    [AddCommGroup W] [Module R W]
    [Fintype ((B × C) →ₗ[R] W)] [Fintype (C →ₗ[R] W)]
    (z : B →ₗ[R] W) :
    (Finset.univ.filter (fun ψ : (B × C) →ₗ[R] W =>
      ψ.comp (LinearMap.inl R B C) = z)).card = Fintype.card (C →ₗ[R] W) := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.natCard_extension line 420
Source documentation
The exact number of extensions is independent of the prescribed map.
```
theorem natCard_extension (z : B →ₗ[F2] W) :
    Nat.card (Extension (C := C) z) =
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.Extension

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.card_restriction_fiber line 427

Source documentation

The same exact count in the filtered form used by the fiber Cauchy bound.

theorem card_restriction_fiber [Fintype ((B × C) →ₗ[F2] W)]
    (z : B →ₗ[F2] W) :
    (Finset.univ.filter (fun ψ : (B × C) →ₗ[F2] W =>
      ψ.comp (LinearMap.inl F2 B C) = z)).card =
        2 ^ (Module.finrank F2 C * Module.finrank F2 W) := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.card_linearMap_eq line 444
Source documentation
Exact binary cardinality of the unrestricted complementary map space.
```
theorem card_linearMap_eq [Fintype (C →ₗ[F2] D)] :
    Fintype.card (C →ₗ[F2] D) =
      2 ^ (Module.finrank F2 C * Module.finrank F2 D) := by
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.natCard_injective_le line 452
Source documentation
Ordered independent complementary choices are no more numerous than all maps on the complementary domain; there is no basis-orbit quotient.
```
theorem natCard_injective_le :
    Nat.card {v : C →ₗ[F2] D // Function.Injective v} ≤
      2 ^ (Module.finrank F2 C * Module.finrank F2 D) := by
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.card_injective_le line 466
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.natCard_rank_subspaces_le line 479
Source documentation
Choose one ordered basis for each image. The resulting encoding gives the dimension-sensitive image count, rather than the count of all subspaces.
```
theorem natCard_rank_subspaces_le (q : ℕ) :
    Nat.card {W : Submodule F2 U // Module.finrank F2 W = q} ≤
      2 ^ (q * Module.finrank F2 U) := by
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.card_rank_subspaces_le line 486
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.count_exponent_le line 495
Source documentation
The three counting costs leave nonnegative slack in the ambient dimension exponent. The complementary image space has dimension q + d.
```
theorem count_exponent_le (a b q d : ℕ) :
    q * (q + d) + (b * d) * 2 + b * q ≤ (2 * b + q) * (a + q + d) := by
…
```

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.count_budget_le line 504

Source documentation

The actual nonnegative counts fit the mixed Fourier denominator. The bound also permits real-valued upper estimates for those counts.

theorem count_budget_le (a b q d : ℕ) (countW countV extensionFactor : ℝ)
    (hv0 : 0 ≤ countV) (he0 : 0 ≤ extensionFactor)
    (hw : countW ≤ (2 : ℝ) ^ (q * (q + d)))
    (hv : countV ≤ (2 : ℝ) ^ (b * d))
    (he : extensionFactor ≤ (2 : ℝ) ^ (b * q)) :
    countW * countV ^ 2 * extensionFactor ≤
      (2 : ℝ) ^ ((2 * b + q) * (a + q + d)) := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.count_budget_le_of_dimension line 527

Source documentation

Ambient-dimension form of the same budget, with the split dimension identity supplied by the adapted coordinates.

theorem count_budget_le_of_dimension (a b q d ell : ℕ)
    (hell : ell = a + q + d) (countW countV extensionFactor : ℝ)
    (hv0 : 0 ≤ countV) (he0 : 0 ≤ extensionFactor)
    (hw : countW ≤ (2 : ℝ) ^ (q * (ell - a)))
    (hv : countV ≤ (2 : ℝ) ^ (b * d))
    (he : extensionFactor ≤ (2 : ℝ) ^ (b * q)) :
    countW * countV ^ 2 * extensionFactor ≤ (2 : ℝ) ^ ((2 * b + q) * ell) := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sliceEnergy_fixed_snd line 566
Source documentation
An actual slice fixing the last frequency block is parametrized by all first blocks, with no multiplicity or normalization factor.
```
theorem sliceEnergy_fixed_snd (ν : F →ₗ[F2] C)
    (g : ((W × C) →ₗ[F2] F) → ℝ) :
    sliceEnergy (fun T => (LinearMap.snd F2 W C).comp T = ν) g =
      ∑ ψ : F →ₗ[F2] W, linearCoeff g (ψ.prod ν) ^ 2 := by
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sliceEnergy_snd_eq_sum line 598
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.sum_extensions_eq_filter line 614
Source documentation
Summing over actual extensions is exactly the corresponding filtered frequency sum. This identity applies to phases and squared coefficients.
```
theorem sum_extensions_eq_filter (z : B →ₗ[R] W)
    [Fintype (Extension (C := C) z)] (H : ((B × C) →ₗ[R] W) → M) :
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.Extension
def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient line 650
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.traceCharacter_re_sq line 662

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.adapted_image_energy_le_mixed line 670

Source documentation

The contribution of all surjective compressed maps onto one fixed image is bounded by the actual mixed-slice energy, with its exact extension count.

theorem adapted_image_energy_le_mixed
    (κ : (A × (W × C)) →ₗ[F2] (A × (W × D))) (hκ : Function.Injective κ)
    (f : ((A × (W × D)) →ₗ[F2] (B × C)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : (A × (W × D)) →ₗ[F2] (B × C)) :
    (∑ z ∈ Finset.univ.filter (fun z : B →ₗ[F2] W => Function.Surjective z), adaptedFiberCoefficient z f T ^ 2) ≤
      (Fintype.card (C →ₗ[F2] D) : ℝ) ^ 2 * (Fintype.card (C →ₗ[F2] W) : ℝ) *
        sliceEnergy (fun U : (B × C) →ₗ[F2] (W × C) =>
          (LinearMap.snd F2 W C).comp U = LinearMap.snd F2 B C)
          (partialRestrict (smallComponent κ f) (primalA T)) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.primalA

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.adapted_image_energy_le_of_mixed line 730

Source documentation

The conditional analytic step uses an actual mixed-slice bound as its only analytic hypothesis.

theorem adapted_image_energy_le_of_mixed
    (κ : (A × (W × C)) →ₗ[F2] (A × (W × D))) (hκ : Function.Injective κ)
    (f : ((A × (W × D)) →ₗ[F2] (B × C)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : (A × (W × D)) →ₗ[F2] (B × C)) (H : ℝ)
    (hH : sliceEnergy (fun U : (B × C) →ₗ[F2] (W × C) =>
        (LinearMap.snd F2 W C).comp U = LinearMap.snd F2 B C)
      (partialRestrict (smallComponent κ f) (primalA T)) ≤ H) :
    (∑ z ∈ Finset.univ.filter (fun z : B →ₗ[F2] W => Function.Surjective z), adaptedFiberCoefficient z f T ^ 2) ≤
      (Fintype.card (C →ₗ[F2] D) : ℝ) ^ 2 * (Fintype.card (C →ₗ[F2] W) : ℝ) * H := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.primalA, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.adaptedFiberCoefficient