OAI/Computability/RationalHitting/QuantumMatrices.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.HahnMatrix.mapCoeff line 12
  2. lemma OAI.RationalHitting.HahnMatrix.coeff_mul_support_superset line 19
  3. def OAI.RationalHitting.HahnMatrix.entry line 39
  4. lemma OAI.RationalHitting.HahnMatrix.entry_coeff line 42
  5. lemma OAI.RationalHitting.HahnMatrix.entry_support line 47
  6. def OAI.RationalHitting.HahnMatrix.split line 56
  7. lemma OAI.RationalHitting.HahnMatrix.split_injective line 74
  8. def OAI.RationalHitting.HahnMatrix.scalarSeries line 82

    Source documentation

    Scalar series embedded as scalar matrices at each coefficient.

    def scalarSeries : HahnSeries Γ K →+* HahnSeries Γ (Matrix ι ι K) :=
…
  9. lemma OAI.RationalHitting.HahnMatrix.split_scalarSeries line 85
  10. lemma OAI.RationalHitting.HahnMatrix.scalarSeries_commute line 92
  11. def OAI.RationalHitting.HahnMatrix.seriesAlgebra line 100

    Source documentation

    The natural scalar-series algebra structure, derived through an injective matrix realization rather than assuming commutative matrix coefficients.

    def seriesAlgebra : Algebra (HahnSeries Γ K) (HahnSeries Γ (Matrix ι ι K)) :=
…
  12. def OAI.RationalHitting.QuantumMatrices.weyl line 116

    Source documentation

    The Weyl monomial D^a S^b.

    def weyl (a b : ZMod d) : Matrix (ZMod d) (ZMod d) K :=
…
  13. lemma OAI.RationalHitting.QuantumMatrices.weyl_zero line 119
  14. lemma OAI.RationalHitting.QuantumMatrices.weyl_mul line 124
  15. lemma OAI.RationalHitting.QuantumMatrices.weyl_inverse_right line 142
  16. lemma OAI.RationalHitting.QuantumMatrices.weyl_inverse_left line 149
  17. def OAI.RationalHitting.QuantumMatrices.weylUnit line 156
  18. lemma OAI.RationalHitting.QuantumMatrices.weylUnit_val line 160
  19. lemma OAI.RationalHitting.QuantumMatrices.weylUnit_zero line 162
  20. def OAI.RationalHitting.QuantumMatrices.fourierCoeff line 176
  21. lemma OAI.RationalHitting.QuantumMatrices.orthogonality line 179
  22. theorem OAI.RationalHitting.QuantumMatrices.fourier_reconstruction line 191

    Source documentation

    Fourier inversion on each cyclic matrix diagonal.

    theorem fourier_reconstruction (R : Matrix (ZMod d) (ZMod d) K) :
    (∑ a, ∑ b, fourierCoeff χ R a b • weyl χ a b) = R := by
…

    Mentions: OAI.RationalHitting.QuantumMatrices.fourierCoeff, OAI.RationalHitting.QuantumMatrices.weyl

  23. abbrev OAI.RationalHitting.QuantumLift.Exponents line 239
  24. abbrev OAI.RationalHitting.QuantumLift.Ambient line 240
  25. def OAI.RationalHitting.QuantumLift.monomialUnit line 242
  26. lemma OAI.RationalHitting.QuantumLift.monomialUnit_zero line 245
  27. lemma OAI.RationalHitting.QuantumLift.monomialUnit_mul line 249
  28. abbrev OAI.RationalHitting.QuantumLift.DivisionSubring line 258
  29. instance OAI.RationalHitting.QuantumLift.(instance at line 260) line 260
  30. def OAI.RationalHitting.QuantumLift.lift line 264

    Source documentation

    The Fourier lift as a finite Hahn series.

    def lift (R : Matrix (ZMod d) (ZMod d) K) : Ambient (K := K) (d := d) :=
…

    Mentions: OAI.RationalHitting.QuantumLift.Ambient

  31. lemma OAI.RationalHitting.QuantumLift.lift_mem line 268
  32. def OAI.RationalHitting.QuantumLift.liftD line 278
  33. def OAI.RationalHitting.QuantumLift.representation line 283

    Source documentation

    The representation used in the rank-gap argument. Its coefficient field is a commutative Hahn field; all inversion takes place inside the division subring, never by adjoining arbitrary matrix-field scalars.

    def representation : DivisionSubring χ →+* Matrix (ZMod d) (ZMod d) (HahnSeries Exponents K) :=
…

    Mentions: OAI.RationalHitting.QuantumLift.DivisionSubring, OAI.RationalHitting.QuantumLift.Exponents