OAI/Computability/FourierCircuit/RationalClearing.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Entrywise regular rational matrices and a common scalar denominator. Regularity is absence of a pole: the reduced polynomial denominator is nonzero at the point. Evaluation is only claimed on this domain.

  1. def OAI.ExactFourier.RationalMatrix.eval line 14
  2. def OAI.ExactFourier.RationalMatrix.RegularAt line 17
  3. def OAI.ExactFourier.RationalMatrix.denominator line 20
  4. def OAI.ExactFourier.RationalMatrix.numerator line 23
  5. theorem OAI.ExactFourier.RationalMatrix.denominator_factor line 26
  6. theorem OAI.ExactFourier.RationalMatrix.denominator_eval_ne_zero line 31
  7. theorem OAI.ExactFourier.RationalMatrix.regular_of_denominator line 37
  8. theorem OAI.ExactFourier.RationalMatrix.eval_clearing line 43
  9. theorem OAI.ExactFourier.MatrixPrice.specialize_polynomial line 61
  10. theorem OAI.ExactFourier.MatrixPrice.specialization line 82

    Source documentation

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

    theorem specialization (p : MatrixPrice) (X : Matrix α α (RatFunc ℂ)) (z0 : ℂ)
    (hreg : RationalMatrix.RegularAt X z0) (hX0 : IsUnit (RationalMatrix.eval X z0))
    (E : Finset ℂ) (C0 : ℝ)
    (hX : ∀ s : ℂ,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 := by
…

    Mentions: OAI.ExactFourier.MatrixPrice, OAI.ExactFourier.RationalMatrix.RegularAt, OAI.ExactFourier.RationalMatrix.eval

  11. theorem OAI.ExactFourier.MatrixPrice.cayley_tangent line 123
  12. def OAI.ExactFourier.CayleyLimit.active line 195
  13. def OAI.ExactFourier.CayleyLimit.denominator line 196
  14. def OAI.ExactFourier.CayleyLimit.except line 197
  15. def OAI.ExactFourier.CayleyLimit.numerator line 198
  16. def OAI.ExactFourier.CayleyLimit.sign line 200
  17. theorem OAI.ExactFourier.CayleyLimit.denominator_factor line 202
  18. theorem OAI.ExactFourier.CayleyLimit.denominator_zero line 206
  19. theorem OAI.ExactFourier.CayleyLimit.numerator_zero line 214
  20. theorem OAI.ExactFourier.CayleyLimit.numerator_identity line 221
  21. def OAI.ExactFourier.CayleyLimit.polynomial line 230
  22. theorem OAI.ExactFourier.CayleyLimit.eval_polynomial line 233
  23. theorem OAI.ExactFourier.CayleyLimit.eval_zero line 241
  24. theorem OAI.ExactFourier.CayleyLimit.eval_as_cayley line 249
  25. def OAI.ExactFourier.CayleyLimit.bad line 265
  26. theorem OAI.ExactFourier.CayleyLimit.generic_units line 267
  27. theorem OAI.ExactFourier.CayleyLimit.price line 293

    Source documentation

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

    theorem price (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 := by
…

    Mentions: OAI.ExactFourier.MatrixPrice, OAI.ExactFourier.Similarity.conj, OAI.ExactFourier.MatrixPrice.cayley, OAI.ExactFourier.CayleyLimit.sign

  28. def OAI.ExactFourier.CayleyLimit.reciprocal line 329
  29. theorem OAI.ExactFourier.CayleyLimit.sign_square line 331
  30. theorem OAI.ExactFourier.CayleyLimit.reflection_square line 338
  31. theorem OAI.ExactFourier.CayleyLimit.killed_sum line 342
  32. theorem OAI.ExactFourier.CayleyLimit.difference_factor line 353
  33. theorem OAI.ExactFourier.CayleyLimit.reflection_symm line 367