KMSLowLevelLemmas.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

The spectral cutoff step of KMS on the actual full uniform rank-one noise. The low-level fourth-moment estimate remains an explicit input to the last combining lemma; none of these statements asserts that estimate or expansion. The multiplier is reused from the proved uniform-subspace kernel count.

def OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.rankEnergy line 42
theorem OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.sum_rankEnergy line 45

theorem OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.spectral_cutoff line 57

Source documentation

Exact rank multiplier cutoff, without dimension-dependent constants.

theorem spectral_cutoff (rank : I → ℕ) (a : I → ℝ) (r : ℕ) :
    (∑ s, ((2 : ℝ) ^ rank s)⁻¹ * a s ^ 2) ≤
      (∑ i ∈ Finset.range (r + 1), rankEnergy rank a i) +
        ((2 : ℝ) ^ (r + 1))⁻¹ * ∑ s, a s ^ 2 := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.rankEnergy

theorem OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.spectral_cutoff_of_level_bounds line 79
def OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.uniformNoise line 105
Source documentation
The actual operator samples both rank-one factors uniformly, including zero.
```
def uniformNoise (f : (E →ₗ[F2] F) → ℝ) : (E →ₗ[F2] F) → ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.uniformNoise_apply line 110
theorem OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.uniformNoise_energy line 117
theorem OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.rankEnergy_eq line 128

theorem OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.rankComponent_bound line 136

Source documentation

The scalar fourth-moment argument applied to genuine rank projections.

theorem rankComponent_bound (f : (E →ₗ[F2] F) → ℝ) (hf : IsBoolean f)
    (r i : ℕ) (ε : ℝ) (hε : 0 ≤ ε)
    (hupper : (𝔼 X, rankComponent i f X ^ 4) ≤
      (2 : ℝ) ^ (25 * r ^ 3) * (𝔼 X, rankComponent i f X ^ 2) * ε) :
    (𝔼 X, rankComponent i f X ^ 2) ≤
      (2 : ℝ) ^ (7 * r ^ 3 + 3) * ε ^ ((1 : ℝ) / 4) * (𝔼 X, f X) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.uniformNoise_bound_of_fourthMoments line 147

Source documentation

The KMS spectral conclusion once the actual pseudorandom upper fourth moments have been proved. The error, cutoff and constants precede dimensions.

theorem uniformNoise_bound_of_fourthMoments (f : (E →ₗ[F2] F) → ℝ)
    (hf : IsBoolean f) (r : ℕ) (ε : ℝ) (hε : 0 ≤ ε)
    (hupper : ∀ i ≤ r, (𝔼 X, rankComponent i f X ^ 4) ≤
      (2 : ℝ) ^ (25 * r ^ 3) * (𝔼 X, rankComponent i f X ^ 2) * ε) :
    (𝔼 X, f X * uniformNoise f X) ≤
      ((r + 1 : ℕ) * ((2 : ℝ) ^ (7 * r ^ 3 + 3) * ε ^ ((1 : ℝ) / 4)) +
        ((2 : ℝ) ^ (r + 1))⁻¹) * (𝔼 X, f X) := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.uniformNoise

theorem OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.projection_bound_of_general_fourthMoment line 183

Source documentation

No particular polynomial in the cutoff is required for the scalar step.

theorem projection_bound_of_general_fourthMoment {X : Type*} [Fintype X]
    {f : X → ℝ} (hf : IsBoolean f) (g : X → ℝ)
    (C ε : ℝ) (hC : 0 ≤ C) (hε : 0 ≤ ε)
    (hprojection : (𝔼 x, g x ^ 2) = 𝔼 x, g x * f x)
    (hupper : (𝔼 x, g x ^ 4) ≤ C * (𝔼 x, g x ^ 2) * ε) :
    (𝔼 x, g x ^ 2) ≤ (C + 1) * ε ^ ((1 : ℝ) / 4) * (𝔼 x, f x) := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.uniformNoise_bound_of_general_fourthMoments line 221

Source documentation

The actual full-uniform rank-one correlation, with a general moment constant.

theorem uniformNoise_bound_of_general_fourthMoments
    (f : (E →ₗ[F2] F) → ℝ) (hf : IsBoolean f)
    (r : ℕ) (C ε : ℝ) (hC : 0 ≤ C) (hε : 0 ≤ ε)
    (hupper : ∀ i ≤ r, (𝔼 X, rankComponent i f X ^ 4) ≤
      C * (𝔼 X, rankComponent i f X ^ 2) * ε) :
    (𝔼 X, f X * uniformNoise f X) ≤
      ((r + 1 : ℕ) * ((C + 1) * ε ^ ((1 : ℝ) / 4)) +
        ((2 : ℝ) ^ (r + 1))⁻¹) * (𝔼 X, f X) := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.uniformNoise

theorem OAI.UniqueGamesTheorem.Inverse.KMSLowLevel.exists_general_cutoff_parameters line 241

Source documentation

Even an arbitrarily large constant depending on r alone permits the cutoff and tolerance to be chosen before both dimensions.

theorem exists_general_cutoff_parameters (C : ℕ → ℝ) (hC : ∀ r, 0 ≤ C r)
    {ζ : ℝ} (hζ : 0 < ζ) :
    ∃ r : ℕ, 1 ≤ r ∧ ∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 ∧
      (r + 1 : ℕ) * ((C r + 1) * ε ^ ((1 : ℝ) / 4)) +
        ((2 : ℝ) ^ (r + 1))⁻¹ ≤ ζ / 2 := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentToExpansion.liftExpansion_of_upperMoments line 294

Source documentation

Any proved dimension-independent upper moment with a finite local budget supplies the exact ordered-basis expansion interface. This lemma is conditional until the genuine KMS small-component induction supplies hupper.

theorem liftExpansion_of_upperMoments
    (C : ℕ → ℝ) (hC : ∀ r, 0 ≤ C r) (R ellMin : ℕ → ℕ)
    (hupper : ∀ r : ℕ, ∀ ε : ℝ, 0 ≤ ε → ε ≤ 1 →
      ∀ ell : ℕ, ellMin r ≤ ell → ∀ n : ℕ,
      ∀ S : Finset (Vertex n ell), TuplePseudorandom S (R r) ε →
      ∀ i : ℕ, i ≤ r →
        (𝔼 X : BasisMap n ell, rankComponent i (liftedIndicator S) X ^ 4) ≤
          C r * (𝔼 X : BasisMap n ell, rankComponent i (liftedIndicator S) X ^ 2) * ε) :
    LiftExpansionPrinciple := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSMomentToExpansion.expansion_of_upperMoments line 335

Source documentation

Checked finite bridges and parameter choices reduce the full KMS expansion principle to the displayed actual upper-moment estimate, and nothing weaker.

theorem expansion_of_upperMoments
    (C : ℕ → ℝ) (hC : ∀ r, 0 ≤ C r) (R ellMin : ℕ → ℕ)
    (hupper : ∀ r : ℕ, ∀ ε : ℝ, 0 ≤ ε → ε ≤ 1 →
      ∀ ell : ℕ, ellMin r ≤ ell → ∀ n : ℕ,
      ∀ S : Finset (Vertex n ell), TuplePseudorandom S (R r) ε →
      ∀ i : ℕ, i ≤ r →
        (𝔼 X : BasisMap n ell, rankComponent i (liftedIndicator S) X ^ 4) ≤
          C r * (𝔼 X : BasisMap n ell, rankComponent i (liftedIndicator S) X ^ 2) * ε) :
    KMS.ExpansionPrinciple :=
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.ExpansionPrinciple

def OAI.UniqueGamesTheorem.Inverse.KMSPointComplement.pointEquivOfIsCompl line 369
Source documentation
The coordinates supplied by a complement to a nonzero point.
```
def pointEquivOfIsCompl (U : Submodule F2 E) (v : E) (hv : v ≠ 0)
    (hc : IsCompl U (Submodule.span F2 {v})) : (U × F2) ≃ₗ[F2] E :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSPointComplement.pointEquivOfIsCompl_apply line 375

theorem OAI.UniqueGamesTheorem.Inverse.KMSPointComplement.exists_aligned_point_equiv line 381

Source documentation

Every injection with a distinguished last coordinate can be expressed as pointLift after a change of coordinates on its target.

theorem exists_aligned_point_equiv (ι : (I × F2) →ₗ[F2] E)
    (hι : Function.Injective ι) :
    ∃ U : Submodule F2 E, ∃ e : (U × F2) ≃ₗ[F2] E,
      ∃ κ : I →ₗ[F2] U, Function.Injective κ ∧
        e.toLinearMap.comp (pointLift κ) = ι := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSPointComplement.exists_point_equiv line 414
Source documentation
A positive-dimensional binary space admits a last-point coordinate, with an actual subspace for the remaining coordinates and the exact dimension drop.
```
theorem exists_point_equiv [FiniteDimensional F2 E]
    (h : 0 < Module.finrank F2 E) :
    ∃ U : Submodule F2 E, ∃ _ : (U × F2) ≃ₗ[F2] E,
      Module.finrank F2 U + 1 = Module.finrank F2 E := by
…
```

theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.exists_mixed_aligned_point line 450

Source documentation

The injection can be aligned with the fixed-point shuffle on its domain.

theorem exists_mixed_aligned_point (ι : (A × I) →ₗ[F2] E)
    (hι : Function.Injective ι) (eA : (A0 × F2) ≃ₗ[F2] A) :
    ∃ U : Submodule F2 E, ∃ eE : (U × F2) ≃ₗ[F2] E,
      ∃ κ : (A0 × I) →ₗ[F2] U, Function.Injective κ ∧
        eE.toLinearMap.comp (pointLift κ) =
          ι.comp (pointShuffle eA).toLinearMap :=
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.pointShuffle

theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.smallComponent_mixed_aligned line 474

Source documentation

Exact small function after both coordinate changes.

theorem smallComponent_mixed_aligned (ι : (A × I) →ₗ[F2] E)
    (eA : (A0 × F2) ≃ₗ[F2] A) (eE : (E0 × F2) ≃ₗ[F2] E)
    (κ : (A0 × I) →ₗ[F2] E0)
    (halign : eE.toLinearMap.comp (pointLift κ) =
      ι.comp (pointShuffle eA).toLinearMap) (f : (E →ₗ[F2] F) → ℝ) :
    smallComponent (pointLift κ)
      (fun X : (E0 × F2) →ₗ[F2] F => f (X.comp eE.symm.toLinearMap)) =
      pointShuffleTransport eA (smallComponent ι f) := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.pointShuffle, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.pointShuffleTransport

theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict_smallComponent_mixed_aligned line 504

Source documentation

The original partially fixed small function is literally the function appearing on the left side of the actual one-point mixed recurrence.

theorem partialRestrict_smallComponent_mixed_aligned (ι : (A × I) →ₗ[F2] E)
    (eA : (A0 × F2) ≃ₗ[F2] A) (eE : (E0 × F2) ≃ₗ[F2] E)
    (κ : (A0 × I) →ₗ[F2] E0)
    (halign : eE.toLinearMap.comp (pointLift κ) =
      ι.comp (pointShuffle eA).toLinearMap)
    (f : (E →ₗ[F2] F) → ℝ) (a : A →ₗ[F2] F) :
    partialRestrict (smallComponent ι f) a =
      partialRestrict (pointRestrict (smallComponent (pointLift κ)
        (fun X : (E0 × F2) →ₗ[F2] F => f (X.comp eE.symm.toLinearMap)))
        (a (eA (0, 1))))
        ((a.comp eA.toLinearMap).comp (LinearMap.inl F2 A0 F2)) := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.pointShuffle, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict

theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixed_bound_of_character_bound line 556

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.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound

theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixed_slice_bound line 686

Source documentation

KMS's mixed bound with an explicit safe rank-dependent constant. Fixed points and fixed characters are arbitrary; their independence is not assumed.

theorem mixed_slice_bound (R : ℕ) (ε : ℝ) (hε : 0 ≤ ε)
    (ι : (A × I) →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (hd : AffineDensityBound (Module.finrank F2 A + Module.finrank F2 I) ε f)
    (a : A →ₗ[F2] F) (π : I →ₗ[F2] J) (hπ : Function.Surjective π)
    (ν : F →ₗ[F2] J) (hr : Module.finrank F2 A + Module.finrank F2 I ≤ R) :
    (2 : ℝ) ^ ((Module.finrank F2 I + Module.finrank F2 J) * Module.finrank F2 E) *
      sliceEnergy (fun T => π.comp T = ν) (partialRestrict (smallComponent ι f) a) ≤
        (2 : ℝ) ^ (4 * R * R) * mixedStepFactor R ^ Module.finrank F2 A * ε := by
…

Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.sliceEnergy, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.partialRestrict, OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixedStepFactor

def OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixedRankConstant line 708
Source documentation
A single uniform constant for all fixed-point dimensions at rank at most R.
```
def mixedRankConstant (R : ℕ) : ℝ := (2 : ℝ) ^ (4 * R * R) * mixedStepFactor R ^ R
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixedStepFactor
theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixedRankConstant_nonneg line 710
theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.mixed_slice_bound_uniform line 714
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.mixedMapFintype line 756
Source documentation
A consistent finite enumeration of actual binary linear maps, built from the finite vertex spaces. This is the enumeration used by the mixed theorem.
```
@[instance_reducible] def mixedMapFintype {V W : Type*}
    [AddCommGroup V] [Module F2 V] [AddCommGroup W] [Module F2 W]
    [Fintype V] [Fintype W] : Fintype (V →ₗ[F2] W) :=
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound line 771
Source documentation
All mixed small-component slices of total degree at most r, with their exact ambient normalization weight. No Hybrid derivative bound is included in this property. Fixed primal points and prescribed frequencies are arbitrary.
```
def UniformMixedBound (r : ℕ) (L : ℝ) (f : (E →ₗ[F2] F) → ℝ) : Prop :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound.pullback line 793
Source documentation
Ambient and codomain coordinate pullback preserves every actual mixed slice, while the exponent is unchanged by ambient dimension invariance.
```
theorem UniformMixedBound.pullback {r : ℕ} {L : ℝ}
    (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (f : (E' →ₗ[F2] F') → ℝ) (hf : UniformMixedBound r L f) :
    UniformMixedBound r L (fun M => f (LinearEquiv.arrowCongr a b M)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound.pullback_iff line 806
Source documentation
The uniform mixed property is independent of both ambient coordinate choices. The reverse direction is pullback by the inverse equivalences.
```
theorem UniformMixedBound.pullback_iff {r : ℕ} {L : ℝ}
    (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (f : (E' →ₗ[F2] F') → ℝ) :
    UniformMixedBound r L (fun M => f (LinearEquiv.arrowCongr a b M)) ↔
      UniformMixedBound r L f := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.uniformMixedBound_of_affineDensityBound line 832
Source documentation
The proved KMS mixed estimate discharges every instance of the uniform mixed property. Only the actual affine density and basis-invariance hypotheses remain; no Fourier or Hybrid estimate is supplied as a premise.
```
theorem uniformMixedBound_of_affineDensityBound (r : ℕ) (ε : ℝ) (hε : 0 ≤ ε)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (hd : AffineDensityBound r ε f) :
    UniformMixedBound r (mixedRankConstant r * ε) f := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound