KMSFourthMomentZoomInAlgebraLemmas.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

The frequency dichotomy behind the KMS point-restriction recursion. A row appended to a surjective frequency is either independent, or is the unique pullback of a functional on the smaller frequency space.

def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointAppend line 29
Source documentation
Append the primal value at the last coordinate.
```
def pointAppend (X : E →ₗ[F2] F) (a : F) : (E × F2) →ₗ[F2] F :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointAppend_apply line 32
def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointRestrict line 36
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.UniqueGamesTheorem.Inverse.KMSAnalytic.pointAppend
def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointLift line 40
Source documentation
Extend an injection while retaining the newly fixed coordinate.
```
def pointLift (ι : J →ₗ[F2] E) : (J × F2) →ₗ[F2] (E × F2) :=
…
```
def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointPad line 44
Source documentation
The lower-dimensional embedding into the old coordinates.
```
def pointPad (ι : J →ₗ[F2] E) : J →ₗ[F2] (E × F2) :=
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointLift_injective line 47
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointPad_injective line 54
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointLift_comp_prod line 59
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointPad_comp line 64
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.ker_le_of_not_surjective_prod line 69
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.UniqueGamesTheorem.Inverse.KMSAnalytic.not_surjective_prod_iff line 89

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.UniqueGamesTheorem.Inverse.KMSAnalytic.surjective_of_surjective_prod line 114

def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.dependentRowEquiv line 122

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.UniqueGamesTheorem.Inverse.KMSAnalytic.ker_prod_pullback line 143
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.UniqueGamesTheorem.Inverse.KMSAnalytic.frequencyProdEquiv line 175
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.UniqueGamesTheorem.Inverse.KMSAnalytic.sum_frequency_prod line 183
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.tracePair_pointAppend line 194
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.character_pointAppend line 205
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.tracePair_pointShift line 213
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.character_pointShift line 224
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointRestrict_eq_synthesis line 237
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.UniqueGamesTheorem.Inverse.KMSAnalytic.pointRestrict, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.synthesis
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.coeff_pointRestrict line 252
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointAppend_comp_basis line 280
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointRestrict_invariant line 288
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.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointRestrict
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointAppend_add line 296
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.pointRestrict_translate line 314
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.UniqueGamesTheorem.Inverse.KMSAnalytic.pointRestrict
def OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound line 353
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.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound.mono line 365
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.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound
theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound.homogeneous line 373
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.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound
theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound.pointRestrict line 383
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.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound
theorem OAI.UniqueGamesTheorem.Inverse.KMSAffineRestriction.lifted_affineDensityBound line 427
Source documentation
This supplies the local-density input of the genuine analytic induction from the actual lifted Grassmann indicator, with the exact order-two loss.
```
theorem lifted_affineDensityBound {n ell d : ℕ} {ε : ℝ}
    (S : Finset (Vertex n ell)) (hS : GrassmannPseudorandom S (2 * d) ε)
    (hε : 0 ≤ ε) : KMSFourthMoment.AffineDensityBound d ε (liftedIndicator S) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonAffineDensity.lifted_expect_in_basis_of_tuple line 467

Source documentation

The tuple hypothesis bounds the lift in every domain basis: the lift depends only on the range, which is the span of the same prescribed tuple.

theorem lifted_expect_in_basis_of_tuple (S : Finset (Vertex n ell))
    (hS : TuplePseudorandom S r ε)
    (b : Module.Basis (Fin q ⊕ Fin t) F2 (Ambient ell))
    (Q : Fin q → Ambient n) (W : Submodule F2 (Ambient n))
    (hbudget : q + (n - Module.finrank F2 W) ≤ r) :
    (𝔼 z : Fin t → W, liftedIndicator S (b.constr F2 (joinedTuple Q W z))) ≤ ε := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonAffineDensity.lifted_expect_shifted_basis_of_tuple line 485

Source documentation

Translation of the free coordinates retains the full uniform tuple law.

theorem lifted_expect_shifted_basis_of_tuple {E0 : Type*}
    [AddCommGroup E0] [Module F2 E0]
    (S : Finset (Vertex n ell)) (hS : TuplePseudorandom S r ε)
    (b : Module.Basis (Fin q ⊕ Fin t) F2 (Ambient ell))
    (Q : Fin q → Ambient n) (W : Submodule F2 (Ambient n))
    [Fintype (E0 →ₗ[F2] W)]
    (b0 : Module.Basis (Fin t) F2 E0) (T0 : E0 →ₗ[F2] W)
    (hbudget : q + (n - Module.finrank F2 W) ≤ r) :
    (𝔼 H : E0 →ₗ[F2] W, liftedIndicator S
      (b.constr F2 (joinedTuple Q W (fun i => T0 (b0 i) + H (b0 i))))) ≤ ε := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonAffineDensity.affine_expect_of_complement_of_tuple line 507

Source documentation

The adapted prefix contains all directions whose affine center lies outside W. After splitting, each fixed constrained parameter gives an allowed arbitrary prefix, and all free coordinates remain uniform in W.

theorem affine_expect_of_complement_of_tuple
    (S : Finset (Vertex n ell)) (hS : TuplePseudorandom S r ε)
    (D U E0 : Submodule F2 (Ambient ell)) (W : Submodule F2 (Ambient n))
    (hDU : D ≤ U) (hc : IsCompl U E0) (T : BasisMap n ell)
    (hE0 : E0 ≤ LinearMap.ker (W.mkQ.comp T))
    (hbudget : Module.finrank F2 U + (n - Module.finrank F2 W) ≤ r) :
    (𝔼 A : Parameter D W, restrict (liftedIndicator S) D W T A) ≤ ε := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonAffineDensity.affine_expect_bound_of_tuple line 535

Source documentation

Order d affine restrictions require at most 2d tuple restriction budget.

theorem affine_expect_bound_of_tuple {d : ℕ}
    (S : Finset (Vertex n ell)) (hS : TuplePseudorandom S (2 * d) ε)
    (D : Submodule F2 (Ambient ell)) (W : Submodule F2 (Ambient n))
    (T : BasisMap n ell) (horder : order D W ≤ d) :
    (𝔼 A : Parameter D W, restrict (liftedIndicator S) D W T A) ≤ ε := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonAffineDensity.affine_squared_expect_bound_of_tuple line 553

Source documentation

Booleanity turns the exact restriction probability into its squared norm.

theorem affine_squared_expect_bound_of_tuple {d : ℕ}
    (S : Finset (Vertex n ell)) (hS : TuplePseudorandom S (2 * d) ε)
    (D : Submodule F2 (Ambient ell)) (W : Submodule F2 (Ambient n))
    (T : BasisMap n ell) (horder : order D W ≤ d) :
    (𝔼 A : Parameter D W, (restrict (liftedIndicator S) D W T A) ^ 2) ≤ ε := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparisonAffineDensity.lifted_affineDensityBound_of_tuple line 569
Source documentation
Directly discharge the fourth-moment affine density input from the literal tuple pseudorandomness input of the ordered-basis expansion theorem.
```
theorem lifted_affineDensityBound_of_tuple {d : ℕ}
    (S : Finset (Vertex n ell)) (hS : TuplePseudorandom S (2 * d) ε) :
    KMSFourthMoment.AffineDensityBound d ε (liftedIndicator S) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound

theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound.domain_equiv line 605

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.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound

theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound.codomain_pullback line 620

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.UniqueGamesTheorem.Inverse.KMSFourthMoment.AffineDensityBound

def OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.ambientPrimalEquiv line 657
Source documentation
Reindex primal matrices by changing the ambient domain.
```
def ambientPrimalEquiv (h : E ≃ₗ[F2] E') :
    (E' →ₗ[F2] F) ≃ (E →ₗ[F2] F) where
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.ambient_character_transport line 664
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.ambient_basisInvariant_transport line 671
Source documentation
The actual invariance property is independent of the ambient coordinates.
```
theorem ambient_basisInvariant_transport (h : E ≃ₗ[F2] E')
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f) :
    KMSBasisInvariant.IsBasisInvariant (fun X : E' →ₗ[F2] F =>
      f (X.comp h.toLinearMap)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSBasisInvariant.IsBasisInvariant

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.ambient_coeff_transport line 688

Source documentation

Normalized Fourier coefficients are preserved by ambient reindexing.

theorem ambient_coeff_transport (h : E ≃ₗ[F2] E')
    (f : (E →ₗ[F2] F) → ℝ) (S : F →ₗ[F2] E) :
    linearCoeff (fun X : E' →ₗ[F2] F => f (X.comp h.toLinearMap))
      (h.toLinearMap.comp S) = linearCoeff f S := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallCoeff_ambient_transport line 708
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent_ambient_transport line 723
Source documentation
Changing the large coordinate space does not change the actual small function when both the injection and the input function are transported.
```
theorem smallComponent_ambient_transport (h : E ≃ₗ[F2] E') (ι : I →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) :
    smallComponent (h.toLinearMap.comp ι)
      (fun X : E' →ₗ[F2] F => f (X.comp h.toLinearMap)) = smallComponent ι f := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalytic.smallComponent
theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.character_codomain_composition line 759
Source documentation
Restricting the codomain of a primal map restricts the domain of its dual frequency. This identity is independent of the choice of bases.
```
theorem character_codomain_composition (J : B →ₗ[F2] F)
    (S : F →ₗ[F2] E) (X : E →ₗ[F2] B) :
    linearTraceCharacter S (J.comp X) = linearTraceCharacter (S.comp J) X := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.coefficient_codomain_pullback line 774
Source documentation
Coefficients of the actual restricted function are the unnormalized sum over exactly those original frequencies whose restriction is the new one. The statement allows arbitrary linear J; injections are the KMS use case.
```
theorem coefficient_codomain_pullback (J : B →ₗ[F2] F)
    (f : (E →ₗ[F2] F) → ℝ) (T : B →ₗ[F2] E) :
    linearCoeff (fun X => f (J.comp X)) T =
      ∑ S : F →ₗ[F2] E, if S.comp J = T then linearCoeff f S else 0 := by
…
```
theorem OAI.UniqueGamesTheorem.Inverse.KMSFourthMoment.coefficient_codomain_pullback_fiber line 796
Source documentation
The same merging identity on the actual fiber type. This form is ready for the hyperplane extension bijection, without changing normalization.
```
theorem coefficient_codomain_pullback_fiber (J : B →ₗ[F2] F)
    (f : (E →ₗ[F2] F) → ℝ) (T : B →ₗ[F2] E) :
    linearCoeff (fun X => f (J.comp X)) T =
      ∑ S : {S : F →ₗ[F2] E // S.comp J = T}, linearCoeff f S.val := by
…
```