# Pattern or ForAll statment in Assumptions

I would like to simplify an expression like $$\sum _{i=1}^k \sqrt{a_i^2}$$, with the condition $$\forall _{i\in \mathbb{Z}_{>\, 0}}a_i\in \mathbb{R}_{>\, 0}$$ and with $$k$$ being undefined, which should give the following result $$\sum _{i=1}^k a_i$$.

My best, yet unsuccessful, attempt was the following:

Refine[Sum[Sqrt[a[i]^2], {i, 1, k}], Element[a[__],PositiveReals]]


which doesn't seem to take into account the fact that $$a_i$$ is positive as the result obtained is $$\sum _{i=1}^k |a_i|$$ (with Abs[a[i]]).

I have read (here) that assumptions will work with Element but not with inequalities, so maybe the PositiveReal assumption is split in Element[a[__],Reals] and a[__]>0, with the first statement working properly but the second doesn't?

Here is the code of other tries:

Refine[Sum[Sqrt[a[i]^2], {i, 1, k}], #] & /@ {Element[a[__],
PositiveReals], Element[a[__], Reals], a[__] > 0,
ForAll[i, PositiveIntegers, a[i] > 0]}


I have already looked at similar threads (1,2,3,4) but couldn't find any solution.

EDIT

The question here isn't about the specific function/sum, but rather the formulation of abstract assumptions with arbitrary number of elements.

The assumption a[i] > 0 may be applied, but one problem not mentioned is that inspection of Sum is limited. If we inactivate Sum, it seems to remove some or all of the restrictions and a[i] > 0 can take effect:

Activate@
Refine[Inactivate[Sum[Sqrt[a[i]^2], {i, 1, k}], Sum],
Element[_a, Reals] && a[i] > 0]
(*  Sum[a[i], {i, 1, k}]  *)


However, if the Sum is stored in a variable, you need to evaluate the variable in Inactivate:

s = Sum[Sqrt[a[i]^2], {i, 1, k}];
Activate@
Refine[Inactivate[Evaluate@s, Sum], Element[_a, Reals] && a[i] > 0]
(*  Sum[a[i], {i, 1, k}]   *)

rule = Power[Power[x__, k_Integer], Rational[1, k_Integer]] :> x

Sum[Sqrt[a[i]^2], {i, 1, k}] /. rule


gives $$\sum _{i=1}^k a(i)$$.

EDIT

It has been correctly pointed out that I am using an operation on structure like it is done with pencil and paper. A slightly better pattern where I divide powers.

rule3 = Power[Power[a[i], g_Integer], Rational[1, h_Integer]] :>
Power[a[i], g/h]


Using it with Refine is not necessary. Patterns work on structure as presented in the FullForm output for the expression.

If this doesn't work in the context of your application then please modify and rephrase the question to include more details.

• How 'bout Sum[Sqrt[a[i]^2], {i, 1, k}] // PowerExpand? Oct 18, 2022 at 13:55
• Also Sum[Sqrt[a[i]^4], {i, 1, k}] /. rule returns Sum[Sqrt[a[i]^4], {i, 1, k}] instead of Sum[Sa[i]^2, {i, 1, k}]. Oct 18, 2022 at 13:57
• The question here is not about the specific example (given as a MWE), but more general about the assumptions phrasing for abstract formulations. Oct 18, 2022 at 13:58
• @MichaelE2: The result of Sum[Sqrt[a[i]^2], {i, 1, k}] // PowerExpand is not true in general and this is written in the documentation. Oct 18, 2022 at 14:06
• @Syed Docs: "PowerExpand also converts (a^b)^c to a^(b c), whatever the form of c is....The transformations made by PowerExpand are correct in general only if c is an integer or a and b are positive real numbers." In other words, PowerExpand just does it, and it's up to the user to apply it only when the assumptions are met. (The same applies to your rule.) Oct 18, 2022 at 14:25