KMSAnalyticSmallInvariant.lean`

52 declarations, 0 contain sorry, 0 declared as axioms

The small-space Fourier component inherits the original function's actual basis invariance. Kernel-orbit transitivity supplies coefficient independence of the embedding; finite character reindexing supplies function invariance. There is no additional Fourier-invariance or analytic estimate hypothesis.

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallCoeff_eq_of_basisInvariant line 31
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_eq_of_basisInvariant line 41
Source documentation
Independence is equality of the actual small-space functions.
```
theorem smallComponent_eq_of_basisInvariant (ι κ : I →ₗ[F2] E)
    (hι : Function.Injective ι) (hκ : Function.Injective κ)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f) :
    smallComponent ι f = smallComponent κ f :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.surjective_postcomp_equiv line 49
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallCoeff_postcomp_equiv line 63
Source documentation
The retained coefficient array is invariant under a small-space basis change, with surjectivity and the lifted frequency kernel both preserved.
```
theorem smallCoeff_postcomp_equiv (ι : I →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (g : I ≃ₗ[F2] I) (T : F →ₗ[F2] I) :
    smallCoeff ι f (g.toLinearMap.comp T) = smallCoeff ι f T := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.smallCoeff
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_invariant line 78
Source documentation
The small component is genuinely invariant as a function on matrices.
```
theorem smallComponent_invariant (ι : I →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f) :
    KMSBasisInvariant.IsBasisInvariant (smallComponent ι f) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent
abbrev OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.Extension line 110
Source documentation
The unnormalized fiber of extensions of one compressed frequency.
```
abbrev Extension (z : B →ₗ[R] W) :=
…
```
def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.coordinatesDataEquiv line 114
Source documentation
The coordinate record has precisely three independent entries.
```
def coordinatesDataEquiv (z : B →ₗ[R] W) :
    Coordinates (A := A) (D := D) (C := C) z ≃
…
```
def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.compressedFiberDataEquiv line 122
def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.extensionEquiv line 130
Source documentation
Specifying the value on the complementary block gives every extension exactly once. This will give the cardinality factor |Hom(C,W)|.
```
def extensionEquiv (z : B →ₗ[R] W) : Extension (C := C) z ≃ (C →ₗ[R] W) where
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.Extension
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybrid_rank_coeff_assemble line 156
Source documentation
The actual hybrid and rank selectors reduce to the small component's ordinary surjectivity selector. The only remaining geometric selector is injectivity of the complementary block.
```
theorem hybrid_rank_coeff_assemble
    {z : B →ₗ[F2] W} (hz : Function.Surjective z)
    (p : Coordinates (A := A) (D := D) (C := C) z)
…
```

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergyPhase.tracePair_prod line 211

Source documentation

Each frequency block pairs with the corresponding restriction of the primal map. The trace is taken on the common codomain H.

theorem tracePair_prod (S : H →ₗ[F2] U) (T : H →ₗ[F2] V)
    (X : (U × V) →ₗ[F2] H) :
    linearTracePair X (S.prod T) =
      linearTracePair (X.comp (LinearMap.inl F2 U V)) S +
      linearTracePair (X.comp (LinearMap.inr F2 U V)) T := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergyPhase.character_prod line 227

Source documentation

Exact complex-valued phase splitting into two frequency blocks.

theorem character_prod (S : H →ₗ[F2] U) (T : H →ₗ[F2] V)
    (X : (U × V) →ₗ[F2] H) :
    linearTraceCharacter (S.prod T) X =
      linearTraceCharacter S (X.comp (LinearMap.inl F2 U V)) *
      linearTraceCharacter T (X.comp (LinearMap.inr F2 U V)) := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergyPhase.character_prod_re line 235

Source documentation

The real phases multiply because every binary trace character is real.

theorem character_prod_re (S : H →ₗ[F2] U) (T : H →ₗ[F2] V)
    (X : (U × V) →ₗ[F2] H) :
    (linearTraceCharacter (S.prod T) X).re =
      (linearTraceCharacter S (X.comp (LinearMap.inl F2 U V))).re *
      (linearTraceCharacter T (X.comp (LinearMap.inr F2 U V))).re := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergyPhase.character_prod_coprod_re line 245

Source documentation

Splitting a primal map and its dual frequency introduces no cardinal factor: both traces remain on the common space H.

theorem character_prod_coprod_re (S : H →ₗ[F2] U) (T : H →ₗ[F2] V)
    (a : U →ₗ[F2] H) (X : V →ₗ[F2] H) :
    (linearTraceCharacter (S.prod T) (a.coprod X)).re =
      (linearTraceCharacter S a).re * (linearTraceCharacter T X).re := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergyPhase.character_assemble line 260
Source documentation
The three actual block phases of the assembled Hybrid frequency.
```
theorem character_assemble {z : B →ₗ[F2] W}
    (p : Coordinates (A := A) (D := D) (C := C) z)
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergyPhase.character_assemble_re line 272
Source documentation
The real phase factorization used in the coefficient fiber sum.
```
theorem character_assemble_re {z : B →ₗ[F2] W}
    (p : Coordinates (A := A) (D := D) (C := C) z)
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergyPhase.character_assemble_eq_fullCoordinates line 285
Source documentation
The ambient character is exactly the small character after restricting the primal map along the last-block embedding.
```
theorem character_assemble_eq_fullCoordinates {z : B →ₗ[F2] W}
    (p : Coordinates (A := A) (D := D) (C := C) z)
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergyPhase.character_assemble_eq_fullCoordinates_re line 294
Source documentation
Real-valued form of the exact small-character transport.
```
theorem character_assemble_eq_fullCoordinates_re {z : B →ₗ[F2] W}
    (p : Coordinates (A := A) (D := D) (C := C) z)
…
```
def OAI.MaxCutGames.Inverse.KMSAnalytic.pointAppend line 321
Source documentation
Append the primal value at the last coordinate.
```
def pointAppend (X : E →ₗ[F2] F) (a : F) : (E × F2) →ₗ[F2] F :=
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.pointAppend_apply line 324
def OAI.MaxCutGames.Inverse.KMSAnalytic.pointRestrict line 328
Source documentation
Fix one primal column, with no averaging or normalization.
```
def pointRestrict (f : ((E × F2) →ₗ[F2] F) → ℝ) (a : F) :
    (E →ₗ[F2] F) → ℝ := fun X => f (pointAppend X a)
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.pointAppend
def OAI.MaxCutGames.Inverse.KMSAnalytic.pointLift line 332
Source documentation
Extend an injection while retaining the newly fixed coordinate.
```
def pointLift (ι : J →ₗ[F2] E) : (J × F2) →ₗ[F2] (E × F2) :=
…
```
def OAI.MaxCutGames.Inverse.KMSAnalytic.pointPad line 336
Source documentation
The lower-dimensional embedding into the old coordinates.
```
def pointPad (ι : J →ₗ[F2] E) : J →ₗ[F2] (E × F2) :=
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.pointLift_injective line 339
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.pointPad_injective line 346
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.pointLift_comp_prod line 351
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.pointPad_comp line 356
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.ker_le_of_not_surjective_prod line 361
Source documentation
A non-surjective appended row vanishes on the kernel of a surjective base frequency; the proof explicitly constructs a preimage otherwise.
```
theorem ker_le_of_not_surjective_prod (T : F →ₗ[F2] J)
    (hT : Function.Surjective T) (ell : F →ₗ[F2] F2)
    (h : ¬ Function.Surjective (T.prod ell)) : T.ker ≤ ell.ker := by
…
```

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.not_surjective_prod_iff line 381

Source documentation

Exact factorization, including uniqueness, of every dependent row.

theorem not_surjective_prod_iff (T : F →ₗ[F2] J)
    (hT : Function.Surjective T) (ell : F →ₗ[F2] F2) :
    ¬ Function.Surjective (T.prod ell) ↔
      ∃! φ : J →ₗ[F2] F2, φ.comp T = ell := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.surjective_of_surjective_prod line 406

def OAI.MaxCutGames.Inverse.KMSAnalytic.dependentRowEquiv line 414

Source documentation

Pullback along a surjection parametrizes the dependent rows exactly.

def dependentRowEquiv (T : F →ₗ[F2] J) (hT : Function.Surjective T) :
    (J →ₗ[F2] F2) ≃ {ell : F →ₗ[F2] F2 // ¬ Function.Surjective (T.prod ell)} where
…

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.ker_prod_pullback line 435
Source documentation
Dependent extension preserves the base kernel.
```
theorem ker_prod_pullback (T : F →ₗ[F2] J) (φ : J →ₗ[F2] F2) :
    (T.prod (φ.comp T)).ker = T.ker := by
…
```
def OAI.MaxCutGames.Inverse.KMSAnalytic.frequencyProdEquiv line 460
Source documentation
Splitting the last frequency row is an exact bijection.
```
def frequencyProdEquiv : ((F →ₗ[F2] E) × (F →ₗ[F2] F2)) ≃
    (F →ₗ[F2] (E × F2)) where
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.sum_frequency_prod line 468
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.tracePair_pointAppend line 479
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.character_pointAppend line 490
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.tracePair_pointShift line 498
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.character_pointShift line 509
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.pointRestrict_eq_synthesis line 522
Source documentation
Fixing a primal column merges exactly its dual frequency row.
```
theorem pointRestrict_eq_synthesis (f : ((E × F2) →ₗ[F2] F) → ℝ) (a : F) :
    pointRestrict f a = synthesis (fun T : F →ₗ[F2] E =>
      ∑ ell : F →ₗ[F2] F2, linearCoeff f (T.prod ell) * (binarySign (ell a)).re) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.pointRestrict, OAI.MaxCutGames.Inverse.KMSAnalytic.synthesis
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.coeff_pointRestrict line 537
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.sum_dependentRows line 560
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.sum_rows_split line 572

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.coeff_dependent_extension line 589

Source documentation

A dependent row changes the embedding, but not its frequency kernel.

theorem coeff_dependent_extension (ι : J →ₗ[F2] E)
    (hι : Function.Injective ι) (f : ((E × F2) →ₗ[F2] F) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : F →ₗ[F2] J) (φ : J →ₗ[F2] F2) :
    linearCoeff f ((ι.comp T).prod (φ.comp T)) =
      linearCoeff f ((pointPad ι).comp T) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.pointPad

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.point_row_recursion line 611

Source documentation

The precise rowwise identity before Fourier synthesis.

theorem point_row_recursion (ι : J →ₗ[F2] E) (hι : Function.Injective ι)
    (f : ((E × F2) →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (T : F →ₗ[F2] J) (hT : Function.Surjective T)
    (X : J →ₗ[F2] F) (a : F) :
    (∑ ell : F →ₗ[F2] F2,
      linearCoeff f ((ι.comp T).prod ell) * (binarySign (ell a)).re) *
        (linearTraceCharacter T X).re =
      (∑ ell : F →ₗ[F2] F2,
        (if Function.Surjective (T.prod ell)
          then linearCoeff f ((ι.comp T).prod ell) else 0) *
            (linearTraceCharacter (T.prod ell) (pointAppend X a)).re) +
      ∑ φ : J →ₗ[F2] F2, linearCoeff f ((pointPad ι).comp T) *
…

Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.pointAppend, OAI.MaxCutGames.Inverse.KMSAnalytic.pointPad

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.point_restriction_recursion_add line 652
Source documentation
One-column point restriction, with the dependent-row correction added back. This identity applies in every dimension, including zero.
```
theorem point_restriction_recursion_add (ι : J →ₗ[F2] E)
    (hι : Function.Injective ι) (f : ((E × F2) →ₗ[F2] F) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (X : J →ₗ[F2] F) (a : F) :
    smallComponent ι (pointRestrict f a) X =
      smallComponent (pointLift ι) f (pointAppend X a) +
        ∑ φ : J →ₗ[F2] F2, smallComponent (pointPad ι) f (X + φ.smulRight a) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent, OAI.MaxCutGames.Inverse.KMSAnalytic.pointRestrict, OAI.MaxCutGames.Inverse.KMSAnalytic.pointLift, OAI.MaxCutGames.Inverse.KMSAnalytic.pointAppend, OAI.MaxCutGames.Inverse.KMSAnalytic.pointPad
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.point_restriction_recursion line 675
Source documentation
KMS Lemma 3.8: the full-rank component after adjoining one coordinate is the restricted component minus the sum of all dependent graph terms.
```
theorem point_restriction_recursion (ι : J →ₗ[F2] E)
    (hι : Function.Injective ι) (f : ((E × F2) →ₗ[F2] F) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (X : J →ₗ[F2] F) (a : F) :
    smallComponent (pointLift ι) f (pointAppend X a) =
      smallComponent ι (pointRestrict f a) X -
        ∑ φ : J →ₗ[F2] F2, smallComponent (pointPad ι) f (X + φ.smulRight a) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent, OAI.MaxCutGames.Inverse.KMSAnalytic.pointLift, OAI.MaxCutGames.Inverse.KMSAnalytic.pointAppend, OAI.MaxCutGames.Inverse.KMSAnalytic.pointRestrict, OAI.MaxCutGames.Inverse.KMSAnalytic.pointPad
def OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy line 708
Source documentation
An arbitrary actual Fourier slice; in the mixed estimate P fixes selected frequency coordinates.
```
def sliceEnergy (P : (F →ₗ[F2] E) → Prop) (f : (E →ₗ[F2] F) → ℝ) : ℝ :=
…
```
theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy_nonneg line 712

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.coeff_translate line 717

Source documentation

Translation acts on each actual coefficient by its trace-character sign.

theorem coeff_translate (f : (E →ₗ[F2] F) → ℝ) (Z : E →ₗ[F2] F)
    (T : F →ₗ[F2] E) :
    linearCoeff (fun X => f (X + Z)) T =
      linearCoeff f T * (linearTraceCharacter T Z).re := by
…

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy_translate line 735
Source documentation
No loss from translating a function before taking a fixed Fourier slice.
```
theorem sliceEnergy_translate (P : (F →ₗ[F2] E) → Prop)
    (f : (E →ₗ[F2] F) → ℝ) (Z : E →ₗ[F2] F) :
    sliceEnergy P (fun X => f (X + Z)) = sliceEnergy P f := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy_sub_sum_le line 750

Source documentation

A finite difference of functions costs only the number of summands in its Fourier slice energy. No pointwise bound on those functions is used.

theorem sliceEnergy_sub_sum_le {J : Type*} [Fintype J]
    (P : (F →ₗ[F2] E) → Prop) (f : (E →ₗ[F2] F) → ℝ)
    (g : J → (E →ₗ[F2] F) → ℝ) :
    sliceEnergy P (fun X => f X - ∑ j, g j X) ≤
      2 * (sliceEnergy P f + (Fintype.card J : ℝ) * ∑ j, sliceEnergy P (g j)) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy_sub_translates_le line 783

Source documentation

A sum of arbitrary translates has the same quadratic slice bound with the square of the number of translates.

theorem sliceEnergy_sub_translates_le {J : Type*} [Fintype J]
    (P : (F →ₗ[F2] E) → Prop) (f g : (E →ₗ[F2] F) → ℝ)
    (Z : J → E →ₗ[F2] F) :
    sliceEnergy P (fun X => f X - ∑ j, g (X + Z j)) ≤
      2 * (sliceEnergy P f + (Fintype.card J : ℝ) ^ 2 * sliceEnergy P g) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy