simplifying expressions - Assumptions on unknown functions

I'm trying to do analytic calculations in a quantum mechanic harmonic oscillator basis. Specifically I want to be able to evaluate functions of the many particle density.

I define the following functions: [definitions]

(* Harmonic Oscillator Eigenstate *)
basis[i_, z_] = Pi^(-1/4)/Sqrt[2^i Factorial[i]] Exp[-z^2/2] HermiteH[i, z];
(* Orbital *)

orb[i_, z_] = Sum[c[i, k] basis[k, z], {k, 0, t}];
(* Particle density of one orbital *)
orbitaldens[i_, z_] = Conjugate[orb[i, z]] psi[i, z];
(* Total density *)
dens[z_] = Sum[a[i] orbitaldens[i, z], {i, 1, n}];

To help Mathematica I define some assumptions beforehand: [assumptions]

$Assumptions = Element[z, Reals] && (* Real-space coordinate is real *)
               Element[{n, t}, Integers] && n > 0 && t > 0 && (* Just indices *)
               Element[c[i_, j_], Complexes] && (* Complex state vector *)

               Element[a[i_], Reals]; (* Real filling factor *)

What is the correct way to define assumptions on an unknown function? Here c[i_, j_] should take integers i, and j and return a complex number. a[i_] on the other hand should take on integer i and return a positive real number.

Unfortunately, the evaluation of the definitons takes very long if I include these assumptions. Without them the definitions block takes about a second to evaluate.

However, I need those assumptions, so Mathematica can do useful simplifications. For example Conjugate[orb[i,z]] orb[i,z]//FullSimplify should simplify to Abs[orb[i,z]]^2. But the same should work, if I only apply the complex conjugation to c[i,k] inside orb[i,z], because basis[i,z] is real. So far, this takes too long to evaluate.

Is it possible to speed this whole thing up?

Another problem I found is the codomain of the Factorial The following two expressions do not evaluate to True, neither to False. They just repeat the first parameter of Refine:

Refine[Element[Sqrt[Factorial[i]], Reals], Element[i, Integers] && i > 0]
Refine[Factorial[i] > 0, Element[i, Integers] && i > 0]

In words, the factorial of a positive integer is not necessarily positive.

What is wrong there? I don't see how the factorial of a positive integer could become negative. (In symbolic maths)