RestrictionLemmas.lean`

79 declarations, 0 contain sorry, 0 declared as axioms

Actual Fourier degree loss for both derivative operators. The support cutoffs apply to genuine binary linear maps, including the case where the total derivative order is larger than the original degree.

def OAI.UniqueGamesTheorem.Appendix.Restriction.isum line 21
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.isum_congr line 25
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.isum_zero line 31
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.isum_add line 36
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.isum_mul_left line 42
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.isum_mul_right line 48
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.isum_const line 54
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.isum_swap line 63
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.isum_map line 69
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.isum_perm line 75
def OAI.UniqueGamesTheorem.Appendix.Restriction.binarySign line 84
Source documentation
The binary character is multiplicative across addition of its exponents.
```
def binarySign (b : Bool) : Int := if b then -1 else 1
```
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.binarySign_xor line 86

theorem OAI.UniqueGamesTheorem.Appendix.Restriction.binary_character_restriction line 93

Source documentation

The character part of (A.1), given the trace-pairing compatibility equation. traceCompatibility states the actual mathematical hypothesis still required when instantiating this result with binary matrix spaces and quotient maps.

theorem binary_character_restriction {M N Y Z : Type}
    (translate : M → N → M) (compress : Y → Z)
    (ambientPair : Y → M → Bool) (restrictedPair : Z → N → Bool)
    (traceCompatibility : ∀ y t n,
      ambientPair y (translate t n) = (ambientPair y t).xor (restrictedPair (compress y) n))
    (y : Y) (t : M) (n : N) :
    binarySign (ambientPair y (translate t n)) =
      binarySign (ambientPair y t) * binarySign (restrictedPair (compress y) n) := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.Restriction.binarySign

theorem OAI.UniqueGamesTheorem.Appendix.Restriction.coefficient_merging line 110

Source documentation

Raw coefficient form of frequency merging in (A.1).

When f is synthesized as sum_y coeff(y) * ambient(y, t+n), the raw restricted coefficient at z is the cardinality of the restricted domain times the sum of translated coefficients with compress y = z. Normalized coefficients divide the displayed equation by that cardinality.

theorem coefficient_merging {M N Y Z : Type} [DecidableEq Z]
    (ys : List Y) (ns : List N) (translate : M → N → M) (compress : Y → Z)
    (ambient : Y → M → Int) (restricted : Z → N → Int) (coeff : Y → Int)
    (compatibility : ∀ y t n,
      ambient y (translate t n) = ambient y t * restricted (compress y) n)
    (orthogonality : ∀ y z,
      isum ns (fun n => restricted (compress y) n * restricted z n) =
        if compress y = z then (ns.length : Int) else 0)
    (t : M) (z : Z) :
    isum ns (fun n =>
      isum ys (fun y => coeff y * ambient y (translate t n)) * restricted z n) =
    (ns.length : Int) *
…

Mentions: OAI.UniqueGamesTheorem.Appendix.Restriction.isum

theorem OAI.UniqueGamesTheorem.Appendix.Restriction.restriction_average line 156
Source documentation
The raw finite-sum translation identity behind (A.2).
For every fixed restriction point n, translation permutes the ambient list. Consequently summing an arbitrary integer observable over all translates and restriction points multiplies its ambient sum by the restriction-domain size. One may use an integer-valued moment as the observable.
```
theorem restriction_average {M N : Type}
    (ms : List M) (ns : List N) (translate : M → N → M)
    (translationPermutes : ∀ n, (ms.map (fun t => translate t n)).Perm ms)
    (observable : M → Int) :
    isum ms (fun t => isum ns (fun n => observable (translate t n))) =
      (ns.length : Int) * isum ms observable := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.Restriction.isum
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.bool_translation_perm line 172
Source documentation
Concrete translation-permutation verification for the one-bit space.
```
theorem bool_translation_perm (n : Bool) :
    ([false, true].map (fun t => t.xor n)).Perm [false, true] := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.bool_restriction_average line 179
Source documentation
Fully instantiated one-bit averaging, with any list of restriction points.
```
theorem bool_restriction_average (ns : List Bool) (observable : Bool → Int) :
    isum [false, true] (fun t => isum ns (fun n => observable (t.xor n))) =
      (ns.length : Int) * isum [false, true] observable :=
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.Restriction.isum
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.bool_character_compatibility line 185
Source documentation
Character compatibility instantiated on the binary one-dimensional space.
```
theorem bool_character_compatibility (y t n : Bool) :
    binarySign (y && (t.xor n)) = binarySign (y && t) * binarySign (y && n) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.Restriction.binarySign
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.bool_character_orthogonality line 190
Source documentation
Fourier orthogonality instantiated on the binary one-dimensional space.
```
theorem bool_character_orthogonality (y z : Bool) :
    isum [false, true] (fun n => binarySign (y && n) * binarySign (z && n)) =
      if y = z then (2 : Int) else 0 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.Restriction.isum, OAI.UniqueGamesTheorem.Appendix.Restriction.binarySign
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.bool_coefficient_merging line 196
Source documentation
A complete instance of the coefficient theorem with no character hypotheses.
```
theorem bool_coefficient_merging (coeff : Bool → Int) (t z : Bool) :
    isum [false, true] (fun n =>
      isum [false, true] (fun y => coeff y * binarySign (y && (t.xor n))) *
        binarySign (z && n)) =
      2 * (coeff z * binarySign (z && t)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.Restriction.isum, OAI.UniqueGamesTheorem.Appendix.Restriction.binarySign

theorem OAI.UniqueGamesTheorem.Appendix.Restriction.real_translation_average line 218

Source documentation

Averaging any real observable over translates of any finite parametrized perturbation preserves its normalized mean.

theorem real_translation_average {G N : Type*} [AddCommGroup G] [Fintype G]
    [Fintype N] [Nonempty N] (embed : N → G) (observable : G → ℝ) :
    (𝔼 t, 𝔼 n, observable (t + embed n)) = 𝔼 t, observable t := by
…

def OAI.UniqueGamesTheorem.Appendix.Restriction.compressFrequency line 236
Source documentation
The actual quotient-and-restriction map on Fourier indices in (A.1).
```
def compressFrequency (A : Submodule F2 E) (B : Submodule F2 F)
    (Y : F →ₗ[F2] E) : B →ₗ[F2] (E ⧸ A) :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.linear_trace_restriction line 242
Source documentation
Trace compatibility on the actual quotient restriction.
```
theorem linear_trace_restriction (A : Submodule F2 E) (B : Submodule F2 F)
    (Y : F →ₗ[F2] E) (N : UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter A B) :
    linearTracePair (UniqueGamesTheorem.Fourier.MatrixRestrictions.embed A B N) Y =
      linearTracePair N (compressFrequency A B Y) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.embed, OAI.UniqueGamesTheorem.Appendix.Restriction.compressFrequency

theorem OAI.UniqueGamesTheorem.Appendix.Restriction.linear_character_restriction line 253

Source documentation

The complex character identity in (A.1), on actual binary linear maps.

theorem linear_character_restriction (A : Submodule F2 E) (B : Submodule F2 F)
    (Y : F →ₗ[F2] E) (T : E →ₗ[F2] F)
    (N : UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter A B) :
    linearTraceCharacter Y (T + UniqueGamesTheorem.Fourier.MatrixRestrictions.embed A B N) =
      linearTraceCharacter Y T * linearTraceCharacter (compressFrequency A B Y) N := by
…

Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.Parameter, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.embed, OAI.UniqueGamesTheorem.Appendix.Restriction.compressFrequency

theorem OAI.UniqueGamesTheorem.Appendix.Restriction.real_character_restriction line 262
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.linear_restriction_average line 274
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.linear_restriction_moment_average line 282
Source documentation
The pth-moment form of (A.2). In fact the averaging identity holds for every real exponent, whenever the observable is interpreted by real powers.
```
theorem linear_restriction_moment_average (A : Submodule F2 E) (B : Submodule F2 F)
    (h : (E →ₗ[F2] F) → ℝ) (p : ℝ) :
    (𝔼 T, 𝔼 N, |UniqueGamesTheorem.Fourier.MatrixRestrictions.restrict h A B T N| ^ p) =
      𝔼 T, |h T| ^ p :=
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.restrict
theorem OAI.UniqueGamesTheorem.Appendix.Restriction.linear_coefficient_merging line 291
def OAI.UniqueGamesTheorem.Appendix.Derivatives.spectralProjector line 341
Source documentation
Actual normalized Fourier projector onto the indices satisfying P.
```
def spectralProjector (P : (F →ₗ[F2] E) → Prop) (f : (E →ₗ[F2] F) → ℝ) :
    (E →ₗ[F2] F) → ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.linearCoeff_spectralProjector line 345
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.spectralProjector_energy line 354
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.spectralProjector_energy_le line 364
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.function_eq_of_linearCoeff_eq line 372
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.spectralProjector_comp line 380
def OAI.UniqueGamesTheorem.Appendix.Derivatives.hybridProjector line 390
def OAI.UniqueGamesTheorem.Appendix.Derivatives.hybridDerivative line 394
def OAI.UniqueGamesTheorem.Appendix.Derivatives.rankProjector line 399
def OAI.UniqueGamesTheorem.Appendix.Derivatives.mapDerivative line 403
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.rankProjector_energy line 407
def OAI.UniqueGamesTheorem.Appendix.Derivatives.selectorMultiplicity line 414
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.selector_energy_sum line 418
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.selector_energy_sum_le line 432
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.linearCoeff_mapDerivative line 447
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.mapDerivative_energy_eq_coefficients line 465

theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.mapDerivative_energy_le line 476

Source documentation

A.10 on actual normalized derivative norms.

theorem mapDerivative_energy_le (X : F →ₗ[F2] E)
    [Fintype (X.ker →ₗ[F2] (E ⧸ X.range))]
    (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hdegree : ∀ Y : F →ₗ[F2] E,
      d < Module.finrank F2 Y.range → linearCoeff f Y = 0) :
    (𝔼 N, mapDerivative X f N ^ 2) ≤
      (2 : ℝ) ^ (2 * Module.finrank F2 X.range * (d - Module.finrank F2 X.range)) *
        (𝔼 M, rankProjector X f M ^ 2) := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.Derivatives.mapDerivative, OAI.UniqueGamesTheorem.Appendix.Derivatives.rankProjector

theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.mapDerivative_energy_eq_weighted_energy line 492
Source documentation
The coefficient-energy definition from the weighted estimate is exactly the normalized squared norm of the actual map derivative.
```
theorem mapDerivative_energy_eq_weighted_energy (X : F →ₗ[F2] E)
    (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 N, mapDerivative X f N ^ 2) = WeightedFourthMoment.energy (linearCoeff f) X := by
…
```
Mentions: OAI.UniqueGamesTheorem.Appendix.Derivatives.mapDerivative, OAI.UniqueGamesTheorem.Appendix.WeightedFourthMoment.energy

theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.weighted_fourth_derivative_energy line 503

Source documentation

The corrected weighted fourth-moment estimate for genuine derivative norms, with the normalized primal measure and counting frequency measure.

theorem weighted_fourth_derivative_energy (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hdegree : ∀ Y : F →ₗ[F2] E,
      d < Module.finrank F2 Y.range → linearCoeff f Y = 0) :
    (∑ X : F →ₗ[F2] E, ((2 : ℝ)⁻¹) ^ (8 * d * Module.finrank F2 X.range) *
      (𝔼 N, mapDerivative X f N ^ 2) ^ 2) ≤ 2 * (𝔼 M, f M ^ 2) ^ 2 := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.Derivatives.mapDerivative

theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.spectralProjector_restriction line 518
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.spectralProjector_restriction_moment_average line 543
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.hybridDerivative_energy_average line 558
def OAI.UniqueGamesTheorem.Appendix.Derivatives.HybridIndex line 565
instance OAI.UniqueGamesTheorem.Appendix.Derivatives.hybridIndexFintype line 569
def OAI.UniqueGamesTheorem.Appendix.Derivatives.hybridMomentSum line 578
def OAI.UniqueGamesTheorem.Appendix.Derivatives.hybridSelectorEnergy line 582
theorem OAI.UniqueGamesTheorem.Appendix.Derivatives.hybridMomentSum_le_of_uniform_energy line 587
def OAI.UniqueGamesTheorem.Appendix.A1Reduction.weakFourthSum line 634
theorem OAI.UniqueGamesTheorem.Appendix.A1Reduction.weakFourthSum_nonneg line 642
theorem OAI.UniqueGamesTheorem.Appendix.A1Reduction.linearCoeff_weakProjector line 651

theorem OAI.UniqueGamesTheorem.Appendix.A1Reduction.piece_fourth_moment line 661

Source documentation

Actual Parseval/product identity for each signed weakly selected piece.

theorem piece_fourth_moment (A : Submodule F2 E) (B : Submodule F2 F)
    (f : (E →ₗ[F2] F) → ℝ) :
    (∑ X : F →ₗ[F2] E, BadConvolution.pieceConvolution A B (linearCoeff f) X^2) =
      𝔼 M, spectralProjector (fun Y => A ≤ Y.range ∧ Y.ker ≤ B) f M^4 := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.BadConvolution.pieceConvolution

theorem OAI.UniqueGamesTheorem.Appendix.A1Reduction.actual_bad_cover line 672
theorem OAI.UniqueGamesTheorem.Appendix.A1Reduction.badConvolution_zero_of_degree_zero line 682
theorem OAI.UniqueGamesTheorem.Appendix.A1Reduction.badConvolution_energy_le_weakFourthSum line 699
theorem OAI.UniqueGamesTheorem.Appendix.A1Reduction.fourth_moment_le_two line 713

theorem OAI.UniqueGamesTheorem.Appendix.A1Reduction.degree_reduction line 726

Source documentation

Lemma A.1, Equation (A.6), for every degree d including zero.

theorem degree_reduction (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hdegree : ∀ Y : F →ₗ[F2] E,
      d < Module.finrank F2 Y.range → linearCoeff f Y = 0) :
    (𝔼 M, f M^4) / 162 ≤ (2:ℝ)^(6*d^2) * (𝔼 M, f M^2)^2 + weakFourthSum d f := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.A1Reduction.weakFourthSum

def OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.DegreeAtMost line 764
Source documentation
Fourier support is restricted to maps of rank at most d.
```
def DegreeAtMost (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) : Prop :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.DegreeAtMost.mono line 768
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.degree_rankLevel line 773
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.degree_spectralProjector line 777
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.eq_zero_of_linearCoeff_zero line 784
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.hybridDerivative_coeff_zero_of_lt line 803
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.degree_hybridDerivative line 831
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.hybridDerivative_eq_zero_of_lt_order line 838
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.mapDerivative_coeff_zero_of_lt line 846
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.degree_mapDerivative line 868
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.mapDerivative_eq_zero_of_lt_rank line 874
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.mapDerivative_zero line 881
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.degree_map_hybridDerivative line 888

theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.map_hybridDerivative_eq_zero_of_lt_order_rank line 898

Source documentation

The support cutoff keeps the total order intact even when order A B > d.

theorem map_hybridDerivative_eq_zero_of_lt_order_rank
    (A : Submodule F2 E) (B : Submodule F2 F)
    (X : B →ₗ[F2] (E ⧸ A)) (T : E →ₗ[F2] F) {d : ℕ}
    (f : (E →ₗ[F2] F) → ℝ) (hf : DegreeAtMost d f)
    (h : d < order A B + Module.finrank F2 X.range) :
    mapDerivative X (hybridDerivative A B T f) = 0 := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.DegreeAtMost

theorem OAI.UniqueGamesTheorem.Appendix.DerivativeDegree.map_hybridDerivative_fourth_average_eq_zero_of_lt_order_rank line 911