OAI/Computability/FourierCircuit/SymmetricLaplacian.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactFourier.SymLap.lap line 11
  2. def OAI.ExactFourier.SymLap.tensor line 12
  3. def OAI.ExactFourier.SymLap.symmetrized line 13
  4. theorem OAI.ExactFourier.SymLap.tensor_square line 15
  5. theorem OAI.ExactFourier.SymLap.lap_factor line 18
  6. theorem OAI.ExactFourier.SymLap.lap_kill line 23
  7. theorem OAI.ExactFourier.SymLap.symmetric line 30
  8. theorem OAI.ExactFourier.SymLap.real_entries line 40
  9. theorem OAI.ExactFourier.SymLap.support_bound line 49
  10. theorem OAI.ExactFourier.det_ne_zero_of_eval_unit line 67
  11. theorem OAI.ExactFourier.unit_eval_of_not_mem_roots line 76
  12. def OAI.ExactFourier.LinearProduct.factor line 96
  13. def OAI.ExactFourier.LinearProduct.product line 98
  14. theorem OAI.ExactFourier.LinearProduct.eval_factor line 102
  15. theorem OAI.ExactFourier.LinearProduct.coeff_zero_factor line 109
  16. theorem OAI.ExactFourier.LinearProduct.coeff_one_factor line 115
  17. theorem OAI.ExactFourier.LinearProduct.coeff_one_mul line 123
  18. theorem OAI.ExactFourier.LinearProduct.eval_zero_product line 132
  19. theorem OAI.ExactFourier.LinearProduct.coeff_zero_product line 138
  20. theorem OAI.ExactFourier.LinearProduct.coeff_one_product line 144
  21. def OAI.ExactFourier.LinearProduct.quotient line 152
  22. theorem OAI.ExactFourier.LinearProduct.eval_zero_quotient line 154
  23. theorem OAI.ExactFourier.LinearProduct.split_product line 163
  24. theorem OAI.ExactFourier.LinearProduct.eval_product_cost line 178
  25. structure OAI.ExactFourier.SparseReflection.PairTerm line 203
  26. def OAI.ExactFourier.SparseReflection.PairTerm.direction line 212
  27. def OAI.ExactFourier.SparseReflection.PairTerm.den line 215
  28. theorem OAI.ExactFourier.SparseReflection.PairTerm.den_ne line 217
  29. def OAI.ExactFourier.SparseReflection.PairTerm.bad line 223
  30. theorem OAI.ExactFourier.SparseReflection.PairTerm.price line 225
  31. theorem OAI.ExactFourier.SparseReflection.pair_list_cost line 245
  32. theorem OAI.ExactFourier.SparseReflection.diagonal_family line 265
  33. theorem OAI.ExactFourier.SparseReflection.exists_tangent line 286

    Source documentation

    The exact polynomial tangent used in the first sparse-reflection specialization.

    theorem exists_tangent (p : MatrixPrice) (d : α → ℂ) (L : List (PairTerm α)) :
    ∃ Q : Matrix α α (Polynomial ℂ),∃ E : Finset ℂ,
      Q.map (evalRingHom 0)=Matrix.diagonal d+(L.map PairTerm.direction).sum ∧
      ∀ s : ℂ,s∉E → IsUnit (1+s•Q.map (evalRingHom s)) ∧
        p.value (1+s•Q.map (evalRingHom s))≤(3:ℝ)/2*L.length := by
…

    Mentions: OAI.ExactFourier.MatrixPrice, OAI.ExactFourier.L, OAI.ExactFourier.SparseReflection.PairTerm, OAI.ExactFourier.SparseReflection.PairTerm.direction

  34. def OAI.ExactFourier.MatrixPrice.cayley line 325
  35. theorem OAI.ExactFourier.MatrixPrice.cayley_unit line 328
  36. theorem OAI.ExactFourier.MatrixPrice.cayley_denominator line 332
  37. theorem OAI.ExactFourier.MatrixPrice.cayley_response line 340
  38. theorem OAI.ExactFourier.MatrixPrice.cayley_feedback line 363