OAI/Computability/FourierCircuit/PositiveReach.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ExactFourier.PositiveGeneration.Pattern.monomial_right line 10
  2. theorem OAI.ExactFourier.PositiveGeneration.Pattern.mul line 16
  3. def OAI.ExactFourier.PositiveGeneration.Reach line 22
  4. theorem OAI.ExactFourier.PositiveGeneration.Reach.one line 24
  5. theorem OAI.ExactFourier.PositiveGeneration.Reach.monomial line 25
  6. theorem OAI.ExactFourier.PositiveGeneration.Reach.self line 26
  7. theorem OAI.ExactFourier.PositiveGeneration.Reach.mul line 30
  8. theorem OAI.ExactFourier.PositiveGeneration.Reach.unit line 35
  9. def OAI.ExactFourier.PositiveGeneration.directions line 39
  10. def OAI.ExactFourier.PositiveGeneration.tangentSpan line 42
  11. theorem OAI.ExactFourier.PositiveGeneration.direction_mem line 44
  12. theorem OAI.ExactFourier.PositiveGeneration.diagonal_mem line 47
  13. theorem OAI.ExactFourier.PositiveGeneration.tangent_conj line 50
  14. theorem OAI.ExactFourier.PositiveGeneration.tangent_monomial_conj line 61
  15. theorem OAI.ExactFourier.PositiveGeneration.single_diagonal line 75
  16. theorem OAI.ExactFourier.PositiveGeneration.projector_apply line 81
  17. theorem OAI.ExactFourier.PositiveGeneration.tangent_top line 85
  18. def OAI.ExactFourier.PositiveGeneration.conjLinear line 119
  19. def OAI.ExactFourier.PositiveGeneration.diagLinear line 124
  20. def OAI.ExactFourier.PositiveGeneration.diagConj line 129
  21. theorem OAI.ExactFourier.PositiveGeneration.mem_diagConj line 132
  22. inductive OAI.ExactFourier.PositiveGeneration.Chain line 135
  23. theorem OAI.ExactFourier.PositiveGeneration.Chain.reach line 139
  24. theorem OAI.ExactFourier.PositiveGeneration.directions_after_span line 144
  25. theorem OAI.ExactFourier.PositiveGeneration.exists_full_chain line 168
  26. def OAI.ExactFourier.PositiveGeneration.genericPoint line 191
  27. theorem OAI.ExactFourier.PositiveGeneration.generic_mem_open line 193
  28. theorem OAI.ExactFourier.PositiveGeneration.constructible_generic_nhds line 204
  29. theorem OAI.ExactFourier.PositiveGeneration.constructible_contains_basic line 222
  30. theorem OAI.ExactFourier.PositiveGeneration.dominant_open_image line 232

    Source documentation

    A dominant finite-presentation map meets an actual nonempty basic open, not merely its closure. This is the open-image step in positive generation.

    theorem dominant_open_image (f : R →+* S) (hf : f.FinitePresentation)
    (hinj : Function.Injective f) (p : S) (hp : p≠0) :
    ∃ g : R,g≠0 ∧ (PrimeSpectrum.basicOpen g : Set _)⊆
      PrimeSpectrum.comap f '' (PrimeSpectrum.basicOpen p : Set _) := by
…
  31. theorem OAI.ExactFourier.PositiveGeneration.polynomial_hom_finitePresentation line 257
  32. theorem OAI.ExactFourier.PositiveGeneration.maximal_avoiding line 267
  33. theorem OAI.ExactFourier.PositiveGeneration.polynomial_open_image line 279

    Source documentation

    Point-level consequence of Chevalley and the Nullstellensatz.

    theorem polynomial_open_image (f : MvPolynomial ι ℂ →ₐ[ℂ] MvPolynomial κ ℂ)
    (hinj : Function.Injective f) (p : MvPolynomial κ ℂ) (hp : p≠0) :
    ∃ g : MvPolynomial ι ℂ,g≠0 ∧ ∀ y : ι→ℂ,aeval y g≠0 →
      ∃ x : κ→ℂ,aeval x p≠0 ∧ ∀ i,aeval x (f (X i))=y i := by
…
  34. def OAI.ExactFourier.PositiveGeneration.polynomialMap line 323
  35. theorem OAI.ExactFourier.PositiveGeneration.eval_polynomialMap line 326
  36. theorem OAI.ExactFourier.PositiveGeneration.injective_of_submersion line 335

    Source documentation

    A surjective strict derivative certifies dominance, with no dimension reduction or extra algebraic hypotheses.

    theorem injective_of_submersion (f : MvPolynomial ι ℂ →ₐ[ℂ] MvPolynomial κ ℂ)
    (x : κ→ℂ) (d : (κ→ℂ) →L[ℂ] (ι→ℂ))
    (hd : HasStrictFDerivAt (polynomialMap f) d x) (hs : d.range=⊤) :
    Function.Injective f := by
…

    Mentions: OAI.ExactFourier.L, OAI.ExactFourier.PositiveGeneration.polynomialMap