MatrixEnergy.lean`

49 declarations, 0 contain sorry, 0 declared as axioms

def OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.energy line 21
Source documentation
Squared coefficient energy, averaged using the supplied question weights.
```
noncomputable def energy (weight : Q → ℝ) (a : (q : Q) → I q → ℝ) : ℝ :=
…
```
def OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy line 25
Source documentation
Squared energy retained by a coordinate projection.
```
noncomputable def cutoffEnergy (weight : Q → ℝ) (keep : (q : Q) → I q → Prop)
    (a : (q : Q) → I q → ℝ) : ℝ := by
…
```
def OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.spectralEnergy line 31
Source documentation
Diagonal spectral quadratic form.
```
noncomputable def spectralEnergy (weight : Q → ℝ) (eigen a : (q : Q) → I q → ℝ) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.energy_nonneg line 34
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy_nonneg line 39
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy_le_energy line 55
Source documentation
The projection onto any set of coefficient indices is a contraction in the weighted squared norm.
```
theorem cutoffEnergy_le_energy (weight : Q → ℝ) (keep : (q : Q) → I q → Prop)
    (a : (q : Q) → I q → ℝ) (hw : ∀ q, 0 ≤ weight q) :
    cutoffEnergy weight keep a ≤ energy weight a := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.energy
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.energy_split line 68
Source documentation
Retained and discarded coefficient coordinates are orthogonal: their energies add exactly to the original energy.
```
theorem energy_split (weight : Q → ℝ) (keep : (q : Q) → I q → Prop) (a : (q : Q) → I q → ℝ) :
    energy weight a = cutoffEnergy weight keep a +
      cutoffEnergy weight (fun q i => ¬ keep q i) a := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.energy, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.spectralEnergy_le_cutoff_add line 84
Source documentation
A spectral multiplier bounded by one on retained indices and by η elsewhere contributes at most retained energy plus η times total energy.
```
theorem spectralEnergy_le_cutoff_add
    (weight : Q → ℝ) (keep : (q : Q) → I q → Prop) (eigen a : (q : Q) → I q → ℝ) (η : ℝ)
    (hw : ∀ q, 0 ≤ weight q) (hη : 0 ≤ η)
    (hone : ∀ q i, eigen q i ≤ 1)
    (hhigh : ∀ q i, ¬ keep q i → eigen q i ≤ η) :
    spectralEnergy weight eigen a ≤ cutoffEnergy weight keep a + η * energy weight a := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.spectralEnergy, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.energy

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy_gt_half line 117

Source documentation

Unit total energy and spectral value above δ force retained energy above δ/2 when all discarded multipliers are at most δ/2.

theorem cutoffEnergy_gt_half
    (weight : Q → ℝ) (keep : (q : Q) → I q → Prop) (eigen a : (q : Q) → I q → ℝ) (δ : ℝ)
    (hw : ∀ q, 0 ≤ weight q) (hδ : 0 ≤ δ)
    (hone : ∀ q i, eigen q i ≤ 1)
    (hhigh : ∀ q i, ¬ keep q i → eigen q i ≤ δ / 2)
    (htotal : energy weight a = 1) (hvalue : δ < spectralEnergy weight eigen a) :
    δ / 2 < cutoffEnergy weight keep a := by
…

Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.energy, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.spectralEnergy, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy_le_twice_difference_add line 132
Source documentation
The elementary square bound, summed over the retained coefficients. The discarded term on the right uses the full coefficient difference, giving the contraction needed for equation (5.11) without introducing square roots.
```
theorem cutoffEnergy_le_twice_difference_add
    (weight : Q → ℝ) (keep : (q : Q) → I q → Prop) (H G : (q : Q) → I q → ℝ)
    (hw : ∀ q, 0 ≤ weight q) :
    cutoffEnergy weight keep H ≤
      2 * energy weight (fun q i => H q i - G q i) + 2 * cutoffEnergy weight keep G := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.energy
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.deleted_energy_gt_eighth line 159
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.boolean_energy_eq_mass line 169
Source documentation
Squared Boolean functions equal their values under a finite weighted sum.
```
theorem boolean_energy_eq_mass (weight : Q → ℝ) (H : (q : Q) → I q → ℝ)
    (hbool : ∀ q i, H q i = 0 ∨ H q i = 1) :
    energy weight H = ∑ q, weight q * ∑ i, H q i := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.energy

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.weighted_union_bound line 182

Source documentation

A finite union bound for fractional removed mass dominated by indicator events. Both the event choice and the removed value may depend on the outcome.

theorem weighted_union_bound {Ω J : Type*} [Fintype Ω] [Fintype J]
    (weight value : Ω → ℝ) (event : J → Ω → Prop)
    [∀ j, DecidablePred (event j)]
    (hw : ∀ ω, 0 ≤ weight ω) (hvalue : ∀ ω, value ω ≤ 1)
    (hcover : ∀ ω, 0 < value ω → ∃ j, event j ω) :
    (∑ ω, weight ω * value ω) ≤
      ∑ j, ∑ ω, weight ω * (if event j ω then (1 : ℝ) else 0) := by
…

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.exists_fixed_event line 207

Source documentation

Finite real pigeonhole principle for the one fixed color/subspace choice.

theorem exists_fixed_event {J : Type*} [Fintype J] (mass : J → ℝ)
    (threshold budget : ℝ)
    (hcount : (Fintype.card J : ℝ) * threshold ≤ budget)
    (hmass : budget < ∑ j, mass j) : ∃ j, threshold < mass j := by
…

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.exists_fixed_event_scaled line 221

Source documentation

The explicit denominator in (5.13), for any supplied event-count bound.

theorem exists_fixed_event_scaled {J : Type*} [Fintype J]
    (mass : J → ℝ) (N : ℕ) (δ : ℝ)
    (hN : 0 < N) (hδ : 0 ≤ δ) (hcard : Fintype.card J ≤ N)
    (hmass : δ / 8 < ∑ j, mass j) :
    ∃ j, δ / (8 * (N : ℝ)) < mass j := by
…

def OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linearRankOn line 246
Source documentation
The actual rank of a Fourier index restricted to the alphabet subspace.
```
noncomputable def linearRankOn (C : Submodule F2 F) (S : F →ₗ[F2] E) : ℕ :=
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linearRankOn_top line 251
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linearRankOn_range line 268
Source documentation
Restricting to the image of a symbol embedding has the same image rank as composition with that embedding, even when it is not injective.
```
theorem linearRankOn_range {V : Type*} [AddCommGroup V] [Module F2 V]
    (S : F →ₗ[F2] E) (ι : V →ₗ[F2] F) :
    linearRankOn (LinearMap.range ι) S =
      Module.finrank F2 (LinearMap.range (S.comp ι)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linearRankOn
def OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.rankProjection line 287
Source documentation
Projection onto trace characters whose index has bounded rank on C.
```
noncomputable def rankProjection (C : Submodule F2 F) (r : ℕ)
    (f : (E →ₗ[F2] F) → ℝ) : (E →ₗ[F2] F) → ℝ := by
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linearCoeff_sub line 295
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linearCoeff_rankProjection line 300
Source documentation
The genuine function-space projection acts by the claimed coefficient mask.
```
theorem linearCoeff_rankProjection (C : Submodule F2 F) (r : ℕ)
    (f : (E →ₗ[F2] F) → ℝ) (S : F →ₗ[F2] E) :
    linearCoeff (rankProjection C r f) S =
      if linearRankOn C S ≤ r then linearCoeff f S else 0 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.rankProjection, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linearRankOn
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.rankProjection_parseval line 311
Source documentation
Squared norm of the actual projection equals the retained coefficient mass.
```
theorem rankProjection_parseval (C : Submodule F2 F) (r : ℕ)
    (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, rankProjection C r f X ^ 2) =
      ∑ S : F →ₗ[F2] E, if linearRankOn C S ≤ r then linearCoeff f S ^ 2 else 0 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.rankProjection, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linearRankOn
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.rankProjection_contraction line 323
Source documentation
Contraction for the actual rank projection with the uniform function norm.
```
theorem rankProjection_contraction (C : Submodule F2 F) (r : ℕ)
    (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, rankProjection C r f X ^ 2) ≤ 𝔼 X, f X ^ 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.rankProjection
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.rankProjection_orthogonal line 336
Source documentation
The projected part is orthogonal to the discarded part in the actual uniform function inner product.
```
theorem rankProjection_orthogonal (C : Submodule F2 F) (r : ℕ)
    (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 X, rankProjection C r f X * (f X - rankProjection C r f X)) = 0 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.rankProjection
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linear_energy_parseval line 346
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linear_difference_energy_parseval line 351

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linear_deleted_energy_gt_eighth line 359

Source documentation

Equation (5.11) now for actual functions on a binary linear-map space, using the actual restriction rank and trace Fourier coefficients.

theorem linear_deleted_energy_gt_eighth
    (weight : Q → ℝ) (C : Submodule F2 F) (r : ℕ)
    (H G : Q → (E →ₗ[F2] F) → ℝ) (δ : ℝ)
    (hw : ∀ q, 0 ≤ weight q)
    (hlarge : δ / 2 < cutoffEnergy weight (fun _ S => linearRankOn C S ≤ r)
      (fun q S => linearCoeff (H q) S))
    (hsmall : cutoffEnergy weight (fun _ S => linearRankOn C S ≤ r)
      (fun q S => linearCoeff (G q) S) ≤ δ / 8) :
    δ / 8 < ∑ q, weight q * (𝔼 X, (H q X - G q X) ^ 2) := by
…

Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linearRankOn

def OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.colorIndicator line 374
Source documentation
Color indicator of one actual labeling.
```
noncomputable def colorIndicator {X Y : Type*} (label : X → Y) (y : Y) : X → ℝ := by
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.colorIndicator_partition line 378
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.colorIndicator_parseval line 385
Source documentation
Parseval for all color indicators sums to exactly one, with the correct uniform primal normalization and counting measure on Fourier indices.
```
theorem colorIndicator_parseval {Y : Type*} [Fintype Y]
    (label : (E →ₗ[F2] F) → Y) :
    (∑ y, ∑ S : F →ₗ[F2] E, linearCoeff (colorIndicator label y) S ^ 2) = 1 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.colorIndicator
def OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.labelingCoeff line 395
Source documentation
Fourier coefficient array for a family of labelings, including color as part of the component index.
```
noncomputable def labelingCoeff {Y : Type*}
    (label : Q → (E →ₗ[F2] F) → Y) (qy : Q × Y) (S : F →ₗ[F2] E) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.labelingCoeff_energy_one line 399

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.labeling_lowRank_energy line 415

Source documentation

The low-rank Fourier-energy conclusion (5.5), for genuine binary linear maps and genuine labeling coefficients. The spectral premise can be obtained from the noise diagonalization; the bound is on actual restriction rank.

theorem labeling_lowRank_energy {Y : Type*} [Fintype Y]
    (weight : Q → ℝ) (label : Q → (E →ₗ[F2] F) → Y)
    (C : Submodule F2 F) (r : ℕ) (eigen : Q → (F →ₗ[F2] E) → ℝ) (δ : ℝ)
    (hw : ∀ q, 0 ≤ weight q) (hnorm : ∑ q, weight q = 1) (hδ : 0 ≤ δ)
    (hone : ∀ q S, eigen q S ≤ 1)
    (hhigh : ∀ q S, r < linearRankOn C S → eigen q S ≤ δ / 2)
    (hvalue : δ < spectralEnergy (fun qy : Q × Y => weight qy.1)
      (fun qy S => eigen qy.1 S) (labelingCoeff label)) :
    δ / 2 < cutoffEnergy (fun qy : Q × Y => weight qy.1)
      (fun _ S => linearRankOn C S ≤ r) (labelingCoeff label) := by
…

Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linearRankOn, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.spectralEnergy, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.labelingCoeff, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.dependent_linear_energy_parseval line 445
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.dependent_remainder_cutoff_le_eighth line 456

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.dependent_deleted_energy_from_level line 486

Source documentation

The actual removed probability energy in Section 5.3, allowing the map domain to depend on the complete question and color index.

theorem dependent_deleted_energy_from_level
    (weight : J → ℝ) (C : Submodule F2 F) (r : ℕ)
    (H G : (j : J) → (E j →ₗ[F2] F) → ℝ) (κ δ : ℝ)
    (hw : ∀ j, 0 ≤ weight j) (hκ : 0 ≤ κ) (hκδ : κ ≤ δ / 8)
    (hlarge : δ / 2 < cutoffEnergy weight (fun _ S => linearRankOn C S ≤ r)
      (fun j S => linearCoeff (H j) S))
    (hlevel : ∀ j, (∑ S : F →ₗ[F2] E j,
      if linearRankOn C S ≤ r then linearCoeff (G j) S ^ 2 else 0) ≤
        κ * (𝔼 X, G j X ^ 2))
    (hmass : (∑ j, weight j * (𝔼 X, G j X ^ 2)) ≤ 1) :
    δ / 8 < ∑ j, weight j * (𝔼 X, (H j X - G j X) ^ 2) := by
…

Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.cutoffEnergy, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.linearRankOn

def OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.boolReal line 507
Source documentation
Real value of a Boolean indicator.
```
def boolReal (b : Bool) : ℝ := if b then 1 else 0
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.boolReal_sq line 509
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.boolReal_le_one line 512
def OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.labelBool line 516
Source documentation
Boolean indicator of one color of a labeling.
```
noncomputable def labelBool {X Y : Type*} (label : X → Y) (y : Y) : X → Bool := by
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.labelBool_real line 520
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.removed_boolReal line 527
Source documentation
Deletion's actual Boolean removed function is exactly the difference of the original and remainder indicators.
```
theorem removed_boolReal {X Row Witness : Type*}
    (S : Deletion.RestrictionSystem X Row Witness) (H : X → Bool) (p d : ℕ) (x : X) :
    boolReal (Deletion.removed S H p d x) =
      boolReal (H x) - boolReal (Deletion.remainder S H p d x) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.boolReal, OAI.UniqueGamesTheorem.Fourier.Deletion.removed, OAI.UniqueGamesTheorem.Fourier.Deletion.remainder
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.removed_difference_sq line 536
def OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.questionEventMass line 549
Source documentation
An event probability: first sample the question with the supplied weights, then sample uniformly in its own finite space.
```
noncomputable def questionEventMass
    (weight : Q → ℝ) (B : (q : Q) → Ω q → Prop) : ℝ := by
…
```
theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.dependent_removed_union_bound line 554

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.fixed_target_of_removed_mass line 591

Source documentation

One target is fixed before sampling the question and its map.

theorem fixed_target_of_removed_mass
    (weight : Q → ℝ) (d : (q : Q) → Y → Ω q → ℝ)
    (B : (q : Q) → Y → A → Ω q → Prop)
    (hw : ∀ q, 0 ≤ weight q) (hd : ∀ q y X, d q y X ≤ 1)
    (hc : ∀ q y X, 0 < d q y X → ∃ a, B q y a X)
    (δ : ℝ) (N : ℕ) (hδ : 0 ≤ δ) (hN : 0 < N)
    (hcount : Fintype.card (Y × A) ≤ N)
    (hremoved : δ / 8 < ∑ q, weight q * ∑ y, 𝔼 X, d q y X) :
    ∃ y a, δ / (8 * (N : ℝ)) <
      questionEventMass weight (fun q X => B q y a X) := by
…

Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.questionEventMass

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.boolean_subpartition_energy_le_one line 609

Source documentation

A Boolean subpartition has total squared mass at most one. Colors are summed with counting measure, not averaged.

theorem boolean_subpartition_energy_le_one [∀ q, Nonempty (Ω q)]
    (weight : Q → ℝ) (label : (q : Q) → Ω q → Y)
    (G : (q : Q) → Y → Ω q → Bool)
    (hw : ∀ q, 0 ≤ weight q) (hnorm : ∑ q, weight q = 1)
    (hG : ∀ q y X, G q y X = true → label q X = y) :
    (∑ q, weight q * ∑ y, 𝔼 X, boolReal (G q y X) ^ 2) ≤ 1 := by
…

Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.boolReal

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.remainder_subpartition_energy_le_one line 639
Source documentation
The actual whole-row remainder of labeling indicators satisfies the mass bound needed in the deleted-energy argument, with no remaining mass hypothesis.
```
theorem remainder_subpartition_energy_le_one [∀ q, Nonempty (Ω q)]
    {Row Witness : Q → Type*}
    (S : (q : Q) → Deletion.RestrictionSystem (Ω q) (Row q) (Witness q))
    (weight : Q → ℝ) (label : (q : Q) → Ω q → Y) (p d : ℕ)
    (hw : ∀ q, 0 ≤ weight q) (hnorm : ∑ q, weight q = 1) :
    (∑ q, weight q * ∑ y, 𝔼 X,
      boolReal (Deletion.remainder (S q) (labelBool (label q) y) p d X) ^ 2) ≤ 1 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Fourier.Deletion.RestrictionSystem, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.boolReal, OAI.UniqueGamesTheorem.Fourier.Deletion.remainder, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.labelBool

theorem OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.fixed_badRow_target_of_removed_mass line 665

Source documentation

Equation (5.13) for the actual whole-row deletion system. Only the color and target subspace are selected. Neither the question, row value, nor witness vanishing subspace is part of the counted target.

theorem fixed_badRow_target_of_removed_mass
    (weight : Q → ℝ) (H : (q : Q) → C → (E q →ₗ[F2] C) → Bool)
    (r p d : ℕ) (δ : ℝ)
    (hw : ∀ q, 0 ≤ weight q) (hδ : 0 ≤ δ)
    (hremoved : δ / 8 < ∑ q, weight q * ∑ y, 𝔼 X,
      boolReal (Deletion.removed (MatrixRestrictions.system r) (H q y) p d X)) :
    ∃ (y : C) (C' : Submodule F2 C), Module.finrank F2 (C ⧸ C') ≤ r ∧
      δ / (8 * (Nat.card C : ℝ) * (2 : ℝ) ^
        (Module.finrank F2 C * Module.finrank F2 C)) <
      questionEventMass weight (fun q (X : E q →ₗ[F2] C) =>
        Deletion.BadRow (MatrixRestrictions.system r) (H q y) p d
          ⟨C', C'.mkQ.comp X⟩) := by
…

Mentions: OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.boolReal, OAI.UniqueGamesTheorem.Fourier.Deletion.removed, OAI.UniqueGamesTheorem.Fourier.MatrixRestrictions.system, OAI.UniqueGamesTheorem.Fourier.MatrixEnergy.questionEventMass, OAI.UniqueGamesTheorem.Fourier.Deletion.BadRow