KMSFourthMomentMixedScalarLemmas.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

Scalar accounting for the genuine point-restriction induction. All ambient weights remain explicit. A global rank cap R gives a dimension-independent factor per fixed point; the proof does not assume any mixed-norm estimate.

def OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixedStepFactor line 34
Source documentation
A deliberately generous rank-dependent cost for one fixed point.
```
def mixedStepFactor (R : ℕ) : ℝ := 2 ^ (2 * R + 2)
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixedStepFactor_nonneg line 36
theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.one_le_mixedStepFactor line 40
theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixed_step_factor_bound line 45
Source documentation
Character dimension is at most the number of free coordinates, so the ambient-weight ratio has exponent at most twice the rank cap.
```
theorem mixed_step_factor_bound (R t n : ℕ) (ht : t ≤ 2 * R) (hn : n ≤ R) :
    2 * ((2 : ℝ) ^ t + ((2 : ℝ) ^ n) ^ 2) ≤ mixedStepFactor R := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixedStepFactor
theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixed_weighted_step line 63
Source documentation
The two lower estimates live in adjacent ambient dimensions. Multiplying by the new weight costs q on the point-restricted branch, and nothing on the unrestricted lower-component branch.
```
theorem mixed_weighted_step {M A B q w n C : ℝ}
    (hq : 0 ≤ q) (hw : 0 ≤ w)
    (hrec : M ≤ 2 * (A + n ^ 2 * B))
    (hA : w * A ≤ C) (hB : (q * w) * B ≤ C) :
    (q * w) * M ≤ 2 * (q + n ^ 2) * C := by
…
```

theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixed_weighted_step_pow line 78

Source documentation

The complete scalar induction step with a rank-independent ambient weight and a rank-dependent but dimension-independent loss.

theorem mixed_weighted_step_pow (R s ell t n : ℕ) (H ε M A B : ℝ)
    (hH : 0 ≤ H) (hε : 0 ≤ ε) (ht : t ≤ 2 * R) (hn : n ≤ R)
    (hrec : M ≤ 2 * (A + ((2 : ℝ) ^ n) ^ 2 * B))
    (hA : (2 : ℝ) ^ (t * ell) * A ≤ H * mixedStepFactor R ^ s * ε)
    (hB : (2 : ℝ) ^ (t * (ell + 1)) * B ≤ H * mixedStepFactor R ^ s * ε) :
    (2 : ℝ) ^ (t * (ell + 1)) * M ≤ H * mixedStepFactor R ^ (s + 1) * ε := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixedStepFactor

abbrev OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.F2 line 116
def OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta line 122
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.UniqueGamesTheorem.Inverse.KMSInjectionCount.F2
def OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.injectiveEquivIndependent line 125
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.UniqueGamesTheorem.Inverse.KMSInjectionCount.F2
theorem OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta_eq_product line 139
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.UniqueGamesTheorem.Inverse.KMSInjectionCount.F2, OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta
theorem OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.binary_factor_lower line 162
theorem OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta_le_pow line 178
theorem OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta_ge_pow line 188
theorem OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta_positive line 201
theorem OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta_self_le line 205
theorem OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.pow_dim_mul_le_pow_sq_mul_beta line 228
Source documentation
A subtraction-free form of the lower injection count.
```
theorem pow_dim_mul_le_pow_sq_mul_beta
    (hdim : Module.finrank F2 I ≤ Module.finrank F2 E) :
    (2 : ℝ) ^ (Module.finrank F2 I * Module.finrank F2 E) ≤
      (2 : ℝ) ^ (Module.finrank F2 I * Module.finrank F2 I) * (beta I E : ℝ) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.F2, OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta
theorem OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta_ratio_le_pow line 246
Source documentation
The small-to-ambient injection ratio, with the full ambient exponent.
```
theorem beta_ratio_le_pow [Finite I]
    (hdim : Module.finrank F2 I ≤ Module.finrank F2 E) :
    (beta I I : ℝ) / (beta I E : ℝ) ≤
      (2 : ℝ) ^ (2 * (Module.finrank F2 I * Module.finrank F2 I)) /
        (2 : ℝ) ^ (Module.finrank F2 I * Module.finrank F2 E) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.F2, OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta

theorem OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.pow_mul_le_of_beta_cross_mul line 273

Source documentation

Convert a count-weighted energy identity into a clean dimension bound.

theorem pow_mul_le_of_beta_cross_mul [Finite I]
    (hdim : Module.finrank F2 I ≤ Module.finrank F2 E)
    {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y)
    (hcross : (beta I E : ℝ) * x = (beta I I : ℝ) * y) :
    (2 : ℝ) ^ (Module.finrank F2 I * Module.finrank F2 E) * x ≤
      (2 : ℝ) ^ (2 * (Module.finrank F2 I * Module.finrank F2 I)) * y := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.F2, OAI.UniqueGamesTheorem.Inverse.KMSInjectionCount.beta

abbrev OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.F2 line 314
abbrev OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.KernelClass line 321
abbrev OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.RankFrequency line 324
abbrev OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.FullFrequency line 327
def OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.rankKernel line 331
def OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.fullKernel line 334
theorem OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.rankKernel_val line 337
theorem OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.fullKernel_val line 340
def OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.quotientEquiv line 369
Source documentation
Equal quotient dimension gives an actual linear equivalence.
```
def quotientEquiv (K : KernelClass F I) : (F ⧸ K.val) ≃ₗ[F2] I :=
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.KernelClass, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.F2
theorem OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.rankKernel_surjective line 374
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.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.F2, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.rankKernel
theorem OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.fullKernel_surjective line 390
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.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.fullKernel
def OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.injectionEquivOfDomainEquiv line 430
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.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.F2
def OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.fixedKernelEquivInjection line 452
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.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.KernelClass, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.F2
theorem OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.natCard_fixedKernel_eq_beta line 459
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.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.KernelClass, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.F2
def OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.rankFiberEquivFixedKernel line 464
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.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.KernelClass, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.RankFrequency, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.rankKernel, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.F2
theorem OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.surjective_of_kernel_class line 481
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.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.KernelClass, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.F2
def OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.fullFiberEquivFixedKernel line 489
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.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.KernelClass, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.FullFrequency, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.fullKernel, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.F2
theorem OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.rankKernel_fiber_card line 504
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.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.F2, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.KernelClass, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.RankFrequency, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.rankKernel
theorem OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.fullKernel_fiber_card line 518
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.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.F2, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.KernelClass, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.FullFrequency, OAI.UniqueGamesTheorem.Inverse.KMSKernelFiberCard.fullKernel
def OAI.UniqueGamesTheorem.Inverse.KMSKernelOrbits.rangeEquivOfKerEq line 553
Source documentation
The range identification induced by a common kernel.
```
def rangeEquivOfKerEq (S T : F →ₗ[K] E) (hker : S.ker = T.ker) :
    S.range ≃ₗ[K] T.range :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSKernelOrbits.rangeEquivOfKerEq_apply line 560
Source documentation
This identification respects every original vector, including vectors in the kernel and maps of rank zero.
```
theorem rangeEquivOfKerEq_apply (S T : F →ₗ[K] E) (hker : S.ker = T.ker) (x : F) :
    (rangeEquivOfKerEq S T hker ⟨S x, ⟨x, rfl⟩⟩ : E) = T x := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSKernelOrbits.rangeEquivOfKerEq
theorem OAI.UniqueGamesTheorem.Inverse.KMSKernelOrbits.exists_postcomp_equiv_of_ker_eq line 571
Source documentation
Finite-dimensional image suffices: the ambient codomain and domain may otherwise be infinite-dimensional.
```
theorem exists_postcomp_equiv_of_ker_eq (S T : F →ₗ[K] E)
    [FiniteDimensional K S.range] (hker : S.ker = T.ker) :
    ∃ g : E ≃ₗ[K] E, g.toLinearMap.comp S = T := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSKernelOrbits.ker_eq_iff_exists_postcomp_equiv line 583
Source documentation
Invertible postcomposition never changes the kernel. Thus the kernel is an exact orbit invariant, rather than only a necessary condition.
```
theorem ker_eq_iff_exists_postcomp_equiv (S T : F →ₗ[K] E)
    [FiniteDimensional K S.range] :
    S.ker = T.ker ↔ ∃ g : E ≃ₗ[K] E, g.toLinearMap.comp S = T := by
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.IsBoolean line 606
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.boolean_nonneg line 609
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.boolean_sq line 613
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.boolean_average_nonneg line 616
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.boolean_squared_average line 619
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.boolean_fourth_holder line 626
Source documentation
Two finite Cauchy–Schwarz steps, with the Boolean support kept explicitly.
```
theorem boolean_fourth_holder {f : X → ℝ} (hf : IsBoolean f) (g : X → ℝ) :
    (𝔼 x, g x * f x) ^ 4 ≤ (𝔼 x, g x ^ 4) * (𝔼 x, f x) ^ 3 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.IsBoolean
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.projection_energy_le_density line 656
Source documentation
The squared norm of an orthogonal component is bounded by the Boolean function's density. The projection identity is the only needed property.
```
theorem projection_energy_le_density {f : X → ℝ} (hf : IsBoolean f) (g : X → ℝ)
    (hprojection : (𝔼 x, g x ^ 2) = 𝔼 x, g x * f x) :
    (𝔼 x, g x ^ 2) ≤ 𝔼 x, f x := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.IsBoolean
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.projection_fifth_le_density_fourth_moment line 667
Source documentation
A stronger lower fourth-moment estimate than KMS Lemma 2.14, avoiding division by the density and remaining valid at density zero.
```
theorem projection_fifth_le_density_fourth_moment {f : X → ℝ} (hf : IsBoolean f)
    (g : X → ℝ) (hprojection : (𝔼 x, g x ^ 2) = 𝔼 x, g x * f x) :
    (𝔼 x, g x ^ 2) ^ 5 ≤ (𝔼 x, f x) ^ 4 * (𝔼 x, g x ^ 4) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.IsBoolean
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.fourth_root_power line 682
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.le_of_fourth_power_le line 687
theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentScalar.lowLevel_bound_of_fourthMoment line 694
theorem OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.exists_cutoff_parameters line 746
Source documentation
The level cutoff and pseudorandomness tolerance are selected before either matrix dimension. The inequality leaves half the retention budget for model comparison errors.
```
theorem exists_cutoff_parameters {ζ : ℝ} (hζ : 0 < ζ) :
    ∃ r : ℕ, 1 ≤ r ∧ ∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 ∧
      (r + 1 : ℕ) * ((2 : ℝ) ^ (7 * r ^ 3 + 3) * ε ^ ((1 : ℝ) / 4)) +
        ((2 : ℝ) ^ (r + 1))⁻¹ ≤ ζ / 2 := by
…
```