OAI/Computability/FourierCircuit/ParameterAlgebra.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactFourier.PositiveGeneration.evalMatrix line 12
  2. theorem OAI.ExactFourier.PositiveGeneration.evalMatrix_apply line 15
  3. theorem OAI.ExactFourier.PositiveGeneration.evalMatrix_mul line 18
  4. theorem OAI.ExactFourier.PositiveGeneration.evalMatrix_const line 21
  5. theorem OAI.ExactFourier.PositiveGeneration.evalMatrix_rename line 24
  6. theorem OAI.ExactFourier.PositiveGeneration.evalMatrix_diag line 30
  7. def OAI.ExactFourier.PositiveGeneration.diagCLM line 34
  8. theorem OAI.ExactFourier.PositiveGeneration.diagCLM_apply line 35
  9. def OAI.ExactFourier.PositiveGeneration.leftProj line 37
  10. def OAI.ExactFourier.PositiveGeneration.rightProj line 39
  11. theorem OAI.ExactFourier.PositiveGeneration.leftProj_apply line 41
  12. theorem OAI.ExactFourier.PositiveGeneration.rightProj_apply line 43
  13. structure OAI.ExactFourier.PositiveGeneration.Param line 59

    Source documentation

    A fixed positive word with polynomial diagonal parameters and its exact derivative.

    structure Param (A p : Matrix α α ℂ) (U : Submodule ℂ (Matrix α α ℂ)) where
…
  14. def OAI.ExactFourier.PositiveGeneration.Param.nil line 72
  15. def OAI.ExactFourier.PositiveGeneration.Param.nextPoly line 91
  16. theorem OAI.ExactFourier.PositiveGeneration.Param.eval_nextPoly line 95
  17. def OAI.ExactFourier.PositiveGeneration.Param.nextDerivative line 101
  18. theorem OAI.ExactFourier.PositiveGeneration.Param.nextDerivative_apply line 106
  19. theorem OAI.ExactFourier.PositiveGeneration.Param.next_deriv line 112
  20. theorem OAI.ExactFourier.PositiveGeneration.Param.base_unit line 139
  21. def OAI.ExactFourier.PositiveGeneration.Param.snoc line 143
  22. theorem OAI.ExactFourier.PositiveGeneration.Chain.parameterization line 175
  23. theorem OAI.ExactFourier.PositiveGeneration.Param.derivative_surjective line 183
  24. def OAI.ExactFourier.PositiveGeneration.flatten line 203
  25. def OAI.ExactFourier.PositiveGeneration.flatCLM line 211
  26. theorem OAI.ExactFourier.PositiveGeneration.flatCLM_apply line 213
  27. def OAI.ExactFourier.PositiveGeneration.Param.hom line 216
  28. theorem OAI.ExactFourier.PositiveGeneration.Param.polynomialMap_hom line 219
  29. theorem OAI.ExactFourier.PositiveGeneration.Param.hom_injective line 224
  30. theorem OAI.ExactFourier.PositiveGeneration.Param.open_word line 235
  31. theorem OAI.ExactFourier.PositiveGeneration.polynomial_nonzero_dense line 267

    Source documentation

    Nonempty Zariski basic opens in complex affine space are Euclidean dense.

    theorem polynomial_nonzero_dense (g : MvPolynomial ι ℂ) (hg : g≠0) :
    Dense {y : ι→ℂ | aeval y g≠0} := by
…
  32. theorem OAI.ExactFourier.PositiveGeneration.polynomial_nonzero_open line 284
  33. theorem OAI.ExactFourier.PositiveGeneration.Pattern.zero_iff line 301
  34. theorem OAI.ExactFourier.PositiveGeneration.positive_generation line 307

    Source documentation

    Positive generation, with a common strictly positive number of forward calls.

    theorem positive_generation (A : Matrix α α ℂ) (hA : IsUnit A) (hn : ¬MonomialMatrix A) :
    ∃ h : ℕ,0<h ∧ ∀ H : Matrix α α ℂ,IsUnit H → Pattern A h H := by
…

    Mentions: OAI.ExactFourier.MonomialMatrix, OAI.ExactFourier.PositiveGeneration.Pattern