DerivativeInduction.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

def OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.IsAntecedent line 21
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.UniqueGamesTheorem.Appendix.DerivativeInduction.Antecedent line 26
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.antecedent_image_from_left line 29
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.antecedent_bottom_mem_range line 42
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.antecedent_vertical_zero line 48
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.antecedent_kernel_le line 54
def OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.graphParameter line 63
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.UniqueGamesTheorem.Appendix.DerivativeInduction.Antecedent
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.graphParameter_apply line 69
def OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.complementParameter line 76
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.UniqueGamesTheorem.Appendix.DerivativeInduction.Antecedent
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.complementParameter_val line 81

def OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.lift line 86

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.UniqueGamesTheorem.Appendix.DerivativeInduction.lift_apply line 91
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.lift_isAntecedent line 96
def OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.intoAntecedent line 121
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.graphParameter_lift line 126
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.complementParameter_lift line 134
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.lift_parameters line 140
def OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.antecedentEquiv line 160
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.UniqueGamesTheorem.Appendix.DerivativeInduction.Antecedent
def OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.graphEmbedding line 170
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.UniqueGamesTheorem.Appendix.DerivativeInduction.graphEmbedding_injective line 173
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.range_lift line 178
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.finrank_range_lift line 191
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.UniqueGamesTheorem.Appendix.DerivativeInduction.lift
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.finrank_range_antecedent line 198
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.UniqueGamesTheorem.Appendix.DerivativeInduction.Antecedent
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.card_antecedent line 205
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.UniqueGamesTheorem.Appendix.DerivativeInduction.Antecedent
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.isAntecedent_iff_pointwise line 215
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.disjoint_range_iff_zero line 241
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.sup_kernel_iff_image line 251
def OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.IsSubspaceAntecedent line 273
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.UniqueGamesTheorem.Appendix.DerivativeInduction.SubspaceAntecedent line 278
def OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.coordinateEquiv line 282
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.coordinateEquiv_apply line 288
theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.coordinate_antecedent_iff line 294
def OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.subspaceAntecedentEquiv line 341
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.UniqueGamesTheorem.Appendix.DerivativeInduction.SubspaceAntecedent

theorem OAI.UniqueGamesTheorem.Appendix.DerivativeInduction.card_subspaceAntecedent line 351

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.UniqueGamesTheorem.Appendix.DerivativeInduction.SubspaceAntecedent