A1Reduction.lean`

70 declarations, 0 contain sorry, 0 declared as axioms

Exact antecedents of quotient compression

This is the reverse-map count used in Proposition A.5. The compressed map is fixed, together with the two removed subspaces; neither a prescribed rank nor an assumed cardinality is part of the antecedent predicate.

def OAI.MaxCutGames.Appendix.A1Reduction.weakFourthSum line 20
theorem OAI.MaxCutGames.Appendix.A1Reduction.weakFourthSum_nonneg line 28
theorem OAI.MaxCutGames.Appendix.A1Reduction.linearCoeff_weakProjector line 37

theorem OAI.MaxCutGames.Appendix.A1Reduction.piece_fourth_moment line 47

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.MaxCutGames.Appendix.BadConvolution.pieceConvolution

theorem OAI.MaxCutGames.Appendix.A1Reduction.actual_bad_cover line 56
theorem OAI.MaxCutGames.Appendix.A1Reduction.badConvolution_zero_of_degree_zero line 65
theorem OAI.MaxCutGames.Appendix.A1Reduction.badConvolution_energy_le_weakFourthSum line 82
theorem OAI.MaxCutGames.Appendix.A1Reduction.fourth_moment_le_two line 96

theorem OAI.MaxCutGames.Appendix.A1Reduction.degree_reduction line 109

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.MaxCutGames.Appendix.A1Reduction.weakFourthSum

theorem OAI.MaxCutGames.Appendix.A13Reduction.exponent_le line 133
Source documentation
The exponent comparison after retaining the total degree loss.
```
theorem exponent_le (d i j t : ℕ) (hi : i ≤ t) (hj : j ≤ t) (ht : t ≤ d) :
    7 * d * (i + j) + 3 * i * j ≤ 24 * d * t := by
…
```

theorem OAI.MaxCutGames.Appendix.A13Reduction.weighted_moment_le line 144

Source documentation

Degree-forced zero moments allow the same weight bound on every raw triple.

theorem weighted_moment_le (d i j t : ℕ) (e : ℝ)
    (hi : i ≤ t) (hj : j ≤ t) (he : 0 ≤ e) (hz : d < t → e = 0) :
    (2 : ℝ) ^ (7 * d * (i + j) + 3 * i * j) * e ≤
      (2 : ℝ) ^ (24 * d * t) * e := by
…

def OAI.MaxCutGames.Appendix.A13Reduction.tripleMoment line 166
Source documentation
The actual averaged fourth moment attached to a raw derivative triple.
```
def tripleMoment (p : A4Index (K := F2) (W := F) (V := E))
…
```
theorem OAI.MaxCutGames.Appendix.A13Reduction.tripleMoment_nonneg line 171

theorem OAI.MaxCutGames.Appendix.A13Reduction.weak_fourth_le_counted line 180

Source documentation

A.4's native fourth-moment bound with its proved binary index count.

theorem weak_fourth_le_counted (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (A4GeometricIndex A B)] (f : (E →ₗ[F2] F) → ℝ) :
    (𝔼 M, spectralProjector (fun Y => A ≤ Y.range ∧ Y.ker ≤ B) f M ^ 4) ≤
      (2 : ℝ) ^ (3 * Module.finrank F2 A * Module.finrank F2 (F ⧸ B)) *
        ∑ p : A4GeometricIndex A B, tripleMoment p.val f := by
…

Mentions: OAI.MaxCutGames.Appendix.A13Reduction.tripleMoment

theorem OAI.MaxCutGames.Appendix.A13Reduction.weighted_weak_fourth_le_counted line 199

Source documentation

Expand one original weak-pair term, retaining its original dimensions.

theorem weighted_weak_fourth_le_counted (d : ℕ)
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (A4GeometricIndex A B)] (f : (E →ₗ[F2] F) → ℝ) :
    (2 : ℝ) ^ (7 * d * (Module.finrank F2 A + Module.finrank F2 (F ⧸ B))) *
      (𝔼 M, spectralProjector (fun Y => A ≤ Y.range ∧ Y.ker ≤ B) f M ^ 4) ≤
    ∑ p : A4GeometricIndex A B,
      (2 : ℝ) ^ (7 * d * (Module.finrank F2 A + Module.finrank F2 (F ⧸ B)) +
        3 * Module.finrank F2 A * Module.finrank F2 (F ⧸ B)) * tripleMoment p.val f := by
…

Mentions: OAI.MaxCutGames.Appendix.A13Reduction.tripleMoment

theorem OAI.MaxCutGames.Appendix.A13Reduction.tripleMoment_eq_zero_of_lt_size line 214
def OAI.MaxCutGames.Appendix.A13Reduction.tripleTerm line 222
Source documentation
The weight after relabeling the actual raw derivative triple.
```
def tripleTerm (d : ℕ) (p : A13Index.Triple (E := E) (F := F))
…
```
Mentions: OAI.MaxCutGames.Appendix.A13Index.Triple
theorem OAI.MaxCutGames.Appendix.A13Reduction.tripleTerm_nonneg line 227
theorem OAI.MaxCutGames.Appendix.A13Reduction.tripleTerm_eq_zero_of_lt_size line 231
theorem OAI.MaxCutGames.Appendix.A13Reduction.weighted_geometric_moment_le line 238
def OAI.MaxCutGames.Appendix.A13Reduction.positiveTripleSum line 259
Source documentation
The displayed A.13 sum: its original positive total order is retained.
```
def positiveTripleSum (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) : ℝ :=
…
```
def OAI.MaxCutGames.Appendix.A13Reduction.boundedPositiveTripleSum line 263
Source documentation
The same sum after the genuine degree-support cutoff.
```
def boundedPositiveTripleSum (d : ℕ) (f : (E →ₗ[F2] F) → ℝ) : ℝ :=
…
```
theorem OAI.MaxCutGames.Appendix.A13Reduction.weakFourthSum_le_positiveTripleSum line 269
Source documentation
Apply A.4 and its count, then forget the uniquely reconstructible weak pair. The old nonzero condition is carried by positiveMap; no descendant condition is substituted for it.
```
theorem weakFourthSum_le_positiveTripleSum (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hf : DerivativeDegree.DegreeAtMost d f) :
    A1Reduction.weakFourthSum d f ≤ positiveTripleSum d f := by
…
```
Mentions: OAI.MaxCutGames.Appendix.DerivativeDegree.DegreeAtMost, OAI.MaxCutGames.Appendix.A1Reduction.weakFourthSum, OAI.MaxCutGames.Appendix.A13Reduction.positiveTripleSum
theorem OAI.MaxCutGames.Appendix.A13Reduction.positiveTripleSum_eq_bounded line 301
theorem OAI.MaxCutGames.Appendix.A13Reduction.degree_reduction line 323
Source documentation
Equation A.13 with the literal positive-triple sum.
```
theorem degree_reduction (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hf : DerivativeDegree.DegreeAtMost d f) :
    (𝔼 M, f M ^ 4) / 162 ≤
      (2 : ℝ) ^ (6 * d ^ 2) * (𝔼 M, f M ^ 2) ^ 2 + positiveTripleSum d f := by
…
```
Mentions: OAI.MaxCutGames.Appendix.DerivativeDegree.DegreeAtMost, OAI.MaxCutGames.Appendix.A13Reduction.positiveTripleSum
theorem OAI.MaxCutGames.Appendix.A13Reduction.degree_reduction_truncated line 331
Source documentation
Equation A.13 after removing terms whose actual derivative is zero.
```
theorem degree_reduction_truncated (f : (E →ₗ[F2] F) → ℝ) (d : ℕ)
    (hf : DerivativeDegree.DegreeAtMost d f) :
    (𝔼 M, f M ^ 4) / 162 ≤
      (2 : ℝ) ^ (6 * d ^ 2) * (𝔼 M, f M ^ 2) ^ 2 + boundedPositiveTripleSum d f := by
…
```
Mentions: OAI.MaxCutGames.Appendix.DerivativeDegree.DegreeAtMost, OAI.MaxCutGames.Appendix.A13Reduction.boundedPositiveTripleSum
def OAI.MaxCutGames.Appendix.DerivativeInduction.IsAntecedent line 350
Source documentation
The actual complement conditions after choosing domain/codomain splittings.
```
def IsAntecedent (Z : B →ₗ[F2] C) (X : (B × U) →ₗ[F2] (A × C)) : Prop :=
…
```
abbrev OAI.MaxCutGames.Appendix.DerivativeInduction.Antecedent line 355
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.antecedent_image_from_left line 358
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.antecedent_bottom_mem_range line 371
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.antecedent_vertical_zero line 377
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.antecedent_kernel_le_inline_DerivativeInduction line 383
def OAI.MaxCutGames.Appendix.DerivativeInduction.graphParameter line 392
Source documentation
The graph map from the fixed compressed image into the removed summand.
```
noncomputable def graphParameter (Z : B →ₗ[F2] C)
    (X : Antecedent (U := U) (A := A) Z) : Z.range →ₗ[F2] A :=
…
```
Mentions: OAI.MaxCutGames.Appendix.DerivativeInduction.Antecedent
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.graphParameter_apply line 398
def OAI.MaxCutGames.Appendix.DerivativeInduction.complementParameter line 405
Source documentation
Values on the omitted domain complement, compressed into range Z.
```
noncomputable def complementParameter (Z : B →ₗ[F2] C)
    (X : Antecedent (U := U) (A := A) Z) : U →ₗ[F2] Z.range :=
…
```
Mentions: OAI.MaxCutGames.Appendix.DerivativeInduction.Antecedent
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.complementParameter_val line 410

def OAI.MaxCutGames.Appendix.DerivativeInduction.lift line 415

Source documentation

The block matrix [F Z, F H; Z, H].

def lift (Z : B →ₗ[F2] C) (F : Z.range →ₗ[F2] A) (H : U →ₗ[F2] Z.range) :
    (B × U) →ₗ[F2] (A × C) :=
…

theorem OAI.MaxCutGames.Appendix.DerivativeInduction.lift_apply line 420
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.lift_isAntecedent line 425
def OAI.MaxCutGames.Appendix.DerivativeInduction.intoAntecedent line 450
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.graphParameter_lift line 455
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.complementParameter_lift line 463
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.lift_parameters line 469
def OAI.MaxCutGames.Appendix.DerivativeInduction.antecedentEquiv line 489
Source documentation
Exact antecedent bijection; neither direction assumes the desired count.
```
noncomputable def antecedentEquiv (Z : B →ₗ[F2] C) :
    Antecedent (U := U) (A := A) Z ≃
…
```
Mentions: OAI.MaxCutGames.Appendix.DerivativeInduction.Antecedent
def OAI.MaxCutGames.Appendix.DerivativeInduction.graphEmbedding line 499
Source documentation
The graph of the reconstruction parameter as an injective linear map.
```
def graphEmbedding (Z : B →ₗ[F2] C) (F : Z.range →ₗ[F2] A) :
    Z.range →ₗ[F2] (A × C) := F.prod Z.range.subtype
```
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.graphEmbedding_injective line 502
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.range_lift line 507
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.finrank_range_lift line 520
Source documentation
The reconstructed map has exactly the rank of the fixed compression.
```
theorem finrank_range_lift (Z : B →ₗ[F2] C)
    (F : Z.range →ₗ[F2] A) (H : U →ₗ[F2] Z.range) :
    Module.finrank F2 (lift Z F H).range = Module.finrank F2 Z.range := by
…
```
Mentions: OAI.MaxCutGames.Appendix.DerivativeInduction.lift
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.finrank_range_antecedent line 527
Source documentation
The map rank is preserved for every antecedent, without a rank hypothesis.
```
theorem finrank_range_antecedent (Z : B →ₗ[F2] C)
    (X : Antecedent (U := U) (A := A) Z) :
…
```
Mentions: OAI.MaxCutGames.Appendix.DerivativeInduction.Antecedent
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.card_antecedent line 534
Source documentation
The sharp cardinality of the antecedents after the outer subspaces are fixed.
```
theorem card_antecedent (Z : B →ₗ[F2] C)
    [Module.Finite F2 A] [Module.Finite F2 U] [Module.Finite F2 C] :
    Nat.card (Antecedent (U := U) (A := A) Z) =
…
```
Mentions: OAI.MaxCutGames.Appendix.DerivativeInduction.Antecedent
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.isAntecedent_iff_pointwise line 544
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.disjoint_range_iff_zero line 568
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.sup_kernel_iff_image line 578
def OAI.MaxCutGames.Appendix.DerivativeInduction.IsSubspaceAntecedent line 600
Source documentation
Antecedents on arbitrary subspaces. Projection onto the chosen complement is the quotient compression expressed through quotientEquivOfIsCompl.
```
def IsSubspaceAntecedent (P : Submodule F2 W) (Q D : Submodule F2 V)
    (hQ : IsCompl Q D) (Z : P →ₗ[F2] D) (X : W →ₗ[F2] V) : Prop :=
…
```
abbrev OAI.MaxCutGames.Appendix.DerivativeInduction.SubspaceAntecedent line 605
def OAI.MaxCutGames.Appendix.DerivativeInduction.coordinateEquiv line 609
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.coordinateEquiv_apply line 615
theorem OAI.MaxCutGames.Appendix.DerivativeInduction.coordinate_antecedent_iff line 621

def OAI.MaxCutGames.Appendix.DerivativeInduction.subspaceAntecedentEquiv line 668

Source documentation

Transport the canonical antecedent count to arbitrary complementary subspaces.

noncomputable def subspaceAntecedentEquiv (P E : Submodule F2 W)
    (Q D : Submodule F2 V) (hP : IsCompl P E) (hQ : IsCompl Q D)
    (Z : P →ₗ[F2] D) :
    SubspaceAntecedent P Q D hQ Z ≃
      (Z.range →ₗ[F2] Q) × (E →ₗ[F2] Z.range) :=
…

Mentions: OAI.MaxCutGames.Appendix.DerivativeInduction.SubspaceAntecedent

theorem OAI.MaxCutGames.Appendix.DerivativeInduction.card_subspaceAntecedent line 678

Source documentation

Exact antecedent cardinality in arbitrary complementary subspaces.

theorem card_subspaceAntecedent (P E : Submodule F2 W)
    (Q D : Submodule F2 V) (hP : IsCompl P E) (hQ : IsCompl Q D)
    (Z : P →ₗ[F2] D) [Module.Finite F2 W] [Module.Finite F2 V] :
    Nat.card (SubspaceAntecedent P Q D hQ Z) =
      2 ^ (Module.finrank F2 Z.range *
        (Module.finrank F2 Q + Module.finrank F2 E)) := by
…

Mentions: OAI.MaxCutGames.Appendix.DerivativeInduction.SubspaceAntecedent

def OAI.MaxCutGames.Appendix.AntecedentCount.IsAntecedent line 714
Source documentation
Actual quotient-compression antecedents with the complement conditions in the passage from (A.15) to (A.16).
```
def IsAntecedent (P : Submodule F2 W) (Q : Submodule F2 V)
    (Y : P →ₗ[F2] (V ⧸ Q)) (X : W →ₗ[F2] V) : Prop :=
…
```
abbrev OAI.MaxCutGames.Appendix.AntecedentCount.Antecedent line 718
abbrev OAI.MaxCutGames.Appendix.AntecedentCount.Admissible line 724
Source documentation
Maps satisfying the geometric complement conditions, before their compression is fixed.
```
abbrev Admissible (P : Submodule F2 W) (Q : Submodule F2 V) :=
…
```
def OAI.MaxCutGames.Appendix.AntecedentCount.compressionEquiv line 728
Source documentation
Reindex the actual maps by their actual compressed frequency.
```
def compressionEquiv (P : Submodule F2 W) (Q : Submodule F2 V) :
    Admissible P Q ≃ Σ Y : P →ₗ[F2] (V ⧸ Q), Antecedent P Q Y where
…
```
Mentions: OAI.MaxCutGames.Appendix.AntecedentCount.Admissible, OAI.MaxCutGames.Appendix.AntecedentCount.Antecedent
theorem OAI.MaxCutGames.Appendix.AntecedentCount.isAntecedent_iff_subspace line 740
Source documentation
Choosing a codomain complement only changes the coordinates of the fixed compressed output.
```
theorem isAntecedent_iff_subspace (P : Submodule F2 W)
    (Q D : Submodule F2 V) (hQ : IsCompl Q D)
    (Y : P →ₗ[F2] (V ⧸ Q)) (X : W →ₗ[F2] V) :
    IsAntecedent P Q Y X ↔
      DerivativeInduction.IsSubspaceAntecedent P Q D hQ
        ((Q.quotientEquivOfIsCompl D hQ).toLinearMap.comp Y) X := by
…
```
Mentions: OAI.MaxCutGames.Appendix.AntecedentCount.IsAntecedent, OAI.MaxCutGames.Appendix.DerivativeInduction.IsSubspaceAntecedent
def OAI.MaxCutGames.Appendix.AntecedentCount.subspaceEquiv line 760
Source documentation
The quotient antecedents and the graph-coordinate antecedents are the same maps, with equivalent predicates.
```
def subspaceEquiv (P : Submodule F2 W) (Q D : Submodule F2 V)
    (hQ : IsCompl Q D) (Y : P →ₗ[F2] (V ⧸ Q)) :
    Antecedent P Q Y ≃ DerivativeInduction.SubspaceAntecedent P Q D hQ
      ((Q.quotientEquivOfIsCompl D hQ).toLinearMap.comp Y) where
…
```
Mentions: OAI.MaxCutGames.Appendix.AntecedentCount.Antecedent, OAI.MaxCutGames.Appendix.DerivativeInduction.SubspaceAntecedent
theorem OAI.MaxCutGames.Appendix.AntecedentCount.rank_eq line 773
Source documentation
Every admissible antecedent has the rank of its fixed compression.
```
theorem rank_eq (P : Submodule F2 W) (Q : Submodule F2 V)
    (Y : P →ₗ[F2] (V ⧸ Q)) (X : Antecedent P Q Y) :
    Module.finrank F2 X.val.range = Module.finrank F2 Y.range := by
…
```
Mentions: OAI.MaxCutGames.Appendix.AntecedentCount.Antecedent
theorem OAI.MaxCutGames.Appendix.AntecedentCount.card_antecedent line 782
Source documentation
Exact number of antecedents of a fixed quotient compression. The graph and omitted-domain parameters have rank Y * (dim Q + codim P) bits.
```
theorem card_antecedent (P : Submodule F2 W) (Q : Submodule F2 V)
    (Y : P →ₗ[F2] (V ⧸ Q)) :
    Nat.card (Antecedent P Q Y) =
      2 ^ (Module.finrank F2 Y.range *
        (Module.finrank F2 Q + Module.finrank F2 (W ⧸ P))) := by
…
```
Mentions: OAI.MaxCutGames.Appendix.AntecedentCount.Antecedent

theorem OAI.MaxCutGames.Appendix.AntecedentCount.card_antecedent_le line 796

Source documentation

The actual reverse-map multiplicity fits the two graph-parameter budgets used in (A.16). No additional isomorphism factor is needed.

theorem card_antecedent_le (P : Submodule F2 W) (Q : Submodule F2 V)
    (Y : P →ₗ[F2] (V ⧸ Q)) (d k : ℕ)
    (hY : Module.finrank F2 Y.range ≤ k)
    (hQ : Module.finrank F2 Q ≤ d)
    (hP : Module.finrank F2 (W ⧸ P) ≤ d) :
    Nat.card (Antecedent P Q Y) ≤ 2 ^ (2 * d * k) := by
…

Mentions: OAI.MaxCutGames.Appendix.AntecedentCount.Antecedent

theorem OAI.MaxCutGames.Appendix.AntecedentCount.sum_compression line 812

Source documentation

Exact finite-sum reindexing by compressed maps, with the true fiber multiplicity. This holds for signed weights as well as nonnegative energies.

theorem sum_compression [Fintype (W →ₗ[F2] V)]
    (P : Submodule F2 W) (Q : Submodule F2 V)
    [Fintype (P →ₗ[F2] (V ⧸ Q))]
    {R : Type*} [Semiring R] (weight : (P →ₗ[F2] (V ⧸ Q)) → R) :
    (∑ X : Admissible P Q, weight (compress X.val Q P)) =
      ∑ Y : P →ₗ[F2] (V ⧸ Q),
        (2 : R) ^ (Module.finrank F2 Y.range *
          (Module.finrank F2 Q + Module.finrank F2 (W ⧸ P))) * weight Y := by
…

Mentions: OAI.MaxCutGames.Appendix.AntecedentCount.Admissible