KMSAnalyticFrequencyShift.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

The dependent branches in the KMS fixed-character recursion inject into the lower-rank restricted Fourier sum. The new coordinate value is kept fixed, so no multiplicity or ambient-dimension loss is introduced here.

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend_old_injective line 23
Source documentation
Fixing the new coordinate still allows recovery of the entire old map.
```
theorem hyperplaneExtend_old_injective (w : J) :
    Function.Injective (fun z : B →ₗ[F2] J => hyperplaneExtend z w) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend_surjective line 31
Source documentation
A surjective old frequency stays surjective after any new coordinate.
```
theorem hyperplaneExtend_surjective {z : B →ₗ[F2] J}
    (hz : Function.Surjective z) (w : J) :
    Function.Surjective (hyperplaneExtend z w) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.comp_hyperplaneExtend line 40
Source documentation
The fixed partial frequency extends by its actual projected new value.
```
theorem comp_hyperplaneExtend (π : J →ₗ[F2] K) (z : B →ₗ[F2] J) (w : J) :
    π.comp (hyperplaneExtend z w) = hyperplaneExtend (π.comp z) (π w) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.dependent_extension_energy_le line 55

Source documentation

Each fixed dependent extension branch is bounded by the genuine restricted small-component energy. There is no hidden cardinality factor.

theorem dependent_extension_energy_le
    (ι : J →ₗ[F2] E) (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (π : J →ₗ[F2] K) (A0 : B →ₗ[F2] K) (w : J) :
    (∑ z : B →ₗ[F2] J with π.comp z = A0 ∧ Function.Surjective z,
      linearCoeff f (ι.comp (hyperplaneExtend z w)) ^ 2) ≤
        fixedFrequencyEnergy ι f π (hyperplaneExtend A0 (π w)) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend, OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.coefficient_lifted_zoomOut_sq_bound line 111

Source documentation

The exact zoom-out square bound after embedding the small frequency space; the dependent sum is indexed by that small space itself.

theorem coefficient_lifted_zoomOut_sq_bound
    (ι : (J × F2) →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] (B × F2)) → ℝ) (hf : IsBasisInvariant f)
    (z : B →ₗ[F2] J) (hz : Function.Surjective z) :
    (((Fintype.card E - Fintype.card J : ℕ) : ℝ) ^ 2) *
        linearCoeff f (hyperplaneExtend ((leftEmbedding ι).comp z) (ι (0, 1))) ^ 2 ≤
      ((Fintype.card J : ℝ) + 1) *
        (linearCoeff (fun X => f ((LinearMap.inl F2 B F2).comp X))
            ((leftEmbedding ι).comp z) ^ 2 +
          ∑ w : J, linearCoeff f ((leftEmbedding ι).comp (hyperplaneExtend z w)) ^ 2) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend, OAI.MaxCutGames.Inverse.KMSAnalytic.leftEmbedding

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedCharacter_step_sum line 134

Source documentation

Summing the genuine pointwise recurrence bounds every dependent branch by an actual lower-rank fixed-character energy, with no missing multiplicity.

theorem fixedCharacter_step_sum
    (ι : (J × F2) →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] (B × F2)) → ℝ) (hf : IsBasisInvariant f)
    (π : J →ₗ[F2] K) (A : B →ₗ[F2] K) :
    (((Fintype.card E - Fintype.card J : ℕ) : ℝ) ^ 2) *
        (∑ z ∈ Finset.univ.filter (fun z : B →ₗ[F2] J =>
            π.comp z = A ∧ Function.Surjective z),
          linearCoeff f (hyperplaneExtend ((leftEmbedding ι).comp z) (ι (0, 1))) ^ 2) ≤
      ((Fintype.card J : ℝ) + 1) *
        (fixedFrequencyEnergy (leftEmbedding ι)
          (fun X : E →ₗ[F2] B => f ((LinearMap.inl F2 B F2).comp X)) π A +
        ∑ w : J, fixedFrequencyEnergy (leftEmbedding ι) f π (hyperplaneExtend A (π w))) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend, OAI.MaxCutGames.Inverse.KMSAnalytic.leftEmbedding, OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy

def OAI.MaxCutGames.Inverse.KMSAnalytic.blockFrequency line 194
Source documentation
Adjoin a new identity coordinate and an arbitrary off-diagonal vector.
```
def blockFrequency (z : B →ₗ[F2] J) (w : J) : (B × F2) →ₗ[F2] (J × F2) :=
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.blockFrequency_apply line 197
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.blockFrequency_surjective_iff line 200
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.ker_blockFrequency line 215
Source documentation
The kernel is independent of the off-diagonal vector, without any surjectivity assumption.
```
theorem ker_blockFrequency (z : B →ₗ[F2] J) (w : J) :
    (blockFrequency z w).ker = z.ker.prod (⊥ : Submodule F2 F2) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.blockFrequency
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.blockFrequency_compatible_iff line 226
def OAI.MaxCutGames.Inverse.KMSAnalytic.blockOld line 243
def OAI.MaxCutGames.Inverse.KMSAnalytic.blockNew line 246
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.blockOld_blockFrequency line 248
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.blockNew_blockFrequency line 253
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.blockFrequency_recover line 256
abbrev OAI.MaxCutGames.Inverse.KMSAnalytic.CompatibleBlockFrequency line 269
abbrev OAI.MaxCutGames.Inverse.KMSAnalytic.CompatibleOldFrequency line 274
def OAI.MaxCutGames.Inverse.KMSAnalytic.compatibleBlockFrequencyEquiv line 278
Source documentation
The actual compatible frequency fiber, with its exact kernel-vector parameter.
```
def compatibleBlockFrequencyEquiv (π : J →ₗ[F2] K) (A : B →ₗ[F2] K) :
    CompatibleBlockFrequency π A ≃ CompatibleOldFrequency π A × π.ker where
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.CompatibleBlockFrequency, OAI.MaxCutGames.Inverse.KMSAnalytic.CompatibleOldFrequency

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.coefficient_blockFrequency_eq line 304

Source documentation

Actual lifted coefficients are independent of the block vector.

theorem coefficient_blockFrequency_eq (ι : (J × F2) →ₗ[F2] E)
    (hι : Function.Injective ι) (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (z : B →ₗ[F2] J) (u v : J) :
    linearCoeff f (ι.comp (blockFrequency z u)) =
      linearCoeff f (ι.comp (blockFrequency z v)) := by
…

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

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_block line 322

Source documentation

Exact collapse of the new-coordinate fiber in the prescribed-frequency energy. The multiplier is the actual number of vectors in ker π.

theorem fixedFrequencyEnergy_block (ι : (J × F2) →ₗ[F2] E)
    (hι : Function.Injective ι) (f : (E →ₗ[F2] (B × F2)) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (π : J →ₗ[F2] K) (A : B →ₗ[F2] K) :
    fixedFrequencyEnergy ι f (π.prodMap (LinearMap.id : F2 →ₗ[F2] F2))
      (A.prodMap (LinearMap.id : F2 →ₗ[F2] F2)) =
      (Fintype.card π.ker : ℝ) * ∑ z : CompatibleOldFrequency π A,
        linearCoeff f (ι.comp (blockFrequency z.val 0)) ^ 2 := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy, OAI.MaxCutGames.Inverse.KMSAnalytic.CompatibleOldFrequency, OAI.MaxCutGames.Inverse.KMSAnalytic.blockFrequency

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.comp_blockFrequency_zero line 372

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_product_step line 397

Source documentation

A genuine one-step recurrence in the actual restricted Fourier energy. Every term on the right has one fewer small-space dimension and one fewer fixed character.

theorem fixedFrequencyEnergy_product_step
    (ι : (J × F2) →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] (B × F2)) → ℝ) (hf : IsBasisInvariant f)
    (π : J →ₗ[F2] K) (A : B →ₗ[F2] K) :
    (((Fintype.card E - Fintype.card J : ℕ) : ℝ) ^ 2) *
        fixedFrequencyEnergy ι f (π.prodMap (LinearMap.id : F2 →ₗ[F2] F2))
          (A.prodMap (LinearMap.id : F2 →ₗ[F2] F2)) ≤
      (Fintype.card π.ker : ℝ) * (((Fintype.card J : ℝ) + 1) *
        (fixedFrequencyEnergy (leftEmbedding ι)
          (fun X : E →ₗ[F2] B => f ((LinearMap.inl F2 B F2).comp X)) π A +
        ∑ w : J, fixedFrequencyEnergy (leftEmbedding ι) f π (hyperplaneExtend A (π w)))) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy, OAI.MaxCutGames.Inverse.KMSAnalytic.leftEmbedding, OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedCharacter_constant_step line 437

Source documentation

The recurrence cost in Lemma 3.19 is absorbed by 2^(4 i²). The proof only needs n < ell, weaker than the usual 2*(n+1) ≤ ell induction hypothesis.

theorem fixedCharacter_constant_step (n m ell : ℕ) (hnell : n < ell) :
    (2 : ℝ) ^ n * ((2 : ℝ) ^ n + 1) ^ 2 * (2 : ℝ) ^ (4 * n * n) /
        ((((2 : ℝ) ^ ell - (2 : ℝ) ^ n) ^ 2) * (2 : ℝ) ^ ((n + m) * ell)) ≤
      (2 : ℝ) ^ (4 * (n + 1) * (n + 1)) /
        (2 : ℝ) ^ (((n + 1) + (m + 1)) * ell) := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_product_bound line 530

Source documentation

The fixed-character recurrence preserves the explicit quadratic constant. No local-density or Fourier bound is hidden in the scalar accounting.

theorem fixedFrequencyEnergy_product_bound
    (ι : (J × F2) →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] (B × F2)) → ℝ) (hf : IsBasisInvariant f)
    (π : J →ₗ[F2] K) (A : B →ₗ[F2] K) (ε : ℝ) (hε : 0 ≤ ε)
    (hfirst : (2 : ℝ) ^ ((Module.finrank F2 J + Module.finrank F2 K) *
        Module.finrank F2 E) * fixedFrequencyEnergy (leftEmbedding ι)
        (fun X : E →ₗ[F2] B => f ((LinearMap.inl F2 B F2).comp X)) π A ≤
      (2 : ℝ) ^ (4 * Module.finrank F2 J * Module.finrank F2 J) * ε)
    (hlower : ∀ w : J, (2 : ℝ) ^ ((Module.finrank F2 J + Module.finrank F2 K) *
        Module.finrank F2 E) * fixedFrequencyEnergy (leftEmbedding ι) f π
        (hyperplaneExtend A (π w)) ≤
      (2 : ℝ) ^ (4 * Module.finrank F2 J * Module.finrank F2 J) * ε) :
…

Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy, OAI.MaxCutGames.Inverse.KMSAnalytic.leftEmbedding, OAI.MaxCutGames.Inverse.KMSAnalytic.hyperplaneExtend

def OAI.MaxCutGames.Inverse.KMSAnalytic.codomainTransport line 654
def OAI.MaxCutGames.Inverse.KMSAnalytic.codomainFrequencyEquiv line 658
Source documentation
Actual dual frequencies are reindexed by precomposition with the inverse.
```
def codomainFrequencyEquiv (e : F ≃ₗ[F2] F') : (F →ₗ[F2] I) ≃ (F' →ₗ[F2] I) where
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.codomainFrequencyEquiv_apply line 664
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.codomainFrequency_cancel line 667
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.surjective_comp_codomainEquiv_iff line 670
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.linearCoeff_codomainTransport line 687
Source documentation
The Fourier pullback fiber of a codomain equivalence has a single term.
```
theorem linearCoeff_codomainTransport (e : F ≃ₗ[F2] F')
    (f : (E →ₗ[F2] F) → ℝ) (S' : F' →ₗ[F2] E) :
    linearCoeff (codomainTransport e f) S' = linearCoeff f (S'.comp e.toLinearMap) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.codomainTransport
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.basisInvariant_codomainTransport line 707
Source documentation
Codomain transport preserves the original basis invariance.
```
theorem basisInvariant_codomainTransport (e : F ≃ₗ[F2] F')
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f) :
    KMSBasisInvariant.IsBasisInvariant (codomainTransport e f) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.codomainTransport
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallCoeff_codomainTransport line 722
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent_codomainTransport line 734
Source documentation
The synthesized small component itself commutes with codomain transport.
```
theorem smallComponent_codomainTransport (e : F ≃ₗ[F2] F') (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) :
    smallComponent ι (codomainTransport e f) =
      codomainTransport e (smallComponent ι f) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.smallComponent, OAI.MaxCutGames.Inverse.KMSAnalytic.codomainTransport
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_codomainTransport line 747
Source documentation
Transport the prescribed partial frequency together with the primal codomain; the normalized energy remains exactly unchanged.
```
theorem fixedFrequencyEnergy_codomainTransport (e : F ≃ₗ[F2] F') (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) (π : I →ₗ[F2] J) (A : F →ₗ[F2] J) :
    fixedFrequencyEnergy ι (codomainTransport e f) π (A.comp e.symm.toLinearMap) =
      fixedFrequencyEnergy ι f π A := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy, OAI.MaxCutGames.Inverse.KMSAnalytic.codomainTransport