Holor.sum_unitVec_mul_slice
theorem Holor.sum_unitVec_mul_slice :
∀ {α : Type} {d : ℕ} {ds : List ℕ} [inst : Ring α] (x : Holor α (d :: ds)),
((Finset.range d).attach.sum fun i => (Holor.unitVec d ↑i).mul (x.slice ↑i ⋯)) = x
The theorem `Holor.sum_unitVec_mul_slice` states that for any type `α` that has a ring structure, any natural number `d`, any list of natural numbers `ds`, and any 'holor' `x` (which is an indexed collection of tensor coefficients defined on a list `d::ds`), the original holor `x` can be recovered by summing up the product of its slices and unit vectors. Specifically, for each index in the range of `d`, we multiply the slice of the holor at that index by the corresponding unit vector and sum these products for all such indices. The resulting sum is equal to the original holor `x`. The unit vector is defined as having 1 at the `j`-th position and zero elsewhere. Slices of a holor are subsections obtained by fixing one of the indices.
More concisely: For any type with a ring structure, any natural number d and list ds, and any holor x indexed on d::ds, x equals the sum of the products of its slices with the corresponding unit vectors.
|
HolorIndex.take.proof_1
theorem HolorIndex.take.proof_1 :
∀ {ds₂ : List ℕ} (ds : List ℕ) (is : HolorIndex (ds ++ ds₂)),
List.Forall₂ (fun x x_1 => x < x_1) (List.take ds.length ↑is) ds
The theorem `HolorIndex.take.proof_1` states that for any two lists of natural numbers `ds` and `ds₂`, and any `HolorIndex` which is formed by appending `ds₂` to `ds`, the sublist retrieved by taking `List.length ds` elements from the `HolorIndex` satisfies the property that each element at position `i` in the sublist is less than the corresponding element at position `i` in the list `ds`. In simpler terms, it says that the elements corresponding to the list `ds` in the `HolorIndex` are less than their counterparts in `ds`.
More concisely: For any lists `ds` and `ds₂`, if `ds` is a prefix of the HolorIndex formed by appending `ds₂` to `ds`, then the first `List.length ds` elements in `ds` are less than or equal to their corresponding elements in the HolorIndex.
|
Holor.slice_eq
theorem Holor.slice_eq : ∀ {α : Type} {d : ℕ} {ds : List ℕ} (x y : Holor α (d :: ds)), x.slice = y.slice → x = y := by
sorry
This theorem states that two holors are equal if all their slices are equal. In more detail, for any type `α` and any list of natural numbers `ds` with a natural number `d` at its head, if we have two holors `x` and `y` of type `Holor α (d :: ds)`, then if the slice function applied to `x` equals the slice function applied to `y`, it implies that `x` is equal to `y`. A holor is an indexed collection of tensor coefficients, and a slice of a holor is a sub-holor obtained by fixing some of the indices.
More concisely: If two holors of the same type and index have equal slices, then they are equal.
|