BlockVanishing.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Vanishing of low antidiagonal blocks

The geometric step is reduced to an explicit finite sum: multiplication on both sides by the square root of a positive weight turns the weighted pairing into a Fourier pairing against the signed weight.

theorem OAI.LeanBlast.GotsmanLinial.abs_mul_thresholdSign line 29
Source documentation
The threshold convention at zero is compatible with the signed absolute value identity used to build the weighted grading.
```
theorem abs_mul_thresholdSign (t : ℝ) : |t| * thresholdSign t = t := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.thresholdSign

theorem OAI.LeanBlast.GotsmanLinial.projectionBlock_eq_zero_of_pairing line 36

Source documentation

If the image of one subspace under an operator is orthogonal to a second subspace, the corresponding projection block vanishes.

theorem projectionBlock_eq_zero_of_pairing
    {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
    (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection]
    (H : E →L[𝕜] E)
    (hpair : ∀ u ∈ U, ∀ v ∈ V, inner 𝕜 v (H u) = 0) :
    V.starProjection * H * U.starProjection = 0 := by
…

theorem OAI.LeanBlast.GotsmanLinial.projectionBlock_eq_zero_of_map_pairing line 50

Source documentation

Lift an orthogonality calculation on preimages through a common linear map to a zero block between subspaces of its images.

theorem projectionBlock_eq_zero_of_map_pairing
    {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
    (A B U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection]
    (D : E →ₗ[𝕜] E) (H : E →L[𝕜] E)
    (hU : U ≤ A.map D) (hV : V ≤ B.map D)
    (hpair : ∀ a ∈ A, ∀ b ∈ B, inner 𝕜 (D b) (H (D a)) = 0) :
    V.starProjection * H * U.starProjection = 0 := by
…

theorem OAI.LeanBlast.GotsmanLinial.sqrtWeight_inner_eq_sum line 65

Source documentation

The finite pairing identity underlying the low antidiagonal cutoff. The norm and inner product are the counting Euclidean ones.

theorem sqrtWeight_inner_eq_sum
    {Ω : Type*} [Fintype Ω]
    (w h : Ω → ℝ) (hw : ∀ x, 0 ≤ w x)
    (D : EuclideanSpace ℂ Ω →ₗ[ℂ] EuclideanSpace ℂ Ω)
    (hD : ∀ a x, D a x = (Real.sqrt (w x) : ℂ) * a x)
    (H : EuclideanSpace ℂ Ω →L[ℂ] EuclideanSpace ℂ Ω)
    (hH : ∀ a x, H a x = (h x : ℂ) * a x)
    (a b : EuclideanSpace ℂ Ω) :
    inner ℂ (D b) (H (D a)) =
      ∑ x, star (b x) * a x * ((w x : ℂ) * (h x : ℂ)) := by
…

theorem OAI.LeanBlast.GotsmanLinial.sqrtWeight_inner_eq_sum_signedWeight line 90

Source documentation

Replace the weight times the diagonal sign by the actual signed weight.

theorem sqrtWeight_inner_eq_sum_signedWeight
    {Ω : Type*} [Fintype Ω]
    (w h : Ω → ℝ) (q : Ω → ℂ) (hw : ∀ x, 0 ≤ w x)
    (hwq : ∀ x, (w x : ℂ) * (h x : ℂ) = q x)
    (D : EuclideanSpace ℂ Ω →ₗ[ℂ] EuclideanSpace ℂ Ω)
    (hD : ∀ a x, D a x = (Real.sqrt (w x) : ℂ) * a x)
    (H : EuclideanSpace ℂ Ω →L[ℂ] EuclideanSpace ℂ Ω)
    (hH : ∀ a x, H a x = (h x : ℂ) * a x)
    (a b : EuclideanSpace ℂ Ω) :
    inner ℂ (D b) (H (D a)) = ∑ x, star (b x) * a x * q x := by
…

theorem OAI.LeanBlast.GotsmanLinial.sqrtWeight_pairing_eq_zero_of_fourier_separation line 105

Source documentation

High Fourier support of the signed weight kills every pairing whose two unweighted degrees have smaller total degree.

theorem sqrtWeight_pairing_eq_zero_of_fourier_separation
    {n r s k : ℕ} (w h : Cube n → ℝ) (q : Cube n → ℂ)
    (hw : ∀ x, 0 ≤ w x) (hwq : ∀ x, (w x : ℂ) * (h x : ℂ) = q x)
    (D : EuclideanSpace ℂ (Cube n) →ₗ[ℂ] EuclideanSpace ℂ (Cube n))
    (hD : ∀ a x, D a x = (Real.sqrt (w x) : ℂ) * a x)
    (H : EuclideanSpace ℂ (Cube n) →L[ℂ] EuclideanSpace ℂ (Cube n))
    (hH : ∀ a x, H a x = (h x : ℂ) * a x)
    (a b : EuclideanSpace ℂ (Cube n))
    (ha : WithLp.ofLp a ∈ fourierSpace n r)
    (hb : WithLp.ofLp b ∈ fourierSpace n s)
    (hq : q ∈ fourierSpaceFrom n k) (hrs : r + s < k) :
    inner ℂ (D b) (H (D a)) = 0 := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierSpace, OAI.LeanBlast.GotsmanLinial.fourierSpaceFrom

theorem OAI.LeanBlast.GotsmanLinial.polynomial_signedWeight line 122
Source documentation
The choices w = |p| and h = parity * sign(p) multiply to the high-degree signed polynomial, including at a zero of the polynomial.
```
theorem polynomial_signedWeight {n : ℕ} (p : MvPolynomial (Fin n) ℝ) (x : Cube n) :
    ((|polynomialValue p x| : ℝ) : ℂ) *
        ((fullParity x * thresholdSign (polynomialValue p x) : ℝ) : ℂ) =
      walshChar Finset.univ x * (polynomialValue p x : ℂ) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.polynomialValue, OAI.LeanBlast.GotsmanLinial.fullParity, OAI.LeanBlast.GotsmanLinial.thresholdSign, OAI.LeanBlast.GotsmanLinial.walshChar
theorem OAI.LeanBlast.GotsmanLinial.polynomial_sqrtWeight_pairing_eq_zero line 139
Source documentation
The weighted pairing vanishes for the polynomial, weight, and parity-modified threshold sign. No Fourier-support assumption remains.
```
theorem polynomial_sqrtWeight_pairing_eq_zero
    {n d r s : ℕ} (p : MvPolynomial (Fin n) ℝ)
    (hp : IsMultilinear p) (hd : p.totalDegree ≤ d)
    (hnz : ∀ x, polynomialValue p x ≠ 0)
    (a b : EuclideanSpace ℂ (Cube n))
    (ha : WithLp.ofLp a ∈ fourierSpace n r)
    (hb : WithLp.ofLp b ∈ fourierSpace n s) (hrs : r + s < n - d) :
    let D := sqrtWeightEquiv (fun x => |polynomialValue p x|)
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.polynomialValue, OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fourierSpace, OAI.LeanBlast.GotsmanLinial.sqrtWeightEquiv

theorem OAI.LeanBlast.GotsmanLinial.polynomial_projectionBlock_eq_zero line 163

Source documentation

The operator between two subspaces of weighted low-degree spaces is zero below the polynomial's degree cutoff.

theorem polynomial_projectionBlock_eq_zero
    {n d r s : ℕ} (p : MvPolynomial (Fin n) ℝ)
    (hp : IsMultilinear p) (hd : p.totalDegree ≤ d)
    (hnz : ∀ x, polynomialValue p x ≠ 0)
    (U V : Submodule ℂ (EuclideanSpace ℂ (Cube n)))
    (hU : U ≤ weightedFourierSpace (fun x => |polynomialValue p x|)
      (fun x => abs_pos.mpr (hnz x)) r)
    (hV : V ≤ weightedFourierSpace (fun x => |polynomialValue p x|)
      (fun x => abs_pos.mpr (hnz x)) s)
    (hrs : r + s < n - d) :
    V.starProjection *
      signMultiplier (fun x => fullParity x * thresholdSign (polynomialValue p x)) *
…

Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.polynomialValue, OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.weightedFourierSpace, OAI.LeanBlast.GotsmanLinial.signMultiplier, OAI.LeanBlast.GotsmanLinial.fullParity, OAI.LeanBlast.GotsmanLinial.thresholdSign

theorem OAI.LeanBlast.GotsmanLinial.weightedFlag_block_eq_zero_of_polynomial_degree line 188
Source documentation
Low antidiagonal vanishing for the actual weighted grading constructed from the polynomial. All geometric hypotheses are discharged.
```
theorem weightedFlag_block_eq_zero_of_polynomial_degree
    {n d r s : ℕ} (p : MvPolynomial (Fin n) ℝ)
    (hp : IsMultilinear p) (hd : p.totalDegree ≤ d)
    (hnz : ∀ x, polynomialValue p x ≠ 0) (hrs : r + s < n - d) :
    let K := weightedFourierFlag (fun x => |polynomialValue p x|)
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.polynomialValue, OAI.LeanBlast.GotsmanLinial.weightedFourierFlag

theorem OAI.LeanBlast.GotsmanLinial.weightedFlag_matrixBlock_eq_zero_of_polynomial_degree line 211

Source documentation

The same vanishing statement in any orthonormal matrix coordinates, ready for the Hilbert-Schmidt block coupling.

theorem weightedFlag_matrixBlock_eq_zero_of_polynomial_degree
    {n d r s : ℕ} (p : MvPolynomial (Fin n) ℝ)
    (hp : IsMultilinear p) (hd : p.totalDegree ≤ d)
    (hnz : ∀ x, polynomialValue p x ≠ 0) (hrs : r + s < n - d)
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (b : OrthonormalBasis ι ℂ (EuclideanSpace ℂ (Cube n))) :
    let K := weightedFourierFlag (fun x => |polynomialValue p x|)
…

Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.polynomialValue, OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.weightedFourierFlag

theorem OAI.LeanBlast.GotsmanLinial.weightedProjectionMatrix_block_eq_zero_of_polynomial_degree line 230
Source documentation
The concrete cutoff used by the finite block coupling: actual weighted projection matrices, actual diagonal parity-modified polynomial threshold, and no unproved construction assumptions.
```
theorem weightedProjectionMatrix_block_eq_zero_of_polynomial_degree
    {n d : ℕ} (p : MvPolynomial (Fin n) ℝ)
    (hp : IsMultilinear p) (hd : p.totalDegree ≤ d)
    (hnz : ∀ x, polynomialValue p x ≠ 0)
    (r s : Fin (n + 1)) (hrs : r.val + s.val < n - d) :
    let w := fun x => |polynomialValue p x|
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.polynomialValue