Restriction.lean`

65 declarations, 0 contain sorry, 0 declared as axioms

The arbitrary-dimensional linear-algebra cover in Appendix A.1.

def OAI.MaxCutGames.Appendix.Restriction.isum line 10
theorem OAI.MaxCutGames.Appendix.Restriction.isum_congr line 14
theorem OAI.MaxCutGames.Appendix.Restriction.isum_zero line 20
theorem OAI.MaxCutGames.Appendix.Restriction.isum_add line 25
theorem OAI.MaxCutGames.Appendix.Restriction.isum_mul_left line 31
theorem OAI.MaxCutGames.Appendix.Restriction.isum_mul_right line 37
theorem OAI.MaxCutGames.Appendix.Restriction.isum_const line 43
theorem OAI.MaxCutGames.Appendix.Restriction.isum_swap line 52
theorem OAI.MaxCutGames.Appendix.Restriction.isum_map line 58
theorem OAI.MaxCutGames.Appendix.Restriction.isum_perm line 64
def OAI.MaxCutGames.Appendix.Restriction.binarySign line 73
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.MaxCutGames.Appendix.Restriction.binarySign_xor line 75

theorem OAI.MaxCutGames.Appendix.Restriction.binary_character_restriction line 82

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.MaxCutGames.Appendix.Restriction.binarySign

theorem OAI.MaxCutGames.Appendix.Restriction.coefficient_merging line 99

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.MaxCutGames.Appendix.Restriction.isum

theorem OAI.MaxCutGames.Appendix.Restriction.restriction_average line 145
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.MaxCutGames.Appendix.Restriction.isum
theorem OAI.MaxCutGames.Appendix.Restriction.bool_translation_perm line 161
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.MaxCutGames.Appendix.Restriction.bool_restriction_average line 168
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.MaxCutGames.Appendix.Restriction.isum
theorem OAI.MaxCutGames.Appendix.Restriction.bool_character_compatibility line 174
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.MaxCutGames.Appendix.Restriction.binarySign
theorem OAI.MaxCutGames.Appendix.Restriction.bool_character_orthogonality line 179
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.MaxCutGames.Appendix.Restriction.isum, OAI.MaxCutGames.Appendix.Restriction.binarySign
theorem OAI.MaxCutGames.Appendix.Restriction.bool_coefficient_merging line 185
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.MaxCutGames.Appendix.Restriction.isum, OAI.MaxCutGames.Appendix.Restriction.binarySign

theorem OAI.MaxCutGames.Appendix.Restriction.real_translation_average line 207

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.MaxCutGames.Appendix.Restriction.compressFrequency line 223
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.MaxCutGames.Appendix.Restriction.linear_trace_restriction line 229
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 : MaxCutGames.Fourier.MatrixRestrictions.Parameter A B) :
    linearTracePair (MaxCutGames.Fourier.MatrixRestrictions.embed A B N) Y =
      linearTracePair N (compressFrequency A B Y) := by
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.Parameter, OAI.MaxCutGames.Fourier.MatrixRestrictions.embed, OAI.MaxCutGames.Appendix.Restriction.compressFrequency

theorem OAI.MaxCutGames.Appendix.Restriction.linear_character_restriction line 240

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 : MaxCutGames.Fourier.MatrixRestrictions.Parameter A B) :
    linearTraceCharacter Y (T + MaxCutGames.Fourier.MatrixRestrictions.embed A B N) =
      linearTraceCharacter Y T * linearTraceCharacter (compressFrequency A B Y) N := by
…

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

theorem OAI.MaxCutGames.Appendix.Restriction.real_character_restriction line 249
theorem OAI.MaxCutGames.Appendix.Restriction.linear_restriction_average line 262
theorem OAI.MaxCutGames.Appendix.Restriction.linear_restriction_moment_average line 270
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, |MaxCutGames.Fourier.MatrixRestrictions.restrict h A B T N| ^ p) =
      𝔼 T, |h T| ^ p :=
…
```
Mentions: OAI.MaxCutGames.Fourier.MatrixRestrictions.restrict
theorem OAI.MaxCutGames.Appendix.Restriction.linear_coefficient_merging line 279
def OAI.MaxCutGames.Appendix.Level.rankFilter line 316
Source documentation
The unselected multiplier in factored form, after multiplying numerator and denominator by 2^(2*r). Selected characters have multiplier one.
```
def rankFilter (d r : Nat) (selected : Bool) : Rat :=
…
```
theorem OAI.MaxCutGames.Appendix.Level.filter_polynomial_algebra line 320
theorem OAI.MaxCutGames.Appendix.Level.rankFilter_selected line 324
theorem OAI.MaxCutGames.Appendix.Level.rankFilter_zero_at_d line 327
theorem OAI.MaxCutGames.Appendix.Level.rankFilter_zero_at_pred line 331
theorem OAI.MaxCutGames.Appendix.Level.only_two_source_ranks line 337
Source documentation
Only ranks d-1 and d can restrict to rank d-1; no degree bound on the original function is needed.
```
theorem only_two_source_ranks {d r s : Nat} (hd : 1 ≤ d)
    (hlo : s ≤ r) (hhi : r ≤ s + 1) (hs : s + 1 = d) :
    r = d ∨ r = d - 1 := by
…
```

theorem OAI.MaxCutGames.Appendix.Level.rank_filter_character line 344

Source documentation

Selected characters lose exactly one rank. On an unselected character, the two roots of the filter remove every possible unwanted contribution.

theorem rank_filter_character {d r s : Nat} (hd : 1 ≤ d)
    (selected : Bool) (c : Rat)
    (hlo : s ≤ r) (hhi : r ≤ s + 1)
    (hselected : selected = true → r = s + 1) :
    (if selected then if r = d then c else 0 else 0) =
      (if s + 1 = d then rankFilter d r selected * c else 0) := by
…

Mentions: OAI.MaxCutGames.Appendix.Level.rankFilter

def OAI.MaxCutGames.Appendix.Level.mergedCoefficient line 364
Source documentation
A finite merged coefficient. phase can incorporate a translation character and the indicator of one restriction fiber.
```
def mergedCoefficient {α : Type} (indices : List α)
    (phase coefficient : α → Rat) : Rat :=
…
```

theorem OAI.MaxCutGames.Appendix.Level.rank_filter_commutes_with_merge line 370

Source documentation

The character identity survives arbitrary merging, signs, and cancellation. No injectivity of the restriction of frequencies is assumed.

theorem rank_filter_commutes_with_merge {α : Type} (indices : List α)
    (d : Nat) (hd : 1 ≤ d) (rank restrictedRank : α → Nat)
    (selected : α → Bool) (phase coefficient : α → Rat)
    (hlo : ∀ x, restrictedRank x ≤ rank x)
    (hhi : ∀ x, rank x ≤ restrictedRank x + 1)
    (hselected : ∀ x, selected x = true → rank x = restrictedRank x + 1) :
    mergedCoefficient indices phase
        (fun x => if selected x then if rank x = d then coefficient x else 0 else 0) =
      mergedCoefficient indices phase
        (fun x => if restrictedRank x + 1 = d
          then rankFilter d (rank x) (selected x) * coefficient x else 0) := by
…

Mentions: OAI.MaxCutGames.Appendix.Level.mergedCoefficient, OAI.MaxCutGames.Appendix.Level.rankFilter

theorem OAI.MaxCutGames.Appendix.Level.higher_ranks_cannot_contaminate line 389
theorem OAI.MaxCutGames.Appendix.Level.iterated_globality_exponent line 395
Source documentation
Arithmetic in the iterated globality parameter 4^k * 2^(4*k*d - 2*k*(k-1)).
```
theorem iterated_globality_exponent {d k : Nat} (hd : 1 ≤ d) (hk : k ≤ d) :
    2 * k + 4 * k * d - 2 * k * (k - 1) ≤ 10 * d * d := by
…
```
theorem OAI.MaxCutGames.Appendix.Level.successor_le_two_pow line 405
theorem OAI.MaxCutGames.Appendix.Level.selector_multiplicity_bound line 414
Source documentation
A deliberately coarse bound for the number of dimension-indexed selector choices. The geometric subspace count is an explicit hypothesis.
```
theorem selector_multiplicity_bound {d count : Nat} (hd : 1 ≤ d)
    (hcount : count ≤ (d + 1) ^ 2 * 2 ^ (d * d)) :
    count ≤ 2 ^ (3 * d * d) := by
…
```
theorem OAI.MaxCutGames.Appendix.Level.final_exponent_slack line 428
Source documentation
The final fourth-root exponent has the advertised slack.
```
theorem final_exponent_slack (d : Nat) : 113 * d * d ≤ 4 * (30 * d * d) := by
…
```
def OAI.MaxCutGames.Appendix.Level.LinearRank.compress line 443
Source documentation
Restriction in the domain and quotient in the codomain, as actual linear maps. This is the Fourier-frequency map of an affine restriction.
```
def compress (A : Submodule K V) (B : Submodule K W) (Y : W →ₗ[K] V) :
    B →ₗ[K] V ⧸ A := A.mkQ.comp (Y.comp B.subtype)
```
theorem OAI.MaxCutGames.Appendix.Level.LinearRank.finrank_comap_subtype_le line 446
theorem OAI.MaxCutGames.Appendix.Level.LinearRank.quotient_rank_bounds line 452
theorem OAI.MaxCutGames.Appendix.Level.LinearRank.quotient_rank_selected line 463
theorem OAI.MaxCutGames.Appendix.Level.LinearRank.domain_rank_bounds line 474
theorem OAI.MaxCutGames.Appendix.Level.LinearRank.domain_rank_selected line 489
theorem OAI.MaxCutGames.Appendix.Level.LinearRank.hybrid_rank_loss line 501
theorem OAI.MaxCutGames.Appendix.Level.LinearRank.finrank_comap_subtype_eq_iff line 514
Source documentation
Equality in the dimension bound for a subspace intersection forces the original subspace to lie in the restricting subspace.
```
theorem finrank_comap_subtype_eq_iff (A B : Submodule K V) :
    finrank K (A.comap B.subtype) = finrank K A ↔ A ≤ B := by
…
```
theorem OAI.MaxCutGames.Appendix.Level.LinearRank.quotient_rank_equality_iff line 527
theorem OAI.MaxCutGames.Appendix.Level.LinearRank.domain_rank_equality_iff line 541

theorem OAI.MaxCutGames.Appendix.Level.LinearRank.compression_rank_bounds line 555

Source documentation

Every genuine restriction loses at most its order in Fourier rank.

theorem compression_rank_bounds (A : Submodule K V) (B : Submodule K W)
    (Y : W →ₗ[K] V) :
    finrank K (range (compress A B Y)) ≤ finrank K (range Y) ∧
      finrank K (range Y) ≤
        finrank K (range (compress A B Y)) + finrank K A + finrank K (W ⧸ B) := by
…

Mentions: OAI.MaxCutGames.Appendix.Level.LinearRank.compress

theorem OAI.MaxCutGames.Appendix.Level.LinearRank.hybrid_rank_loss_iff line 566

theorem OAI.MaxCutGames.Appendix.Level.LinearRank.line_rank_filter line 591

Source documentation

Instantiation of (A.17)'s rank filter for quotient by an actual line. The only dimension hypothesis is the line's dimension; no rank cutoff is imposed on the original map Y.

theorem line_rank_filter (A : Submodule K V) (Y : W →ₗ[K] V)
    (hline : finrank K A = 1) (d : Nat) (hd : 1 ≤ d) (c : Rat) :
    (if A ≤ range Y then
      if finrank K (range Y) = d then c else 0 else 0) =
      (if finrank K (range (A.mkQ.comp Y)) + 1 = d then
        MaxCutGames.Appendix.Level.rankFilter d (finrank K (range Y))
          (decide (A ≤ range Y)) * c else 0) := by
…

Mentions: OAI.MaxCutGames.Appendix.Level.rankFilter

theorem OAI.MaxCutGames.Appendix.Level.LinearRank.hyperplane_rank_filter line 612

Source documentation

The dual order-one instance: restriction to an actual hyperplane.

theorem hyperplane_rank_filter (B : Submodule K W) (Y : W →ₗ[K] V)
    (hhyperplane : finrank K (W ⧸ B) = 1) (d : Nat) (hd : 1 ≤ d) (c : Rat) :
    (if ker Y ≤ B then
      if finrank K (range Y) = d then c else 0 else 0) =
      (if finrank K (range (Y.comp B.subtype)) + 1 = d then
        MaxCutGames.Appendix.Level.rankFilter d (finrank K (range Y))
          (decide (ker Y ≤ B)) * c else 0) := by
…

Mentions: OAI.MaxCutGames.Appendix.Level.rankFilter

abbrev OAI.MaxCutGames.Appendix.DegreeCover.F2 line 637
theorem OAI.MaxCutGames.Appendix.DegreeCover.binary_add_self line 641
theorem OAI.MaxCutGames.Appendix.DegreeCover.binary_neg line 645

theorem OAI.MaxCutGames.Appendix.DegreeCover.exists_glue_zero line 650

Source documentation

Glue a linear map on P to zero on Q when the restrictions agree.

theorem exists_glue_zero (P Q : Submodule F2 W) (f : W →ₗ[F2] V)
    (cover : P ⊔ Q = ⊤) (compatible : ∀ w ∈ P, w ∈ Q → f w = 0) :
    ∃ g : W →ₗ[F2] V,
      (∀ w ∈ P, g w = f w) ∧ (∀ w ∈ Q, g w = 0) := by
…

Mentions: OAI.MaxCutGames.Appendix.DegreeCover.F2

theorem OAI.MaxCutGames.Appendix.DegreeCover.binary_cross_inline_DegreeCover line 672
theorem OAI.MaxCutGames.Appendix.DegreeCover.exists_cover_component line 680

theorem OAI.MaxCutGames.Appendix.DegreeCover.exists_disjoint_decomposition line 720

Source documentation

A general, dimension-free decomposition with pairwise disjoint images. These are exactly the linear-algebra data used to establish the cover in A.1.

theorem exists_disjoint_decomposition (Y Z : W →ₗ[F2] V)
    (triple : (LinearMap.range (Y + Z) ⊓ LinearMap.range Y) ⊓ LinearMap.range Z = ⊥)
    (cover : LinearMap.ker (Y + Z) ⊔ LinearMap.ker Y ⊔ LinearMap.ker Z = ⊤) :
    ∃ R S C : W →ₗ[F2] V,
      Y + Z = R + S ∧ Y = R + C ∧ Z = S + C ∧
      Disjoint (LinearMap.range R) (LinearMap.range S) ∧
      Disjoint (LinearMap.range R) (LinearMap.range C) ∧
      Disjoint (LinearMap.range S) (LinearMap.range C) ∧
      LinearMap.range R ≤ LinearMap.range (Y + Z) ⊓ LinearMap.range Y ∧
      LinearMap.range S ≤ LinearMap.range (Y + Z) ⊓ LinearMap.range Z ∧
      LinearMap.range C ≤ LinearMap.range Y ⊓ LinearMap.range Z := by
…

Mentions: OAI.MaxCutGames.Appendix.DegreeCover.F2

theorem OAI.MaxCutGames.Appendix.DegreeCover.rank_add_of_disjoint line 783

Source documentation

Rank additivity needs image containment as well as disjointness.

theorem rank_add_of_disjoint [FiniteDimensional F2 V] (R S : W →ₗ[F2] V)
    (hd : Disjoint (LinearMap.range R) (LinearMap.range S))
    (hR : LinearMap.range R ≤ LinearMap.range (R + S))
    (hS : LinearMap.range S ≤ LinearMap.range (R + S)) :
    Module.finrank F2 (LinearMap.range (R + S)) =
      Module.finrank F2 (LinearMap.range R) + Module.finrank F2 (LinearMap.range S) := by
…

Mentions: OAI.MaxCutGames.Appendix.DegreeCover.F2

theorem OAI.MaxCutGames.Appendix.DegreeCover.outside_bad_rank_cover line 798

Source documentation

The cover F(X) \ F₂(X) ⊆ F₁(X), with all three rank-additive decompositions. There is no bound on dimension, and both bad-event exclusions are discharged.

theorem outside_bad_rank_cover [FiniteDimensional F2 V] (Y Z : W →ₗ[F2] V)
    (triple : (LinearMap.range (Y + Z) ⊓ LinearMap.range Y) ⊓ LinearMap.range Z = ⊥)
    (cover : LinearMap.ker (Y + Z) ⊔ LinearMap.ker Y ⊔ LinearMap.ker Z = ⊤) :
    ∃ R S C : W →ₗ[F2] V,
      Y + Z = R + S ∧ Y = R + C ∧ Z = S + C ∧
      Module.finrank F2 (LinearMap.range (Y + Z)) =
        Module.finrank F2 (LinearMap.range R) + Module.finrank F2 (LinearMap.range S) ∧
      Module.finrank F2 (LinearMap.range Y) =
        Module.finrank F2 (LinearMap.range R) + Module.finrank F2 (LinearMap.range C) ∧
      Module.finrank F2 (LinearMap.range Z) =
        Module.finrank F2 (LinearMap.range S) + Module.finrank F2 (LinearMap.range C) := by
…

Mentions: OAI.MaxCutGames.Appendix.DegreeCover.F2