AlternatingProducts.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Alternating products over literal finite subsets

The exponent is (-1)^card S. Pairing subsets along p follows from the powerset decomposition, with the quotient orientation x S / x (insert p S).

The definition and pairing are valid in a division commutative monoid, so they apply both to actual field values and to units. Cancellation of a constant family is stated in a commutative group. No local comparison, nonvanishing, integrality, or torsion statement is assumed or inferred.

def OAI.CirculantHadamard.subsetSign line 29
theorem OAI.CirculantHadamard.subsetSign_empty line 31
theorem OAI.CirculantHadamard.subsetSign_of_even line 34
theorem OAI.CirculantHadamard.subsetSign_of_odd line 37
theorem OAI.CirculantHadamard.subsetSign_insert line 40
theorem OAI.CirculantHadamard.sum_subsetSign_eq_zero line 45
Source documentation
The signed subset count vanishes by pairing along an actual element of t.
```
theorem sum_subsetSign_eq_zero (t : Finset I) (ht : t.Nonempty) :
    ∑ S ∈ t.powerset, subsetSign S = 0 := by
…
```
Mentions: OAI.CirculantHadamard.subsetSign

theorem OAI.CirculantHadamard.card_even_subsets_eq_card_odd_subsets line 66

Source documentation

The even-cardinality and odd-cardinality subset filters have equal size.

theorem card_even_subsets_eq_card_odd_subsets (t : Finset I) (ht : t.Nonempty) :
    (t.powerset.filter (fun S => Even S.card)).card =
      (t.powerset.filter (fun S => Odd S.card)).card := by
…

def OAI.CirculantHadamard.evenSubsetProduct line 97
Source documentation
Numerator before introducing any inverse, available in a coefficient ring.
```
def evenSubsetProduct {G : Type uG} [CommMonoid G] (t : Finset I)
    (x : Finset I → G) : G :=
…
```
def OAI.CirculantHadamard.oddSubsetProduct line 102
Source documentation
Denominator before introducing any inverse, available in a coefficient ring.
```
def oddSubsetProduct {G : Type uG} [CommMonoid G] (t : Finset I)
    (x : Finset I → G) : G :=
…
```
theorem OAI.CirculantHadamard.map_evenSubsetProduct line 106
theorem OAI.CirculantHadamard.map_oddSubsetProduct line 111
def OAI.CirculantHadamard.alternatingProduct line 121
Source documentation
The alternating product of the actual family indexed by subsets of t.
```
def alternatingProduct (t : Finset I) (x : Finset I → G) : G :=
…
```
theorem OAI.CirculantHadamard.alternatingProduct_empty line 124
theorem OAI.CirculantHadamard.alternatingProduct_one line 128
theorem OAI.CirculantHadamard.alternatingProduct_congr line 132
theorem OAI.CirculantHadamard.alternatingProduct_mul line 139
theorem OAI.CirculantHadamard.alternatingProduct_inv line 144
theorem OAI.CirculantHadamard.alternatingProduct_div line 148
theorem OAI.CirculantHadamard.alternatingProduct_insert line 155
Source documentation
A single direction pairs each omitted-p subset with its insertion. The exponent at the inserted subset is the negative of the original one.
```
theorem alternatingProduct_insert [DecidableEq I] (t : Finset I)
    (x : Finset I → G) (p : I) (hp : p ∉ t) :
    alternatingProduct (insert p t) x =
      ∏ S ∈ t.powerset, (x S / x (insert p S)) ^ subsetSign S := by
…
```
Mentions: OAI.CirculantHadamard.alternatingProduct, OAI.CirculantHadamard.subsetSign
theorem OAI.CirculantHadamard.alternatingProduct_pair line 166
theorem OAI.CirculantHadamard.alternatingProduct_eq_parity line 176
Source documentation
Even subsets contribute the value itself; odd subsets contribute its inverse.
```
theorem alternatingProduct_eq_parity (t : Finset I) (x : Finset I → G) :
    alternatingProduct t x =
      ∏ S ∈ t.powerset, if Even S.card then x S else (x S)⁻¹ := by
…
```
Mentions: OAI.CirculantHadamard.alternatingProduct
theorem OAI.CirculantHadamard.alternatingProduct_eq_even_div_odd line 189
Source documentation
Collect the signed powers as a quotient of two ordinary products. Both products themselves make sense before passing to a fraction field.
```
theorem alternatingProduct_eq_even_div_odd (t : Finset I) (x : Finset I → G) :
    alternatingProduct t x = evenSubsetProduct t x / oddSubsetProduct t x := by
…
```
Mentions: OAI.CirculantHadamard.alternatingProduct, OAI.CirculantHadamard.evenSubsetProduct, OAI.CirculantHadamard.oddSubsetProduct
theorem OAI.CirculantHadamard.map_alternatingProduct line 209
Source documentation
In particular this applies to the homomorphism from local units to the fraction field, retaining the single fixed alternating product.
```
theorem map_alternatingProduct (f : G →* H) (t : Finset I) (x : Finset I → G) :
    f (alternatingProduct t x) = alternatingProduct t (fun S => f (x S)) := by
…
```
Mentions: OAI.CirculantHadamard.alternatingProduct
theorem OAI.CirculantHadamard.alternatingProduct_const line 214
Source documentation
A nonempty index set cancels every constant family, by actual subset pairing.
```
theorem alternatingProduct_const (t : Finset I) (ht : t.Nonempty) (c : G) :
    alternatingProduct t (fun _ => c) = 1 := by
…
```
Mentions: OAI.CirculantHadamard.alternatingProduct
theorem OAI.CirculantHadamard.alternatingProduct_mul_oddSubsetProduct line 224
Source documentation
Clearing the odd-subset denominator inside the group of units. Mapping this equality into the fraction field gives the polynomial identity needed before applying a homomorphism defined only on the coefficient ring.
```
theorem alternatingProduct_mul_oddSubsetProduct (t : Finset I) (x : Finset I → G) :
    alternatingProduct t x * oddSubsetProduct t x = evenSubsetProduct t x := by
…
```
Mentions: OAI.CirculantHadamard.alternatingProduct, OAI.CirculantHadamard.oddSubsetProduct, OAI.CirculantHadamard.evenSubsetProduct
def OAI.CirculantHadamard.fullAlternatingProduct line 235
Source documentation
The full prime-index product, using all subsets of the finite index type.
```
def fullAlternatingProduct (x : Finset I → G) : G :=
…
```
theorem OAI.CirculantHadamard.fullAlternatingProduct_pair line 238
theorem OAI.CirculantHadamard.fullAlternatingProduct_const line 246