English
For any α with a ring structure, for any Holor x with shape ds, CPRankMax ds.prod x is an upper bound for x.
Русский
Для кольца α и любого холора x формы ds, CPRankMax ds.prod x является верхней границей для x.
LaTeX
$$$$ CPRankMax \\ ds.prod \\ x $$$$
Lean4
theorem cprankMax_upper_bound [Semiring α] : ∀ {ds}, ∀ x : Holor α ds, CPRankMax ds.prod x
| [], x => cprankMax_nil x
| d :: ds, x =>
by
have h_summands :
∀ i : { x // x ∈ Finset.range d }, CPRankMax ds.prod (unitVec d i.1 ⊗ slice x i.1 (mem_range.1 i.2)) := fun i =>
cprankMax_mul _ _ _ (cprankMax_upper_bound (slice x i.1 (mem_range.1 i.2)))
have h_dds_prod : (List.cons d ds).prod = Finset.card (Finset.range d) * prod ds := by simp [Finset.card_range]
have :
CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
(∑ i ∈ Finset.attach (Finset.range d), unitVec d i.val ⊗ slice x i.val (mem_range.1 i.2)) :=
cprankMax_sum (Finset.range d).attach _ fun i _ => h_summands i
have h_cprankMax_sum :
CPRankMax (Finset.card (Finset.range d) * prod ds)
(∑ i ∈ Finset.attach (Finset.range d), unitVec d i.val ⊗ slice x i.val (mem_range.1 i.2)) :=
by rwa [Finset.card_attach] at this
rw [← sum_unitVec_mul_slice x]
rw [h_dds_prod]
exact h_cprankMax_sum
