KMSFourthMomentZoomInvariant.lean`

51 declarations, 0 contain sorry, 0 declared as axioms

Point restrictions inherit basis invariance in the remaining coordinates. Translations split into a shift of the fixed point and a translation of the remaining matrix; both identities are exact, with no probability loss.

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.pointAppend_comp_basis line 21
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.pointRestrict_invariant line 29
Source documentation
Fixing a column preserves invariance under changes of the other columns.
```
theorem pointRestrict_invariant (f : ((E × F2) →ₗ[F2] F) → ℝ)
    (hf : KMSBasisInvariant.IsBasisInvariant f) (a : F) :
    KMSBasisInvariant.IsBasisInvariant (pointRestrict f a) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalytic.pointRestrict
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.pointAppend_add line 37
theorem OAI.MaxCutGames.Inverse.KMSAnalytic.pointRestrict_translate line 55
Source documentation
A translation of the full matrix merely translates the remaining coordinates and shifts the fixed primal value.
```
theorem pointRestrict_translate (f : ((E × F2) →ₗ[F2] F) → ℝ)
    (Z : (E × F2) →ₗ[F2] F) (a : F) :
    pointRestrict (fun Y => f (Y + Z)) a =
      fun X => pointRestrict f (a + Z (0, 1))
        (X + Z.comp (LinearMap.inl F2 E F2)) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.pointRestrict
def OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound line 90
Source documentation
All affine restrictions with at most r prescribed input/output dimensions have normalized squared density at most ε. The dimension sum avoids any truncated-subtraction ambiguity.
```
def AffineDensityBound (r : ℕ) (ε : ℝ) (f : (E →ₗ[F2] F) → ℝ) : Prop :=
…
```
theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound.mono line 102
Source documentation
A stronger restriction budget supplies every smaller budget.
```
theorem AffineDensityBound.mono {r s : ℕ} (hrs : r ≤ s) (ε : ℝ)
    (f : (E →ₗ[F2] F) → ℝ) (hf : AffineDensityBound s ε f) :
    AffineDensityBound r ε f := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound
theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound.homogeneous line 110
Source documentation
The homogeneous output restriction required for Lemma 3.19 is an actual special case, using the identity domain quotient and zero affine center.
```
theorem AffineDensityBound.homogeneous [FiniteDimensional F2 E]
    (r : ℕ) (ε : ℝ) (f : (E →ₗ[F2] F) → ℝ)
    (hf : AffineDensityBound r ε f) : HomogeneousRestrictionBound r ε f := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound
theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound.pointRestrict line 120
Source documentation
Fixing one additional primal column consumes exactly one dimension of local-density budget. Its prescribed value is arbitrary, including zero.
```
theorem AffineDensityBound.pointRestrict [FiniteDimensional F2 E]
    (r : ℕ) (ε : ℝ) (f : ((E × F2) →ₗ[F2] F) → ℝ)
    (hf : AffineDensityBound (r + 1) ε f) (a : F) :
    AffineDensityBound r ε (pointRestrict f a) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound.domain_equiv line 164

Source documentation

Exact ambient coordinate transport of all sampled affine restrictions.

theorem AffineDensityBound.domain_equiv
    [FiniteDimensional F2 E] [FiniteDimensional F2 E']
    (r : ℕ) (ε : ℝ) (f : (E →ₗ[F2] F) → ℝ)
    (hf : AffineDensityBound r ε f) (e : E ≃ₗ[F2] E') :
    AffineDensityBound r ε (fun X : E' →ₗ[F2] F => f (X.comp e.toLinearMap)) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound.codomain_pullback line 179

Source documentation

Homogeneous codomain restriction uses its actual codimension budget.

theorem AffineDensityBound.codomain_pullback
    [FiniteDimensional F2 B] (r s : ℕ) (ε : ℝ)
    (f : (E →ₗ[F2] F) → ℝ) (hf : AffineDensityBound (r + s) ε f)
    (K : B →ₗ[F2] F) (hK : Function.Injective K)
    (hdimK : Module.finrank F2 F ≤ Module.finrank F2 B + s) :
    AffineDensityBound r ε (fun X : E →ₗ[F2] B => f (K.comp X)) := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound

theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.mixed_bound_of_character_bound line 223

Source documentation

The actual mixed norm for arbitrary prescribed fixed points. The rank cap and scalar constants are chosen before either ambient dimension.

theorem mixed_bound_of_character_bound (R : ℕ) (H ε : ℝ)
    (hH : 0 ≤ H) (hε : 0 ≤ ε) (π : I →ₗ[F2] J) (ν : F →ₗ[F2] J)
    (hπ : Function.Surjective π)
    (hbase : ∀ (E : Type u) [AddCommGroup E] [Module F2 E]
      [FiniteDimensional F2 E] [Fintype E],
      ∀ (ι : I →ₗ[F2] E), Function.Injective ι →
      ∀ (f : (E →ₗ[F2] F) → ℝ), KMSBasisInvariant.IsBasisInvariant f →
      AffineDensityBound (Module.finrank F2 I) ε f →
      (2 : ℝ) ^ ((Module.finrank F2 I + Module.finrank F2 J) * Module.finrank F2 E) *
        fixedFrequencyEnergy ι f π ν ≤ H * ε) :
    ∀ (n : ℕ) (E : Type u) [AddCommGroup E] [Module F2 E]
      [FiniteDimensional F2 E] [Fintype E]
…

Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.sum_comp_eq_fiber_card line 342

Source documentation

Exact sum of a function constant on the fibers of a finite map.

theorem sum_comp_eq_fiber_card (p : A → J) (b : J → ℝ) :
    (∑ x, b (p x)) =
      ∑ j, ((Finset.univ.filter fun x => p x = j).card : ℝ) * b j := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.sum_sq_eq_fiber_card line 357

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.sum_sq_eq_uniform_fiber_card line 364

Source documentation

If every orbit has the same size, its multiplicity factors out exactly.

theorem sum_sq_eq_uniform_fiber_card (p : A → J) (a : A → ℝ) (b : J → ℝ)
    (hab : ∀ x, a x = b (p x)) (n : ℕ)
    (hn : ∀ j, (Finset.univ.filter fun x => p x = j).card = n) :
    (∑ x, a x ^ 2) = (n : ℝ) * ∑ j, b j ^ 2 := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fiber_constant_energy_cross_mul line 376

Source documentation

Two coefficient arrays with the same orbit values have exactly the ratio of their orbit multiplicities. Cross multiplication includes zero-energy functions without dividing by their norm.

theorem fiber_constant_energy_cross_mul (p : A → J) (q : B → J)
    (hp : Function.Surjective p) (hq : Function.Surjective q)
    (a : A → ℝ) (b : B → ℝ)
    (hab : ∀ x y, p x = q y → a x = b y)
    (nA nB : ℕ)
    (hA : ∀ j, (Finset.univ.filter fun x => p x = j).card = nA)
    (hB : ∀ j, (Finset.univ.filter fun y => q y = j).card = nB) :
    (nB : ℝ) * (∑ x, a x ^ 2) = (nA : ℝ) * ∑ y, b y ^ 2 := by
…

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.synthesis_energy_grouped line 408

Source documentation

Parseval grouped by any genuine finite classification of frequencies.

theorem synthesis_energy_grouped (p : (F →ₗ[F2] E) → J)
    (a : (F →ₗ[F2] E) → ℝ) (b : J → ℝ) (hab : ∀ S, a S = b (p S)) :
    (𝔼 X, synthesis a X ^ 2) =
      ∑ j, ((Finset.univ.filter fun S => p S = j).card : ℝ) * b j ^ 2 := by
…

Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.synthesis

theorem OAI.MaxCutGames.Inverse.KMSAnalytic.synthesis_energy_by_kernel line 418
Source documentation
In particular, basis-invariant coefficients may be grouped by their actual kernels. The invariance premise is supplied separately by the proved change-of-basis theorem, not by any inverse or hypercontractive hypothesis.
```
theorem synthesis_energy_by_kernel [Fintype (Submodule F2 F)]
    (a : (F →ₗ[F2] E) → ℝ) (b : Submodule F2 F → ℝ)
    (hab : ∀ S, a S = b S.ker) :
    (𝔼 X, synthesis a X ^ 2) =
      ∑ K : Submodule F2 F,
        ((Finset.univ.filter fun S : F →ₗ[F2] E => S.ker = K).card : ℝ) * b K ^ 2 :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.synthesis
abbrev OAI.MaxCutGames.Inverse.KMSKernelFiberCard.F2 line 439
abbrev OAI.MaxCutGames.Inverse.KMSKernelFiberCard.KernelClass line 446
abbrev OAI.MaxCutGames.Inverse.KMSKernelFiberCard.RankFrequency line 449
abbrev OAI.MaxCutGames.Inverse.KMSKernelFiberCard.FullFrequency line 452
def OAI.MaxCutGames.Inverse.KMSKernelFiberCard.rankKernel line 456
def OAI.MaxCutGames.Inverse.KMSKernelFiberCard.fullKernel line 459
theorem OAI.MaxCutGames.Inverse.KMSKernelFiberCard.rankKernel_val line 462
theorem OAI.MaxCutGames.Inverse.KMSKernelFiberCard.fullKernel_val line 465
theorem OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.ker_comp_mkQ line 489
Source documentation
Composing an injective map with the quotient projection has exactly the prescribed kernel.
```
theorem ker_comp_mkQ (K : Submodule R F) (J : (F ⧸ K) →ₗ[R] E)
    (hJ : Function.Injective J) : (J.comp K.mkQ).ker = K := by
…
```
def OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.fixedKernelEquivQuotientInjection line 496
Source documentation
Every map with kernel K factors uniquely through an injective quotient map; the inverse sends that quotient map to its composition with K.mkQ.
```
def fixedKernelEquivQuotientInjection (K : Submodule R F) :
    {S : F →ₗ[R] E // S.ker = K} ≃
      {J : (F ⧸ K) →ₗ[R] E // Function.Injective J} where
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.fixedKernelEquiv_apply_mkQ line 513
theorem OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.fixedKernelEquiv_symm_apply line 518
theorem OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.range_forward line 523
Source documentation
Quotient factorization leaves the image subspace unchanged.
```
theorem range_forward (K : Submodule R F)
    (S : {S : F →ₗ[R] E // S.ker = K}) :
    (fixedKernelEquivQuotientInjection K S).val.range = S.val.range :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.fixedKernelEquivQuotientInjection
theorem OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.finrank_range_forward line 529
Source documentation
The quotient lift has the same rank as the original map.
```
theorem finrank_range_forward (K : Submodule R F)
    (S : {S : F →ₗ[R] E // S.ker = K}) :
    Module.finrank R (fixedKernelEquivQuotientInjection K S).val.range =
      Module.finrank R S.val.range := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.fixedKernelEquivQuotientInjection
theorem OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.fixedKernel_finrank_eq_quotient line 536
Source documentation
A prescribed kernel fixes the rank to the dimension of its quotient.
```
theorem fixedKernel_finrank_eq_quotient (K : Submodule R F)
    (S : {S : F →ₗ[R] E // S.ker = K}) :
    Module.finrank R S.val.range = Module.finrank R (F ⧸ K) := by
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.range_comp_mkQ line 544
Source documentation
Surjectivity of the quotient projection preserves the range of any map defined on the quotient.
```
theorem range_comp_mkQ (K : Submodule R F) (J : (F ⧸ K) →ₗ[R] E) :
    (J.comp K.mkQ).range = J.range := by
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.quotientInjection_comp_finrank line 556
Source documentation
The inverse factorization of an injection has quotient dimension as its rank. In the finite-dimensional binary case this is the ordinary finite rank.
```
theorem quotientInjection_comp_finrank (K : Submodule R F)
    (J : (F ⧸ K) →ₗ[R] E) (hJ : Function.Injective J) :
    Module.finrank R (J.comp K.mkQ).range = Module.finrank R (F ⧸ K) := by
…
```
theorem OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.natCard_fixedKernel_eq_injectiveQuotient line 563
Source documentation
Exact fixed-kernel count, stated without requiring a chosen enumeration.
```
theorem natCard_fixedKernel_eq_injectiveQuotient (K : Submodule R F) :
    Nat.card {S : F →ₗ[R] E // S.ker = K} =
      Nat.card {J : (F ⧸ K) →ₗ[R] E // Function.Injective J} :=
…
```

theorem OAI.MaxCutGames.Inverse.KMSAnalyticKernelCount.card_fixedKernel_eq_injectiveQuotient line 569

Source documentation

The same counting equality for any finite enumerations of the two sides.

theorem card_fixedKernel_eq_injectiveQuotient (K : Submodule R F)
    [Fintype {S : F →ₗ[R] E // S.ker = K}]
    [Fintype {J : (F ⧸ K) →ₗ[R] E // Function.Injective J}] :
    Fintype.card {S : F →ₗ[R] E // S.ker = K} =
      Fintype.card {J : (F ⧸ K) →ₗ[R] E // Function.Injective J} :=
…

def OAI.MaxCutGames.Inverse.KMSKernelFiberCard.quotientEquiv line 598
Source documentation
Equal quotient dimension gives an actual linear equivalence.
```
def quotientEquiv (K : KernelClass F I) : (F ⧸ K.val) ≃ₗ[F2] I :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSKernelFiberCard.KernelClass, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.F2
theorem OAI.MaxCutGames.Inverse.KMSKernelFiberCard.rankKernel_surjective line 603
Source documentation
Every kernel of the prescribed codimension occurs among rank-dim I maps into any ambient space whose dimension is at least dim I.
```
theorem rankKernel_surjective
    (hdim : Module.finrank F2 I ≤ Module.finrank F2 E) :
    Function.Surjective (rankKernel (F := F) (E := E) (I := I)) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSKernelFiberCard.F2, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.rankKernel
theorem OAI.MaxCutGames.Inverse.KMSKernelFiberCard.fullKernel_surjective line 619
Source documentation
Every kernel of the prescribed codimension occurs among surjections onto the comparison space, including the zero-dimensional case.
```
theorem fullKernel_surjective :
    Function.Surjective (fullKernel (F := F) (I := I)) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSKernelFiberCard.fullKernel
abbrev OAI.MaxCutGames.Inverse.KMSInjectionCount.F2 line 643
def OAI.MaxCutGames.Inverse.KMSInjectionCount.beta line 649
Source documentation
The actual number of injective linear maps, with no asymptotic convention.
```
def beta : ℕ := Nat.card {J : I →ₗ[F2] E // Function.Injective J}
```
Mentions: OAI.MaxCutGames.Inverse.KMSInjectionCount.F2
def OAI.MaxCutGames.Inverse.KMSInjectionCount.injectiveEquivIndependent line 652
Source documentation
A domain basis turns injective maps into independent image families.
```
def injectiveEquivIndependent {ι : Type*} (b : Module.Basis ι F2 I) :
    {J : I →ₗ[F2] E // Function.Injective J} ≃
      {s : ι → E // LinearIndependent F2 s} where
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSInjectionCount.F2
theorem OAI.MaxCutGames.Inverse.KMSInjectionCount.beta_eq_product line 666
Source documentation
Exact binary injection count, including the zero-dimensional domain.
```
theorem beta_eq_product [FiniteDimensional F2 I] [Finite E]
    (hdim : Module.finrank F2 I ≤ Module.finrank F2 E) :
    beta I E = ∏ j : Fin (Module.finrank F2 I),
      (2 ^ Module.finrank F2 E - 2 ^ j.val) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSInjectionCount.F2, OAI.MaxCutGames.Inverse.KMSInjectionCount.beta
def OAI.MaxCutGames.Inverse.KMSKernelFiberCard.injectionEquivOfDomainEquiv line 700
Source documentation
Changing the domain by a linear equivalence preserves the set of actual injective linear maps.
```
def injectionEquivOfDomainEquiv (e : J ≃ₗ[F2] I) :
    {u : J →ₗ[F2] E // Function.Injective u} ≃
      {u : I →ₗ[F2] E // Function.Injective u} where
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSKernelFiberCard.F2
def OAI.MaxCutGames.Inverse.KMSKernelFiberCard.fixedKernelEquivInjection line 722
Source documentation
A fixed-kernel fiber is in explicit bijection with injections from the comparison space. This includes the zero-dimensional comparison space.
```
def fixedKernelEquivInjection (K : KernelClass F I) :
    {S : F →ₗ[F2] E // S.ker = K.val} ≃
      {J : I →ₗ[F2] E // Function.Injective J} :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSKernelFiberCard.KernelClass, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.F2
theorem OAI.MaxCutGames.Inverse.KMSKernelFiberCard.natCard_fixedKernel_eq_beta line 729
Source documentation
Exact fixed-kernel count, without a chosen finite enumeration.
```
theorem natCard_fixedKernel_eq_beta (K : KernelClass F I) :
    Nat.card {S : F →ₗ[F2] E // S.ker = K.val} = beta I E :=
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSKernelFiberCard.KernelClass, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.F2
def OAI.MaxCutGames.Inverse.KMSKernelFiberCard.rankFiberEquivFixedKernel line 734
Source documentation
The kernel condition already forces the rank condition.
```
def rankFiberEquivFixedKernel (K : KernelClass F I) :
    {S : RankFrequency F E I // rankKernel S = K} ≃
      {S : F →ₗ[F2] E // S.ker = K.val} where
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSKernelFiberCard.KernelClass, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.RankFrequency, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.rankKernel, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.F2
theorem OAI.MaxCutGames.Inverse.KMSKernelFiberCard.surjective_of_kernel_class line 751
Source documentation
A map into the comparison space with this kernel has full range.
```
theorem surjective_of_kernel_class (K : KernelClass F I)
    (T : F →ₗ[F2] I) (hT : T.ker = K.val) : Function.Surjective T := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSKernelFiberCard.KernelClass, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.F2
def OAI.MaxCutGames.Inverse.KMSKernelFiberCard.fullFiberEquivFixedKernel line 759
Source documentation
The kernel condition already forces surjectivity onto the comparison space.
```
def fullFiberEquivFixedKernel (K : KernelClass F I) :
    {T : FullFrequency F I // fullKernel T = K} ≃
      {T : F →ₗ[F2] I // T.ker = K.val} where
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSKernelFiberCard.KernelClass, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.FullFrequency, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.fullKernel, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.F2
theorem OAI.MaxCutGames.Inverse.KMSKernelFiberCard.rankKernel_fiber_card line 774
Source documentation
Every rank-frequency kernel fiber has the same actual cardinality.
```
theorem rankKernel_fiber_card [Fintype (F →ₗ[F2] E)]
    (K : KernelClass F I) :
    (Finset.univ.filter (fun S : RankFrequency F E I => rankKernel S = K)).card =
      beta I E := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSKernelFiberCard.F2, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.KernelClass, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.RankFrequency, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.rankKernel
theorem OAI.MaxCutGames.Inverse.KMSKernelFiberCard.fullKernel_fiber_card line 788
Source documentation
Every surjective-frequency kernel fiber has the square injection count.
```
theorem fullKernel_fiber_card [Fintype (F →ₗ[F2] I)]
    (K : KernelClass F I) :
    (Finset.univ.filter (fun T : FullFrequency F I => fullKernel T = K)).card =
      beta I I := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSKernelFiberCard.F2, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.KernelClass, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.FullFrequency, OAI.MaxCutGames.Inverse.KMSKernelFiberCard.fullKernel