ScaledWordLeaves.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Selected prime factors through every actual ancestor substitution

def OAI.Ostmann.wordLeafScale line 11
theorem OAI.Ostmann.wordLeaf_reconstruct line 18
theorem OAI.Ostmann.wordLeafScale_leaf line 29
theorem OAI.Ostmann.wordLeafScale_outside line 36

theorem OAI.Ostmann.reverseCopyLabelMap_wordLeafScale line 44

Source documentation

The inserted pivot is unchanged; only its original selected leaves scale.

theorem reverseCopyLabelMap_wordLeafScale {I A : Type*} [Mul A]
    (role : I → CopyScheduleRole) (i : I) (hi : role i = .word) (n : ℕ)
    (b : Bool) (P : A) (base : CopyScheduleAtoms role (n + 1) → A)
    (x : TreeLeafIndex (n + 1) → A) :
    reverseCopyLabelMap role n b P (wordLeafScale role i hi (n + 1) base x) =
      wordLeafScale role i hi n (reverseCopyLabelMap role n b P base)
        (fun t => x (if b then .inl t else .inr t)) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.reverseCopyLabelMap, OAI.Ostmann.wordLeafScale

def OAI.Ostmann.descendLeafValues line 64

theorem OAI.Ostmann.descendAtomValues_wordLeafScale line 71

Source documentation

Unexposed prime factors follow precisely their own branches.

theorem descendAtomValues_wordLeafScale {I A : Type*} [Mul A]
    (role : I → CopyScheduleRole) (i : I) (hi : role i = .word)
    (h n d : ℕ) (path : Fin h → Bool) (p : ℕ → A)
    (base : CopyScheduleAtoms role (n + h) → A) (x : TreeLeafIndex (n + h) → A) :
    descendAtomValues role h n d path p (wordLeafScale role i hi (n + h) base x) =
      wordLeafScale role i hi n (descendAtomValues role h n d path p base)
        (descendLeafValues h n path x) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.descendAtomValues, OAI.Ostmann.wordLeafScale, OAI.Ostmann.descendLeafValues

theorem OAI.Ostmann.wordLeafScale_H_product line 88

Source documentation

All remaining factors of the composite words stay in the coefficient.

theorem wordLeafScale_H_product {I A : Type*} [Fintype I] [CommMonoid A]
    (role : I → CopyScheduleRole) (i : I) (hi : role i = .word) (n : ℕ) (b : Bool)
    (base : CopyScheduleAtoms role (n + 1) → A) (x : TreeLeafIndex (n + 1) → A) :
    (∏ h : CopyScheduleH role n,
      wordLeafScale role i hi (n + 1) base x ⟨.inl (b, h.val), h.property⟩) =
      (∏ h : CopyScheduleH role n, base ⟨.inl (b, h.val), h.property⟩) *
        ∏ t : TreeLeafIndex n, x (if b then .inl t else .inr t) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.wordLeafScale

theorem OAI.Ostmann.descendAtomValues_H_product line 104

Source documentation

At any internal node the H product has its original fixed/ancestor coefficient times exactly the selected prime product below that child.

theorem descendAtomValues_H_product {I A : Type*} [Fintype I] [CommMonoid A]
    (role : I → CopyScheduleRole) (i : I) (hi : role i = .word)
    (h n d : ℕ) (path : Fin h → Bool) (p : ℕ → A) (b : Bool)
    (base : CopyScheduleAtoms role (n + 1 + h) → A)
    (x : TreeLeafIndex (n + 1 + h) → A) :
    (∏ a : CopyScheduleH role n,
      descendAtomValues role h (n + 1) d path p
        (wordLeafScale role i hi (n + 1 + h) base x) ⟨.inl (b, a.val), a.property⟩) =
      (∏ a : CopyScheduleH role n,
        descendAtomValues role h (n + 1) d path p base ⟨.inl (b, a.val), a.property⟩) *
          ∏ t : TreeLeafIndex n, descendLeafValues h (n + 1) path x
            (if b then .inl t else .inr t) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.descendAtomValues, OAI.Ostmann.wordLeafScale, OAI.Ostmann.descendLeafValues