OAI/Algebra/DepthFive/ImmFockMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.immPathAmplitude line 14

   Source documentation

   The normalized coefficient contributed by one endpoint path of IMM.

   def immPathAmplitude (n : ℕ) (hn : 0 < n)
       (isV : (Fin n × Fin n × Fin n) → Bool)
       (d : (Fin n × Fin n × Fin n) →₀ ℕ) (p : Fin (immPaths n hn).length) : ℝ :=
   …

   Mentions: OAI.Problem335.immPaths

2. def OAI.Problem335.immPathOccupation line 20

   Source documentation

   The final occupation vector of one path operator.

   def immPathOccupation (n : ℕ) (hn : 0 < n)
       (isV : (Fin n × Fin n × Fin n) → Bool)
       (d : (Fin n × Fin n × Fin n) →₀ ℕ) (p : Fin (immPaths n hn).length) :
       (Fin n × Fin n × Fin n) →₀ ℕ :=
   …

   Mentions: OAI.Problem335.immPaths

3. theorem OAI.Problem335.immPathAmplitude_nonneg line 26
4. theorem OAI.Problem335.mixedOperator_imm_complexFockMonomial line 36

   Source documentation

   The actual IMM operator on a normalized monomial is the sum of its sparse path actions.

   theorem mixedOperator_imm_complexFockMonomial (n : ℕ) (hn : 0 < n)
       (isV : (Fin n × Fin n × Fin n) → Bool)
       (d : (Fin n × Fin n × Fin n) →₀ ℕ) :
       mixedOperator isV (imm ℂ n) (complexFockMonomial d) =
         ∑ p : Fin (immPaths n hn).length,
           (immPathAmplitude n hn isV d p : ℂ) •
             complexFockMonomial (immPathOccupation n hn isV d p) := by
   …

   Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.imm, OAI.Problem335.complexFockMonomial, OAI.Problem335.immPaths, OAI.Problem335.immPathAmplitude, OAI.Problem335.immPathOccupation

5. theorem OAI.Problem335.complexFockBasis_repr_mixedOperator_imm line 52

   Source documentation

   Normalized matrix entries of the actual IMM operator are weighted path-shift counts.

   theorem complexFockBasis_repr_mixedOperator_imm (n : ℕ) (hn : 0 < n)
       (isV : (Fin n × Fin n × Fin n) → Bool)
       (d e : (Fin n × Fin n × Fin n) →₀ ℕ) :
       complexFockBasis.repr (mixedOperator isV (imm ℂ n) (complexFockMonomial d)) e =
         ∑ p : Fin (immPaths n hn).length,
           if immPathOccupation n hn isV d p = e then (immPathAmplitude n hn isV d p : ℂ)
           else 0 := by
   …

   Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.imm, OAI.Problem335.complexFockMonomial, OAI.Problem335.immPaths, OAI.Problem335.immPathOccupation, OAI.Problem335.immPathAmplitude

6. theorem OAI.Problem335.variable_list_product_isWeightedHomogeneous line 68

   Source documentation

   A product of variables has the sum of their assigned weighted degrees.

   theorem variable_list_product_isWeightedHomogeneous {K σ M : Type*}
       [CommSemiring K] [AddCommMonoid M] (w : σ → M) (l : List σ) :
       ((l.map (MvPolynomial.X : σ → MvPolynomial σ K)).prod).IsWeightedHomogeneous
         w (l.map w).sum := by
   …

7. theorem OAI.Problem335.immPath_product_mem_bidegreeSubmodule line 79

   Source documentation

   The path monomials all have the same layerwise bidegree as IMM.

   theorem immPath_product_mem_bidegreeSubmodule (K : Type*) [CommSemiring K]
       (n : ℕ) (hn : 0 < n) (side : Fin n → Bool)
       (p : Fin (immPaths n hn).length) :
       ((((immPaths n hn).get p).map (MvPolynomial.X (R := K))).prod) ∈
   …

   Mentions: OAI.Problem335.immPaths

8. theorem OAI.Problem335.weight_eq_of_complexFockMonomial_smul_mem line 108

   Source documentation

   A nonzero scalar multiple of a normalized monomial determines its weighted degree.

   theorem weight_eq_of_complexFockMonomial_smul_mem {σ M : Type*}
       [Fintype σ] [DecidableEq σ] [AddCommMonoid M]
       (w : σ → M) (d : σ →₀ ℕ) (a : M) (c : ℂ) (hc : c ≠ 0)
       (h : (c • complexFockMonomial d).IsWeightedHomogeneous w a) :
       Finsupp.weight w d = a := by
   …

   Mentions: OAI.Problem335.complexFockMonomial

9. theorem OAI.Problem335.immPathOccupation_bidegree_of_amplitude_ne_zero line 120

   Source documentation

   A nonzero path amplitude guarantees that its occupation lies in the genuine target bidegree.

   theorem immPathOccupation_bidegree_of_amplitude_ne_zero (n : ℕ) (hn : 0 < n)
       (side : Fin n → Bool) (a b : ℕ)
       (d : (Fin n × Fin n × Fin n) →₀ ℕ)
       (hd : Finsupp.weight (bidegreeWeight (fun x => side x.1)) d = (a, b))
       (p : Fin (immPaths n hn).length)
       (hp : immPathAmplitude n hn (fun x => side x.1) d p ≠ 0) :
       Finsupp.weight (bidegreeWeight (fun x => side x.1))
           (immPathOccupation n hn (fun x => side x.1) d p) =
         (a - (Finset.univ.filter (fun t => side t = true)).card,
          b + (Finset.univ.filter (fun t => side t = false)).card) := by
   …

   Mentions: OAI.Problem335.bidegreeWeight, OAI.Problem335.immPaths, OAI.Problem335.immPathAmplitude, OAI.Problem335.immPathOccupation

10. theorem OAI.Problem335.immPathAmplitude_sq line 149

    Source documentation

    Squared path amplitudes are the occupation monomials occurring in the moment calculation.

    theorem immPathAmplitude_sq (n : ℕ) (hn : 0 < n)
        (isV : (Fin n × Fin n × Fin n) → Bool)
        (d : (Fin n × Fin n × Fin n) →₀ ℕ) (p : Fin (immPaths n hn).length) :
        (immPathAmplitude n hn isV d p) ^ 2 =
          (((immPaths n hn).get p).map
            (fun i => if isV i then (d i : ℝ) else (d i : ℝ) + 1)).prod :=
    …

    Mentions: OAI.Problem335.immPaths, OAI.Problem335.immPathAmplitude