PolynomialDegree.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Polynomial degree and the Walsh filtration

The polynomial lemmas concern real multilinear MvPolynomials. Restriction to the cube is justified by an explicit monomial expansion rather than assumed as an alternate polynomial representation.

theorem OAI.LeanBlast.GotsmanLinial.IsMultilinear.add_C line 23
Source documentation
Adding a constant preserves the multilinearity condition.
```
theorem IsMultilinear.add_C {p : MvPolynomial (Fin n) ℝ}
    (hp : IsMultilinear p) (c : ℝ) : IsMultilinear (p + MvPolynomial.C c) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear

theorem OAI.LeanBlast.GotsmanLinial.totalDegree_add_C_le line 36

Source documentation

Adding a constant cannot violate an existing total-degree upper bound.

theorem totalDegree_add_C_le {p : MvPolynomial (Fin n) ℝ}
    (hd : p.totalDegree ≤ d) (c : ℝ) :
    (p + MvPolynomial.C c).totalDegree ≤ d := by
…

theorem OAI.LeanBlast.GotsmanLinial.IsMultilinear.exponent_eq_one line 42
Source documentation
Every exponent occurring in a supported multilinear monomial is one.
```
theorem IsMultilinear.exponent_eq_one {p : MvPolynomial (Fin n) ℝ}
    (hp : IsMultilinear p) {m : Fin n →₀ ℕ} (hm : m ∈ p.support)
    {i : Fin n} (hi : i ∈ m.support) : m i = 1 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear
theorem OAI.LeanBlast.GotsmanLinial.monomial_support_card_le_totalDegree line 50
Source documentation
A supported monomial has no more variables than the polynomial's total degree. This estimate does not require multilinearity.
```
theorem monomial_support_card_le_totalDegree {p : MvPolynomial (Fin n) ℝ}
    {m : Fin n →₀ ℕ} (hm : m ∈ p.support) : m.support.card ≤ p.totalDegree := by
…
```
theorem OAI.LeanBlast.GotsmanLinial.polynomialValue_eq_multilinear_expansion line 62
Source documentation
Faithful evaluation of a multilinear polynomial as products over the supports of its monomials.
```
theorem polynomialValue_eq_multilinear_expansion {p : MvPolynomial (Fin n) ℝ}
    (hp : IsMultilinear p) (x : Cube n) :
    polynomialValue p x =
      ∑ m ∈ p.support, p.coeff m * ∏ i ∈ m.support, cubeCoord x i := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.polynomialValue, OAI.LeanBlast.GotsmanLinial.cubeCoord
theorem OAI.LeanBlast.GotsmanLinial.polynomialValue_walsh_expansion line 77
Source documentation
The same faithful expansion, with values regarded as complex numbers.
```
theorem polynomialValue_walsh_expansion {p : MvPolynomial (Fin n) ℝ}
    (hp : IsMultilinear p) (x : Cube n) :
    (polynomialValue p x : ℂ) =
      ∑ m ∈ p.support, ((p.coeff m : ℝ) : ℂ) * walshChar m.support x := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.polynomialValue, OAI.LeanBlast.GotsmanLinial.walshChar
theorem OAI.LeanBlast.GotsmanLinial.walshChar_mem_fourierSpace line 85
Source documentation
A character of degree at most d belongs to the corresponding filtration.
```
theorem walshChar_mem_fourierSpace {S : Finset (Fin n)} (hS : S.card ≤ d) :
    walshChar S ∈ fourierSpace n d :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.walshChar, OAI.LeanBlast.GotsmanLinial.fourierSpace
theorem OAI.LeanBlast.GotsmanLinial.polynomialValue_mem_fourierSpace line 90
Source documentation
The exact polynomial bridge into the complex Walsh filtration.
```
theorem polynomialValue_mem_fourierSpace {p : MvPolynomial (Fin n) ℝ}
    (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) :
    (fun x => (polynomialValue p x : ℂ)) ∈ fourierSpace n d := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.polynomialValue, OAI.LeanBlast.GotsmanLinial.fourierSpace
theorem OAI.LeanBlast.GotsmanLinial.fourierSpace_star line 106
Source documentation
Complex conjugation preserves Fourier degree, since each character is real.
```
theorem fourierSpace_star {a : Cube n → ℂ} (ha : a ∈ fourierSpace n d) :
    star a ∈ fourierSpace n d := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierSpace
theorem OAI.LeanBlast.GotsmanLinial.fourierSpace_mul line 124
Source documentation
The filtration is multiplicative. The symmetric difference of two index sets has cardinality at most the sum of their cardinalities.
```
theorem fourierSpace_mul {r s : ℕ} {a b : Cube n → ℂ}
    (ha : a ∈ fourierSpace n r) (hb : b ∈ fourierSpace n s) :
    a * b ∈ fourierSpace n (r + s) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierSpace
theorem OAI.LeanBlast.GotsmanLinial.fourierSpace_conj_mul line 150
Source documentation
The precise multiplication-conjugation rule used in the weighted pairing.
```
theorem fourierSpace_conj_mul {r s : ℕ} {a b : Cube n → ℂ}
    (ha : a ∈ fourierSpace n r) (hb : b ∈ fourierSpace n s) :
    (fun x => star (b x) * a x) ∈ fourierSpace n (r + s) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierSpace
theorem OAI.LeanBlast.GotsmanLinial.cubeCoord_mul_mem_fourierSpace line 157
Source documentation
Multiplication by one cube coordinate raises the degree by at most one.
```
theorem cubeCoord_mul_mem_fourierSpace {r : ℕ} {a : Cube n → ℂ}
    (ha : a ∈ fourierSpace n r) (i : Fin n) :
    (fun x => (cubeCoord x i : ℂ) * a x) ∈ fourierSpace n (r + 1) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierSpace, OAI.LeanBlast.GotsmanLinial.cubeCoord
def OAI.LeanBlast.GotsmanLinial.fourierSpaceFrom line 169
Source documentation
Functions whose Walsh support starts in degree k.
```
def fourierSpaceFrom (n k : ℕ) : Submodule ℂ (Cube n → ℂ) :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
theorem OAI.LeanBlast.GotsmanLinial.walshChar_mem_fourierSpaceFrom line 172
theorem OAI.LeanBlast.GotsmanLinial.parity_mul_mem_fourierSpaceFrom line 178
Source documentation
Full parity complements character index sets, taking low degree d to Fourier support in degrees at least n - d.
```
theorem parity_mul_mem_fourierSpaceFrom {a : Cube n → ℂ}
    (ha : a ∈ fourierSpace n d) :
    (fun x => walshChar Finset.univ x * a x) ∈ fourierSpaceFrom n (n - d) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierSpace, OAI.LeanBlast.GotsmanLinial.walshChar, OAI.LeanBlast.GotsmanLinial.fourierSpaceFrom
theorem OAI.LeanBlast.GotsmanLinial.sum_mul_eq_zero_of_fourier_separated line 201
Source documentation
Low and high Fourier support with a strict gap have zero counting pairing. There is no conjugation in this formulation because Walsh characters are real; it applies directly to the product appearing in the weighted proof.
```
theorem sum_mul_eq_zero_of_fourier_separated {r s : ℕ} {a b : Cube n → ℂ}
    (ha : a ∈ fourierSpace n r) (hb : b ∈ fourierSpaceFrom n s) (hrs : r < s) :
    (∑ x : Cube n, a x * b x) = 0 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierSpace, OAI.LeanBlast.GotsmanLinial.fourierSpaceFrom
theorem OAI.LeanBlast.GotsmanLinial.parity_polynomialValue_mem_fourierSpaceFrom line 229
Source documentation
The polynomial has high Fourier support after multiplication by full parity, with no alternate polynomial-class assumption.
```
theorem parity_polynomialValue_mem_fourierSpaceFrom {p : MvPolynomial (Fin n) ℝ}
    (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) :
    (fun x => walshChar Finset.univ x * (polynomialValue p x : ℂ)) ∈
      fourierSpaceFrom n (n - d) :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.walshChar, OAI.LeanBlast.GotsmanLinial.polynomialValue, OAI.LeanBlast.GotsmanLinial.fourierSpaceFrom
theorem OAI.LeanBlast.GotsmanLinial.parity_polynomialValue_low_coefficient_eq_zero line 237
Source documentation
Every Fourier coefficient below n - d of the parity-transformed polynomial vanishes.
```
theorem parity_polynomialValue_low_coefficient_eq_zero {p : MvPolynomial (Fin n) ℝ}
    (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) {S : Finset (Fin n)}
    (hS : S.card < n - d) :
    walshCoefficientLinear S
      (fun x => walshChar Finset.univ x * (polynomialValue p x : ℂ)) = 0 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.walshCoefficientLinear, OAI.LeanBlast.GotsmanLinial.walshChar, OAI.LeanBlast.GotsmanLinial.polynomialValue