Exact Fourier circuits: rational clearing

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/RationalClearing.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

noncomputable def Complexity.ExactFourier.RationalMatrix.eval {α : Type} (X : Matrix α α (RatFunc ℂ)) (s : ℂ) : Matrix α α ℂ

Evaluate every rational-function entry at one complex scalar.

Equations

• Complexity.ExactFourier.RationalMatrix.eval X s = X.map (RatFunc.eval (RingHom.id ℂ) s)

def Complexity.ExactFourier.RationalMatrix.RegularAt {α : Type} (X : Matrix α α (RatFunc ℂ)) (s : ℂ) : Prop

Every entry denominator is nonzero at the specified evaluation point.

Equations

• Complexity.ExactFourier.RationalMatrix.RegularAt X s = ∀ (i j : α), Polynomial.eval s (X i j).denom ≠ 0

noncomputable def Complexity.ExactFourier.RationalMatrix.denominator {α : Type} [Fintype α] (X : Matrix α α (RatFunc ℂ)) : Polynomial ℂ

The common denominator formed by multiplying all matrix-entry denominators.

Equations

• Complexity.ExactFourier.RationalMatrix.denominator X = ∏ v : α × α, (X v.1 v.2).denom

noncomputable def Complexity.ExactFourier.RationalMatrix.numerator {α : Type} [Fintype α] [DecidableEq α] (X : Matrix α α (RatFunc ℂ)) : Matrix α α (Polynomial ℂ)

The polynomial matrix obtained by clearing the common denominator.

Equations

• Complexity.ExactFourier.RationalMatrix.numerator X i j = (X i j).num * ∏ v ∈ Finset.univ.erase (i, j), (X v.1 v.2).denom

theorem Complexity.ExactFourier.RationalMatrix.denominator_factor {α : Type} [Fintype α] [DecidableEq α] (X : Matrix α α (RatFunc ℂ)) (i j : α) : denominator X = (X i j).denom * ∏ v ∈ Finset.univ.erase (i, j), (X v.1 v.2).denom

theorem Complexity.ExactFourier.RationalMatrix.denominator_eval_ne_zero {α : Type} [Fintype α] (X : Matrix α α (RatFunc ℂ)) (s : ℂ) (hX : RegularAt X s) : Polynomial.eval s (denominator X) ≠ 0

theorem Complexity.ExactFourier.RationalMatrix.regular_of_denominator {α : Type} [Fintype α] [DecidableEq α] (X : Matrix α α (RatFunc ℂ)) (s : ℂ) (hX : Polynomial.eval s (denominator X) ≠ 0) : RegularAt X s

theorem Complexity.ExactFourier.RationalMatrix.eval_clearing {α : Type} [Fintype α] [DecidableEq α] (X : Matrix α α (RatFunc ℂ)) (s : ℂ) (hX : RegularAt X s) : (numerator X).map (Polynomial.eval s) = Polynomial.eval s (denominator X) • eval X s

theorem Complexity.ExactFourier.MatrixPrice.specialize_polynomial {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (G : Matrix α α (Polynomial ℂ)) (z0 : ℂ) (hG0 : IsUnit (G.map (Polynomial.eval z0))) (E : Finset ℂ) (C0 : ℝ) (hG : ∀ s ∉ E, IsUnit (G.map (Polynomial.eval s)) ∧ p.value (G.map (Polynomial.eval s)) ≤ C0) : p.value (G.map (Polynomial.eval z0)) ≤ C0

theorem Complexity.ExactFourier.MatrixPrice.specialization {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (X : Matrix α α (RatFunc ℂ)) (z0 : ℂ) (hreg : RationalMatrix.RegularAt X z0) (hX0 : IsUnit (RationalMatrix.eval X z0)) (E : Finset ℂ) (C0 : ℝ) (hX : ∀ s ∉ E, RationalMatrix.RegularAt X s ∧ IsUnit (RationalMatrix.eval X s) ∧ p.value (RationalMatrix.eval X s) ≤ C0) : p.value (RationalMatrix.eval X z0) ≤ C0

Literal algebraic specialization (06-feedback:383--393), including a finite exceptional set which may contain the specialization point itself.

theorem Complexity.ExactFourier.MatrixPrice.cayley_tangent {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (Q : Matrix α α (Polynomial ℂ)) (E : Finset ℂ) (C0 : ℝ) (hQ : ∀ s ∉ E, IsUnit (1 + s • Q.map (Polynomial.eval s)) ∧ p.value (1 + s • Q.map (Polynomial.eval s)) ≤ C0) (t : ℂ) (hp : IsUnit (1 + t • Q.map (Polynomial.eval 0))) (hm : IsUnit (1 - t • Q.map (Polynomial.eval 0))) : p.value (cayley (Q.map (Polynomial.eval 0)) t) ≤ C0 + 2 * ↑(Fintype.card α)

noncomputable def Complexity.ExactFourier.CayleyLimit.active {α : Type} [Fintype α] (a : α → ℂ) : Finset α

Indices with nonzero eigenvalue parameters.

Equations

• Complexity.ExactFourier.CayleyLimit.active a = {i : α | a i ≠ 0}

noncomputable def Complexity.ExactFourier.CayleyLimit.denominator {α : Type} [Fintype α] (a : α → ℂ) : Polynomial ℂ

The product of linear factors associated with all nonzero parameters.

Equations

• Complexity.ExactFourier.CayleyLimit.denominator a = ∏ i ∈ Complexity.ExactFourier.CayleyLimit.active a, (Polynomial.X - Polynomial.C (a i))

noncomputable def Complexity.ExactFourier.CayleyLimit.except {α : Type} [Fintype α] [DecidableEq α] (a : α → ℂ) (i : α) : Polynomial ℂ

The active denominator product with one selected factor omitted.

Equations

• Complexity.ExactFourier.CayleyLimit.except a i = ∏ j ∈ (Complexity.ExactFourier.CayleyLimit.active a).erase i, (Polynomial.X - Polynomial.C (a j))

noncomputable def Complexity.ExactFourier.CayleyLimit.numerator {α : Type} [Fintype α] [DecidableEq α] (a : α → ℂ) (i : α) : Polynomial ℂ

The selected Cayley numerator after clearing the common denominator.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.ExactFourier.CayleyLimit.sign {α : Type} (a : α → ℂ) (i : α) : ℂ

The limiting sign: one on zero parameters and minus one on nonzero parameters.

Equations

• Complexity.ExactFourier.CayleyLimit.sign a i = if a i = 0 then 1 else -1

theorem Complexity.ExactFourier.CayleyLimit.denominator_factor {α : Type} [Fintype α] [DecidableEq α] (a : α → ℂ) (i : α) (hi : a i ≠ 0) : denominator a = (Polynomial.X - Polynomial.C (a i)) * except a i

theorem Complexity.ExactFourier.CayleyLimit.denominator_zero {α : Type} [Fintype α] (a : α → ℂ) : Polynomial.eval 0 (denominator a) ≠ 0

theorem Complexity.ExactFourier.CayleyLimit.numerator_zero {α : Type} [Fintype α] [DecidableEq α] (a : α → ℂ) (i : α) : Polynomial.eval 0 (numerator a i) = Polynomial.eval 0 (denominator a) * sign a i

theorem Complexity.ExactFourier.CayleyLimit.numerator_identity {α : Type} [Fintype α] [DecidableEq α] (a : α → ℂ) (i : α) (s : ℂ) (hs : s ≠ 0) : Polynomial.eval s (numerator a i) * (1 - s⁻¹ * a i) = Polynomial.eval s (denominator a) * (1 + s⁻¹ * a i)

noncomputable def Complexity.ExactFourier.CayleyLimit.polynomial {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) (a : α → ℂ) : Matrix α α (Polynomial ℂ)

Conjugate the diagonal cleared Cayley numerators by U.

Equations

• Complexity.ExactFourier.CayleyLimit.polynomial U a = U.map ⇑Polynomial.C * Matrix.diagonal (Complexity.ExactFourier.CayleyLimit.numerator a) * U⁻¹.map ⇑Polynomial.C

theorem Complexity.ExactFourier.CayleyLimit.eval_polynomial {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) (a : α → ℂ) (s : ℂ) : (polynomial U a).map ⇑(Polynomial.evalRingHom s) = Similarity.conj U (Matrix.diagonal fun (i : α) => Polynomial.eval s (numerator a i))

theorem Complexity.ExactFourier.CayleyLimit.eval_zero {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) (a : α → ℂ) : (polynomial U a).map ⇑(Polynomial.evalRingHom 0) = Polynomial.eval 0 (denominator a) • Similarity.conj U (Matrix.diagonal (sign a))

theorem Complexity.ExactFourier.CayleyLimit.eval_as_cayley {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) (hU : IsUnit U) (a : α → ℂ) (s : ℂ) (hs : s ≠ 0) (hm : IsUnit (1 - s⁻¹ • Similarity.conj U (Matrix.diagonal a))) : (polynomial U a).map ⇑(Polynomial.evalRingHom s) = Polynomial.eval s (denominator a) • MatrixPrice.cayley (Similarity.conj U (Matrix.diagonal a)) s⁻¹

noncomputable def Complexity.ExactFourier.CayleyLimit.bad {α : Type} [Fintype α] (a : α → ℂ) : Finset ℂ

The excluded scalar parameters: zero, the eigenvalues, and their negatives.

Equations

• Complexity.ExactFourier.CayleyLimit.bad a = insert 0 (Finset.image a Finset.univ ∪ Finset.image (fun (i : α) => -a i) Finset.univ)

theorem Complexity.ExactFourier.CayleyLimit.generic_units {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) (hU : IsUnit U) (a : α → ℂ) (s : ℂ) (hs : s ∉ bad a) : s ≠ 0 ∧ Polynomial.eval s (denominator a) ≠ 0 ∧ IsUnit (1 + s⁻¹ • Similarity.conj U (Matrix.diagonal a)) ∧ IsUnit (1 - s⁻¹ • Similarity.conj U (Matrix.diagonal a))

theorem Complexity.ExactFourier.CayleyLimit.price {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (U : Matrix α α ℂ) (hU : IsUnit U) (a : α → ℂ) (C0 : ℝ) (hp : ∀ (t : ℂ), IsUnit (1 + t • Similarity.conj U (Matrix.diagonal a)) → IsUnit (1 - t • Similarity.conj U (Matrix.diagonal a)) → p.value (MatrixPrice.cayley (Similarity.conj U (Matrix.diagonal a)) t) ≤ C0) : p.value (Similarity.conj U (Matrix.diagonal (sign a))) ≤ C0

The second specialization; no priced use of the diagonalizing basis is made.

noncomputable def Complexity.ExactFourier.CayleyLimit.reciprocal {α : Type} (a : α → ℂ) (i : α) : ℂ

Twice the reciprocal of each nonzero parameter, with zero retained at zero.

Equations

• Complexity.ExactFourier.CayleyLimit.reciprocal a i = if a i = 0 then 0 else 2 / a i

theorem Complexity.ExactFourier.CayleyLimit.sign_square {α : Type} [Fintype α] [DecidableEq α] (a : α → ℂ) : Matrix.diagonal (sign a) * Matrix.diagonal (sign a) = 1

theorem Complexity.ExactFourier.CayleyLimit.reflection_square {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) (hU : IsUnit U) (a : α → ℂ) : Similarity.conj U (Matrix.diagonal (sign a)) * Similarity.conj U (Matrix.diagonal (sign a)) = 1

theorem Complexity.ExactFourier.CayleyLimit.killed_sum {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) (hU : IsUnit U) (a : α → ℂ) : Similarity.conj U (Matrix.diagonal a) * (1 + Similarity.conj U (Matrix.diagonal (sign a))) = 0

theorem Complexity.ExactFourier.CayleyLimit.difference_factor {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) (hU : IsUnit U) (a : α → ℂ) : 1 - Similarity.conj U (Matrix.diagonal (sign a)) = Similarity.conj U (Matrix.diagonal a) * Similarity.conj U (Matrix.diagonal (reciprocal a))

theorem Complexity.ExactFourier.CayleyLimit.reflection_symm {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) (hi : U⁻¹ = U.transpose) (a : α → ℂ) : (Similarity.conj U (Matrix.diagonal (sign a))).IsSymm