ConstituentSelectedProducts.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Selected leaf primes in the literal grouped-atom reversal products

theorem OAI.Ostmann.constituent_H_product line 11
def OAI.Ostmann.wordLeafFixedHProduct line 28
theorem OAI.Ostmann.constituent_wordLeaf_H_product line 33

theorem OAI.Ostmann.constituent_wordLeaf_node_relation line 48

Source documentation

The reversal equation now uses exactly the selected child products and coefficients made only from the fixed remaining prime coordinates.

theorem constituent_wordLeaf_node_relation {I : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (size : I → ℕ)
    (i : Σ a, Fin (size a)) (hi : role i.1 = .word) (n : ℕ)
    (y : WordLeafOutside (fun j : Σ a, Fin (size a) => role j.1) i hi (n + 1) → ℕ)
    (x : TreeLeafIndex (n + 1) → ℕ) (childBound pivotBound : ℕ → ℕ)
    (s v w : ℤ) (P : ℕ)
    (h : ValidTransferNode (scheduleAtomSystem role childBound pivotBound)
      ⟨n + 1, fun a => ((scheduleConstituentWord role size (n + 1) a).map
        (wordLeafAssignment (fun j : Σ a, Fin (size a) => role j.1) i hi (n + 1) y x)).prod⟩
      s v w P) :
    v * ((wordLeafFixedHProduct (fun j : Σ a, Fin (size a) => role j.1) i hi n false y : ℕ) : ℤ) *
        ((∏ t : TreeLeafIndex n, x (.inr t) : ℕ) : ℤ) -
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.WordLeafOutside, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.ValidTransferNode, OAI.Ostmann.scheduleAtomSystem, OAI.Ostmann.scheduleConstituentWord, OAI.Ostmann.wordLeafAssignment, OAI.Ostmann.wordLeafFixedHProduct

theorem OAI.Ostmann.constituent_wordLeaf_coefficient_unit line 68