Discriminant.lean`

74 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SidorenkoCounterexample.radicalQuotientForm line 18
Source documentation
The bilinear form induced on the quotient by its radical.
```
def radicalQuotientForm (B : LinearMap.BilinForm K V) (hB : B.IsSymm) :
    LinearMap.BilinForm K (V ⧸ B.ker) :=
…
```
theorem OAI.SidorenkoCounterexample.radicalQuotientForm_mk line 22
theorem OAI.SidorenkoCounterexample.radicalQuotientForm_nondegenerate line 27
Source documentation
Passing to the radical quotient really gives a nondegenerate form.
```
theorem radicalQuotientForm_nondegenerate [FiniteDimensional K V]
    (B : LinearMap.BilinForm K V) (hB : B.IsSymm) :
    (radicalQuotientForm B hB).Nondegenerate := by
…
```
Mentions: OAI.SidorenkoCounterexample.radicalQuotientForm
theorem OAI.SidorenkoCounterexample.radicalQuotientForm_isSymm line 41
theorem OAI.SidorenkoCounterexample.form_isSymm_neg line 50
def OAI.SidorenkoCounterexample.radicalNegEquiv line 57
theorem OAI.SidorenkoCounterexample.radicalQuotientForm_neg line 61
def OAI.SidorenkoCounterexample.discriminantSign line 74
Source documentation
Determinant character of the nondegenerate radical quotient, including rank zero (where the empty determinant is one).
```
noncomputable def discriminantSign (B : LinearMap.BilinForm K V) (hB : B.IsSymm) : ℤ :=
…
```
theorem OAI.SidorenkoCounterexample.discriminantSign_ne_zero line 78
theorem OAI.SidorenkoCounterexample.discriminantSign_sq line 84
theorem OAI.SidorenkoCounterexample.discriminantSign_cases line 90

theorem OAI.SidorenkoCounterexample.determinant_character_basis_independent line 98

Source documentation

The determinant character is independent of a basis.

theorem determinant_character_basis_independent {ι : Type*}
    [Fintype ι] [DecidableEq ι] (b c : Basis ι K V) (B : LinearMap.BilinForm K V) :
    quadraticChar K (B.toMatrix b).det = quadraticChar K (B.toMatrix c).det := by
…

theorem OAI.SidorenkoCounterexample.determinant_character_basis_independent_indices line 109

Source documentation

Basis invariance also allows unrelated finite indexing types.

theorem determinant_character_basis_independent_indices {ι κ : Type*}
    [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
    (b : Basis ι K V) (c : Basis κ K V) (B : LinearMap.BilinForm K V) :
    quadraticChar K (B.toMatrix b).det = quadraticChar K (B.toMatrix c).det := by
…

theorem OAI.SidorenkoCounterexample.discriminantSign_eq line 126
Source documentation
The definition can be evaluated in any basis of the radical quotient.
```
theorem discriminantSign_eq (B : LinearMap.BilinForm K V) (hB : B.IsSymm)
    {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι K (V ⧸ B.ker)) :
    discriminantSign B hB = quadraticChar K ((radicalQuotientForm B hB).toMatrix b).det :=
…
```
Mentions: OAI.SidorenkoCounterexample.discriminantSign, OAI.SidorenkoCounterexample.radicalQuotientForm
theorem OAI.SidorenkoCounterexample.discriminantSign_neg line 132
Source documentation
Negation changes the intrinsic sign by the character of (-1)^rank.
```
theorem discriminantSign_neg (B : LinearMap.BilinForm K V) (hB : B.IsSymm) :
    discriminantSign (-B) (form_isSymm_neg B hB) =
      quadraticChar K ((-1 : K) ^ finrank K (V ⧸ B.ker)) * discriminantSign B hB := by
…
```
Mentions: OAI.SidorenkoCounterexample.discriminantSign, OAI.SidorenkoCounterexample.form_isSymm_neg
theorem OAI.SidorenkoCounterexample.pullback_isSymm line 153
theorem OAI.SidorenkoCounterexample.pullback_ker line 159
def OAI.SidorenkoCounterexample.pullbackQuotientEquiv line 174
theorem OAI.SidorenkoCounterexample.pullbackQuotientEquiv_mk line 180
theorem OAI.SidorenkoCounterexample.pullbackQuotientForm line 184
theorem OAI.SidorenkoCounterexample.discriminantSign_pullback line 200
Source documentation
Pulling a nondegenerate form back along a surjection does not change its intrinsic determinant character. This covers the rank-k matrix representation P*R*Pᵀ used in the signed layer counts.
```
theorem discriminantSign_pullback (B : LinearMap.BilinForm K W)
    (hBs : B.IsSymm) (hB : B.Nondegenerate)
    (f : V →ₗ[K] W) (hf : Function.Surjective f)
    {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι K W) :
    discriminantSign (B.compl₁₂ f f) (pullback_isSymm B hBs f) =
      quadraticChar K (B.toMatrix b).det := by
…
```
Mentions: OAI.SidorenkoCounterexample.discriminantSign, OAI.SidorenkoCounterexample.pullback_isSymm
theorem OAI.SidorenkoCounterexample.matrix_bilin_eval line 219
theorem OAI.SidorenkoCounterexample.matrix_bilin_ker line 230
theorem OAI.SidorenkoCounterexample.matrix_radical_quotient_rank line 238
Source documentation
The rank of the intrinsic quotient is the usual matrix rank.
```
theorem matrix_radical_quotient_rank (M : Matrix n n K) :
    finrank K ((n → K) ⧸ M.toBilin'.ker) = M.rank := by
…
```
theorem OAI.SidorenkoCounterexample.matrix_rank_neg line 248
def OAI.SidorenkoCounterexample.MainClaim line 258
instance OAI.SidorenkoCounterexample.(instance at line 271) line 271
def OAI.SidorenkoCounterexample.matrixSign line 273
theorem OAI.SidorenkoCounterexample.exists_matrix_of_nonsingular line 278
Source documentation
A nonsingular r-form occurs as a rank-r symmetric D-matrix, with its intrinsic sign unchanged.
```
theorem exists_matrix_of_nonsingular {r : ℕ} (hrD : r ≤ D)
    (R : Matrix (Fin r) (Fin r) K) (hRs : R.IsSymm) (hR : R.det ≠ 0) :
    ∃ Z : SymMatrix K D, Z.val.rank = r ∧
      matrixSign K D Z = quadraticChar K R.det := by
…
```
Mentions: OAI.SidorenkoCounterexample.SymMatrix, OAI.SidorenkoCounterexample.matrixSign
theorem OAI.SidorenkoCounterexample.exists_matrix_rank_sign line 310
Source documentation
The two positive-rank layers used in the manuscript are nonempty.
```
theorem exists_matrix_rank_sign {r : ℕ} (hr : 0 < r) (hrD : r ≤ D)
    (hK : ringChar K ≠ 2) {ξ : ℤ} (hξ : ξ = 1 ∨ ξ = -1) :
    ∃ Z : SymMatrix K D, Z.val.rank = r ∧ matrixSign K D Z = ξ := by
…
```
Mentions: OAI.SidorenkoCounterexample.SymMatrix, OAI.SidorenkoCounterexample.matrixSign
def OAI.SidorenkoCounterexample.signedLayer line 331
def OAI.SidorenkoCounterexample.layerMass line 335
def OAI.SidorenkoCounterexample.rankKernel line 338
theorem OAI.SidorenkoCounterexample.matrixSign_neg line 342
theorem OAI.SidorenkoCounterexample.mem_signedLayer line 349
theorem OAI.SidorenkoCounterexample.signedLayer_nonempty line 354
theorem OAI.SidorenkoCounterexample.layerMass_pos line 360
theorem OAI.SidorenkoCounterexample.rankKernel_nonneg line 367
theorem OAI.SidorenkoCounterexample.neg_mem_signedLayer line 373
theorem OAI.SidorenkoCounterexample.signedLayer_card_neg line 390
theorem OAI.SidorenkoCounterexample.rankKernel_neg line 402
def OAI.SidorenkoCounterexample.uniformMean line 415
Source documentation
Expectation under the uniform law on a finite type.
```
noncomputable def uniformMean {A : Type*} [Fintype A] (f : A → ℝ) : ℝ :=
…
```
theorem OAI.SidorenkoCounterexample.uniformMean_rankKernel line 418
abbrev OAI.SidorenkoCounterexample.OddPrime line 433
instance OAI.SidorenkoCounterexample.(instance at line 434) line 434
def OAI.SidorenkoCounterexample.primeInfinity line 436
def OAI.SidorenkoCounterexample.corners line 438
def OAI.SidorenkoCounterexample.modelPointPairs line 441
abbrev OAI.SidorenkoCounterexample.ModelPair line 444
def OAI.SidorenkoCounterexample.layerCorrelation line 446
def OAI.SidorenkoCounterexample.signModelCorrelation line 452
def OAI.SidorenkoCounterexample.RankLayerLimit line 465
theorem OAI.SidorenkoCounterexample.range_sup_complement line 482

theorem OAI.SidorenkoCounterexample.complementary_rank_iff line 491

Source documentation

Equality in the dimension subadditivity for an operator and its complement is equivalent to idempotence.

theorem complementary_rank_iff {K V : Type*} [Field K] [AddCommGroup V]
    [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) :
    finrank K (LinearMap.range f) + finrank K (LinearMap.range (LinearMap.id-f)) =
      finrank K V ↔ IsIdempotentElem f := by
…

theorem OAI.SidorenkoCounterexample.matrix_complementary_rank_iff line 517

Source documentation

Matrix version of complementary_rank_iff.

theorem matrix_complementary_rank_iff {K n : Type*} [Field K] [Fintype n]
    [DecidableEq n] (P : Matrix n n K) :
    P.rank + (1-P).rank = Fintype.card n ↔ P*P=P := by
…

theorem OAI.SidorenkoCounterexample.half_rank_projection line 532
Source documentation
Exact complementary-images equivalence in the main proof. Nonsingularity is determinant ≠ 0; no characteristic or symmetry hypothesis is discarded from an application, since the equivalence holds without those restrictions.
```
theorem half_rank_projection {K n : Type*} [Field K] [Fintype n] [DecidableEq n]
    (r : ℕ) (hdim : Fintype.card n = 2*r) (A B : Matrix n n K)
    (hB : B.det ≠ 0) (hA : A.rank = r) :
    (B-A).rank = r ↔ A*B⁻¹*A=A := by
…
```
def OAI.SidorenkoCounterexample.borderIndex line 569
def OAI.SidorenkoCounterexample.borderRaw line 572
def OAI.SidorenkoCounterexample.symmetricBorder line 576
def OAI.SidorenkoCounterexample.borderUnpack line 587
def OAI.SidorenkoCounterexample.symmetricBorderEquiv line 595
theorem OAI.SidorenkoCounterexample.symmetricBorder_det line 624
theorem OAI.SidorenkoCounterexample.uniformMean_congr line 652
theorem OAI.SidorenkoCounterexample.uniformMean_equiv line 658
theorem OAI.SidorenkoCounterexample.uniformMean_prod line 664
theorem OAI.SidorenkoCounterexample.uniformMean_const line 671
theorem OAI.SidorenkoCounterexample.uniformMean_add line 675
theorem OAI.SidorenkoCounterexample.uniformMean_sub line 679
theorem OAI.SidorenkoCounterexample.uniformMean_mul line 683
theorem OAI.SidorenkoCounterexample.uniformMean_mono line 687
theorem OAI.SidorenkoCounterexample.uniformMean_nonneg line 692
theorem OAI.SidorenkoCounterexample.abs_uniformMean_le line 695
theorem OAI.SidorenkoCounterexample.uniformMean_bound line 701
theorem OAI.SidorenkoCounterexample.uniformMean_indicator line 705