RankAdditivity.lean`

107 declarations, 0 contain sorry, 0 declared as axioms

Rank-additive pairs of linear maps

The rank-additive selector in Appendix A.1 has a concrete geometric meaning: the two image spaces are disjoint and the two kernels span the domain. These lemmas apply over any field and arbitrary finite dimensions, in particular over ZMod 2 with the second map equal to Y + X.

theorem OAI.MaxCutGames.Appendix.RankAdditivity.ker_add_of_disjoint line 24

Source documentation

Disjoint images prevent cancellation between the two map values.

theorem ker_add_of_disjoint (f g : W →ₗ[K] V)
    (h : Disjoint (LinearMap.range f) (LinearMap.range g)) :
    LinearMap.ker (f + g) = LinearMap.ker f ⊓ LinearMap.ker g := by
…

theorem OAI.MaxCutGames.Appendix.RankAdditivity.finrank_add_eq_iff line 47

Source documentation

The exact rank-additivity criterion used to define X ⪯ Y in Appendix A.1.

theorem finrank_add_eq_iff (f g : W →ₗ[K] V) :
    finrank K (LinearMap.range (f + g)) =
        finrank K (LinearMap.range f) + finrank K (LinearMap.range g) ↔
      Disjoint (LinearMap.range f) (LinearMap.range g) ∧
        LinearMap.ker f ⊔ LinearMap.ker g = ⊤ := by
…

theorem OAI.MaxCutGames.Appendix.RankAdditivity.range_left_le_range_add line 76

Source documentation

The left image is contained in the total image for a rank-additive pair.

theorem range_left_le_range_add (f g : W →ₗ[K] V)
    (h : finrank K (LinearMap.range (f + g)) =
      finrank K (LinearMap.range f) + finrank K (LinearMap.range g)) :
    LinearMap.range f ≤ LinearMap.range (f + g) := by
…

theorem OAI.MaxCutGames.Appendix.RankAdditivity.ker_add_le_ker_left line 94

Source documentation

The total kernel is contained in the left kernel for a rank-additive pair.

theorem ker_add_le_ker_left (f g : W →ₗ[K] V)
    (h : finrank K (LinearMap.range (f + g)) =
      finrank K (LinearMap.range f) + finrank K (LinearMap.range g)) :
    LinearMap.ker (f + g) ≤ LinearMap.ker f := by
…

def OAI.MaxCutGames.Appendix.RankAdditivity.RankBelow line 101
theorem OAI.MaxCutGames.Appendix.RankAdditivity.add_remainder line 106
theorem OAI.MaxCutGames.Appendix.RankAdditivity.rankBelow_iff line 110
theorem OAI.MaxCutGames.Appendix.RankAdditivity.range_le_of_rankBelow line 119
theorem OAI.MaxCutGames.Appendix.RankAdditivity.ker_le_of_rankBelow line 128
theorem OAI.MaxCutGames.Appendix.RankAdditivity.range_remainder_eq_range_on_kernel line 137
theorem OAI.MaxCutGames.Appendix.RankAdditivity.mem_ker_of_apply_mem_range_remainder line 161
def OAI.MaxCutGames.Appendix.CompressionCount.base line 189
Source documentation
Canonical rank-dim U map.
```
def base : (U × K) →ₗ[F2] (U × C) :=
…
```
theorem OAI.MaxCutGames.Appendix.CompressionCount.base_apply line 192
def OAI.MaxCutGames.Appendix.CompressionCount.compress line 198
Source documentation
Compress by restricting to the second domain factor and taking the second codomain coordinate.
```
def compress (Y : (U × K) →ₗ[F2] (U × C)) : K →ₗ[F2] C :=
…
```
theorem OAI.MaxCutGames.Appendix.CompressionCount.compress_apply line 201
def OAI.MaxCutGames.Appendix.CompressionCount.Fiber line 206
Source documentation
The actual rank-order compression fiber; subtraction agrees with addition over the binary field.
```
def Fiber (Z : K →ₗ[F2] C) :=
…
```
abbrev OAI.MaxCutGames.Appendix.CompressionCount.Parameters line 211
def OAI.MaxCutGames.Appendix.CompressionCount.graph line 214
def OAI.MaxCutGames.Appendix.CompressionCount.inclusion line 217
def OAI.MaxCutGames.Appendix.CompressionCount.lower line 220
def OAI.MaxCutGames.Appendix.CompressionCount.lift line 224
Source documentation
The block matrix [I+FH,FZ;H,Z].
```
def lift (Z : K →ₗ[F2] C) (P : Parameters (U := U) Z) :
…
```
Mentions: OAI.MaxCutGames.Appendix.CompressionCount.Parameters
theorem OAI.MaxCutGames.Appendix.CompressionCount.lift_apply line 228
theorem OAI.MaxCutGames.Appendix.CompressionCount.compress_lift line 234
theorem OAI.MaxCutGames.Appendix.CompressionCount.graph_injective line 239
theorem OAI.MaxCutGames.Appendix.CompressionCount.inclusion_injective line 244
theorem OAI.MaxCutGames.Appendix.CompressionCount.lower_surjective line 250
theorem OAI.MaxCutGames.Appendix.CompressionCount.range_lift_sub_base line 257
theorem OAI.MaxCutGames.Appendix.CompressionCount.range_lift line 263
theorem OAI.MaxCutGames.Appendix.CompressionCount.finrank_base line 283
theorem OAI.MaxCutGames.Appendix.CompressionCount.lift_rank_order line 289
def OAI.MaxCutGames.Appendix.CompressionCount.toFiber line 296
theorem OAI.MaxCutGames.Appendix.CompressionCount.lift_injective line 300
theorem OAI.MaxCutGames.Appendix.CompressionCount.natCard_linearMap line 314
theorem OAI.MaxCutGames.Appendix.CompressionCount.card_parameters line 328
theorem OAI.MaxCutGames.Appendix.CompressionCount.fiber_geometry line 337
Source documentation
Rank additivity supplies exactly the image/kernel hypotheses used by the block argument.
```
theorem fiber_geometry (Z : K →ₗ[F2] C) (Y : Fiber (U := U) Z) :
…
```
Mentions: OAI.MaxCutGames.Appendix.CompressionCount.Fiber
theorem OAI.MaxCutGames.Appendix.CompressionCount.snd_mem_range line 348
Source documentation
Every lower coordinate of a map in the fiber lies in the compressed image. This is the step that permits taking H : U → range Z.
```
theorem snd_mem_range (Z : K →ₗ[F2] C) (Y : Fiber (U := U) Z) (p : U × K) :
…
```
Mentions: OAI.MaxCutGames.Appendix.CompressionCount.Fiber
def OAI.MaxCutGames.Appendix.CompressionCount.linearSection line 366
Source documentation
Choose a linear section of the map onto its image.
```
noncomputable def linearSection (Z : K →ₗ[F2] C) : Z.range →ₗ[F2] K :=
…
```
theorem OAI.MaxCutGames.Appendix.CompressionCount.section_spec line 371
def OAI.MaxCutGames.Appendix.CompressionCount.extractedF line 376
def OAI.MaxCutGames.Appendix.CompressionCount.extractedH line 381
theorem OAI.MaxCutGames.Appendix.CompressionCount.extracted_lower line 387
theorem OAI.MaxCutGames.Appendix.CompressionCount.difference_ext_snd line 400
Source documentation
On the difference image, the lower coordinate uniquely determines the upper coordinate.
```
theorem difference_ext_snd (Z : K →ₗ[F2] C) (Y : Fiber (U := U) Z)
…
```
Mentions: OAI.MaxCutGames.Appendix.CompressionCount.Fiber
theorem OAI.MaxCutGames.Appendix.CompressionCount.lift_extracted line 416
theorem OAI.MaxCutGames.Appendix.CompressionCount.toFiber_bijective line 440
def OAI.MaxCutGames.Appendix.CompressionCount.fiberEquiv line 450
Source documentation
The exact compression fiber is in bijection with two independent spaces of linear maps. No rank or cardinality claim is an assumption of this equivalence.
```
noncomputable def fiberEquiv (Z : K →ₗ[F2] C) :
    Parameters (U := U) Z ≃ Fiber (U := U) Z :=
…
```
Mentions: OAI.MaxCutGames.Appendix.CompressionCount.Parameters, OAI.MaxCutGames.Appendix.CompressionCount.Fiber
theorem OAI.MaxCutGames.Appendix.CompressionCount.fiber_remainder_rank line 455
theorem OAI.MaxCutGames.Appendix.CompressionCount.fiber_rank line 463
theorem OAI.MaxCutGames.Appendix.CompressionCount.card_fiber line 469
Source documentation
Lemma A.2 in arbitrary finite-dimensional block coordinates.
```
theorem card_fiber (Z : K →ₗ[F2] C) : Nat.card (Fiber (U := U) Z) =
…
```
Mentions: OAI.MaxCutGames.Appendix.CompressionCount.Fiber
theorem OAI.MaxCutGames.Fourier.MatrixSubspaceCount.endomorphism_range_surjective line 493
Source documentation
Taking the image of an endomorphism reaches every actual subspace.
```
theorem endomorphism_range_surjective :
    Function.Surjective (fun f : V →ₗ[K] V => LinearMap.range f) := by
…
```
theorem OAI.MaxCutGames.Fourier.MatrixSubspaceCount.card_subspaces_le_endomorphisms line 499
theorem OAI.MaxCutGames.Fourier.MatrixSubspaceCount.finite_color_space_inline_MatrixSubspaceCount line 509
theorem OAI.MaxCutGames.Fourier.MatrixSubspaceCount.finite_endomorphisms_inline_MatrixSubspaceCount line 513
theorem OAI.MaxCutGames.Fourier.MatrixSubspaceCount.finite_subspaces_inline_MatrixSubspaceCount line 517
theorem OAI.MaxCutGames.Fourier.MatrixSubspaceCount.card_binary_subspaces_le line 521
theorem OAI.MaxCutGames.Fourier.MatrixSubspaceCount.card_binary_subspaces_le_of_finrank_le line 528
theorem OAI.MaxCutGames.Fourier.MatrixSubspaceCount.card_admissible_subspaces_le line 533
theorem OAI.MaxCutGames.Fourier.MatrixSubspaceCount.card_color_admissible_subspaces_le line 541
Source documentation
Counting fixed colors together with actual admissible subspaces gives precisely the q * 2^(s*s) denominator budget from (5.13).
```
theorem card_color_admissible_subspaces_le (P : Submodule F2 C → Prop) :
    Nat.card (C × {S : Submodule F2 C // P S}) ≤
      Nat.card C * 2 ^ (finrank F2 C * finrank F2 C) := by
…
```
theorem OAI.MaxCutGames.Fourier.MatrixSubspaceCount.card_color_admissible_subspaces_le_of_finrank_le line 547
def OAI.MaxCutGames.Fourier.MatrixEnergy.energy line 563
Source documentation
Squared coefficient energy, averaged using the supplied question weights.
```
noncomputable def energy (weight : Q → ℝ) (a : (q : Q) → I q → ℝ) : ℝ :=
…
```

def OAI.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy line 567

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.MaxCutGames.Fourier.MatrixEnergy.spectralEnergy line 573
Source documentation
Diagonal spectral quadratic form.
```
noncomputable def spectralEnergy (weight : Q → ℝ) (eigen a : (q : Q) → I q → ℝ) : ℝ :=
…
```
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.energy_nonneg line 576
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy_nonneg line 581
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy_le_energy line 597
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.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy, OAI.MaxCutGames.Fourier.MatrixEnergy.energy
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.energy_split line 610
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.MaxCutGames.Fourier.MatrixEnergy.energy, OAI.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.spectralEnergy_le_cutoff_add line 626
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.MaxCutGames.Fourier.MatrixEnergy.spectralEnergy, OAI.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy, OAI.MaxCutGames.Fourier.MatrixEnergy.energy

theorem OAI.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy_gt_half line 659

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.MaxCutGames.Fourier.MatrixEnergy.energy, OAI.MaxCutGames.Fourier.MatrixEnergy.spectralEnergy, OAI.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy

theorem OAI.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy_le_twice_difference_add line 674
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.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy, OAI.MaxCutGames.Fourier.MatrixEnergy.energy
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.deleted_energy_gt_eighth line 701
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.boolean_energy_eq_mass line 711
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.MaxCutGames.Fourier.MatrixEnergy.energy

theorem OAI.MaxCutGames.Fourier.MatrixEnergy.weighted_union_bound line 724

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.MaxCutGames.Fourier.MatrixEnergy.exists_fixed_event line 749

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.MaxCutGames.Fourier.MatrixEnergy.exists_fixed_event_scaled line 763

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.MaxCutGames.Fourier.MatrixEnergy.linearRankOn line 788
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.MaxCutGames.Fourier.MatrixEnergy.linearRankOn_top line 793
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.linearRankOn_range line 810
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.MaxCutGames.Fourier.MatrixEnergy.linearRankOn
def OAI.MaxCutGames.Fourier.MatrixEnergy.rankProjection line 829
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.MaxCutGames.Fourier.MatrixEnergy.linearCoeff_sub line 837
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.linearCoeff_rankProjection line 842
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.MaxCutGames.Fourier.MatrixEnergy.rankProjection, OAI.MaxCutGames.Fourier.MatrixEnergy.linearRankOn
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.rankProjection_parseval line 853
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.MaxCutGames.Fourier.MatrixEnergy.rankProjection, OAI.MaxCutGames.Fourier.MatrixEnergy.linearRankOn
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.rankProjection_contraction line 865
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.MaxCutGames.Fourier.MatrixEnergy.rankProjection
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.rankProjection_orthogonal line 878
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.MaxCutGames.Fourier.MatrixEnergy.rankProjection
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.linear_energy_parseval line 888
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.linear_difference_energy_parseval line 893

theorem OAI.MaxCutGames.Fourier.MatrixEnergy.linear_deleted_energy_gt_eighth line 901

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.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy, OAI.MaxCutGames.Fourier.MatrixEnergy.linearRankOn

def OAI.MaxCutGames.Fourier.MatrixEnergy.colorIndicator line 916
Source documentation
Color indicator of one actual labeling.
```
noncomputable def colorIndicator {X Y : Type*} (label : X → Y) (y : Y) : X → ℝ := by
…
```
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.colorIndicator_partition line 920
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.colorIndicator_parseval line 927
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.MaxCutGames.Fourier.MatrixEnergy.colorIndicator
def OAI.MaxCutGames.Fourier.MatrixEnergy.labelingCoeff line 937
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.MaxCutGames.Fourier.MatrixEnergy.labelingCoeff_energy_one line 941

theorem OAI.MaxCutGames.Fourier.MatrixEnergy.labeling_lowRank_energy line 957

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.MaxCutGames.Fourier.MatrixEnergy.linearRankOn, OAI.MaxCutGames.Fourier.MatrixEnergy.spectralEnergy, OAI.MaxCutGames.Fourier.MatrixEnergy.labelingCoeff, OAI.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy

theorem OAI.MaxCutGames.Fourier.MatrixEnergy.dependent_linear_energy_parseval line 987
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.dependent_remainder_cutoff_le_eighth line 998

theorem OAI.MaxCutGames.Fourier.MatrixEnergy.dependent_deleted_energy_from_level line 1028

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.MaxCutGames.Fourier.MatrixEnergy.cutoffEnergy, OAI.MaxCutGames.Fourier.MatrixEnergy.linearRankOn

def OAI.MaxCutGames.Fourier.MatrixEnergy.boolReal line 1049
Source documentation
Real value of a Boolean indicator.
```
def boolReal (b : Bool) : ℝ := if b then 1 else 0
```
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.boolReal_sq line 1051
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.boolReal_le_one line 1054
def OAI.MaxCutGames.Fourier.MatrixEnergy.labelBool line 1058
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.MaxCutGames.Fourier.MatrixEnergy.labelBool_real line 1062
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.removed_boolReal line 1069
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.MaxCutGames.Fourier.Deletion.RestrictionSystem, OAI.MaxCutGames.Fourier.MatrixEnergy.boolReal, OAI.MaxCutGames.Fourier.Deletion.removed, OAI.MaxCutGames.Fourier.Deletion.remainder
theorem OAI.MaxCutGames.Fourier.MatrixEnergy.removed_difference_sq line 1078
def OAI.MaxCutGames.Fourier.MatrixEnergy.questionEventMass line 1091
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.MaxCutGames.Fourier.MatrixEnergy.dependent_removed_union_bound line 1096

theorem OAI.MaxCutGames.Fourier.MatrixEnergy.fixed_target_of_removed_mass line 1133

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.MaxCutGames.Fourier.MatrixEnergy.questionEventMass

theorem OAI.MaxCutGames.Fourier.MatrixEnergy.boolean_subpartition_energy_le_one line 1151

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.MaxCutGames.Fourier.MatrixEnergy.boolReal

theorem OAI.MaxCutGames.Fourier.MatrixEnergy.remainder_subpartition_energy_le_one line 1181
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.MaxCutGames.Fourier.Deletion.RestrictionSystem, OAI.MaxCutGames.Fourier.MatrixEnergy.boolReal, OAI.MaxCutGames.Fourier.Deletion.remainder, OAI.MaxCutGames.Fourier.MatrixEnergy.labelBool

theorem OAI.MaxCutGames.Fourier.MatrixEnergy.fixed_badRow_target_of_removed_mass line 1205

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.MaxCutGames.Fourier.MatrixEnergy.boolReal, OAI.MaxCutGames.Fourier.Deletion.removed, OAI.MaxCutGames.Fourier.MatrixRestrictions.system, OAI.MaxCutGames.Fourier.MatrixEnergy.questionEventMass, OAI.MaxCutGames.Fourier.Deletion.BadRow