FinitePrefixEmbedding.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite sums over embedded prefixes

A function supported on the image of an embedding can be summed over its domain. For an ordered retained-candidate embedding, its natural prefix before a candidate agrees with the prefix of retained nodes before that node.

theorem OAI.ReflexiveFixedPoints.FinitePrefix.sum_univ_supported_embedding line 21

Source documentation

Reindex a finite sum whose summands vanish outside an embedding's image.

theorem sum_univ_supported_embedding {A B : Type*} [Fintype A] [Fintype B]
    (e : A ↪ B) (f : B → M)
    (hf : ∀ b, (¬ ∃ a, e a = b) → f b = 0) :
    (∑ b, f b) = ∑ a, f (e a) := by
…

def OAI.ReflexiveFixedPoints.FinitePrefix.inclusion line 37
Source documentation
The inclusion of an initial finite segment into a larger finite segment.
```
def inclusion {c q : ℕ} (h : q ≤ c) : Fin q ↪ Fin c :=
…
```
theorem OAI.ReflexiveFixedPoints.FinitePrefix.inclusion_apply line 41
theorem OAI.ReflexiveFixedPoints.FinitePrefix.inclusion_val line 45
theorem OAI.ReflexiveFixedPoints.FinitePrefix.sum_prefix_eq_sum_cutoff line 49
Source documentation
An initial-segment sum is a full sum with the complementary summands zeroed.
```
theorem sum_prefix_eq_sum_cutoff {c q : ℕ} (h : q ≤ c) (f : Fin c → M) :
    (∑ i : Fin q, f (inclusion h i)) =
      ∑ j : Fin c, if j.val < q then f j else 0 := by
…
```
Mentions: OAI.ReflexiveFixedPoints.FinitePrefix.inclusion
theorem OAI.ReflexiveFixedPoints.FinitePrefix.sum_prefix_eq_sum_retained line 72
Source documentation
Summing supported candidate data before a retained candidate is exactly summing the retained data before its retained node.
```
theorem sum_prefix_eq_sum_retained {n c : ℕ} (e : Fin n ↪o Fin c)
    (v : Fin n) (f : Fin c → M)
    (hf : ∀ b, (¬ ∃ a, e a = b) → f b = 0) :
    (∑ i : Fin (e v).val, f (inclusion (e v).isLt.le i)) =
      ∑ w : Fin n, if w < v then f (e w) else 0 := by
…
```
Mentions: OAI.ReflexiveFixedPoints.FinitePrefix.inclusion