#] #] ********************* #] http://www.BillHowell.ca/Neural nets/Paper reviews/230120 journal paper review - math only.txt 20Jan2023 initial Assigned : 11Jan2023 Due : 08Feb2023 Bill@BillHowell.ca #] +-----+ #] Setup, ToDos : #] IMPORTANT! For proper alignment of math expressions, view this file in a text editor - UNICODE characters (most modern text editors have this) - constant width font (eg Courier 10) - tabs of 3 spaces each - window width to give >=122 characters - ensure that long text lines "wrap" to a new line. I use the text editor "geany" in Linux, which is my favourite as well as "kwrite". There are many, many others! (gedit,I forget many others- especially those geared to programming). Suggestion : Open a second copy of this file for easy reference while viewing the step-by-step derivations. #24************************24 # Table of Contents, generated on computer with : # $ grep "^#]" "$d_web"'Neural nets/Paper reviews/230120 journal paper review - math only.txt' | sed "s/^#\]/ /" # ********************* http://www.BillHowell.ca/Neural nets/Paper reviews/230120 journal paper review - math only.txt +-----+ Setup, ToDos : IMPORTANT! For proper alignment of math expressions, view this file in a text editor "Howell's Flat Liner Notation" (HFLN) - selected symbols (background information) SYMBOLS and notes "Quick notes" as a reminder to myself : Preliminaries : +-----+ p3c1h0.77 Lemma 4 proof by [contradiction, Tmax derivation] Part 1 - drop p1*V(u)^k1 Part 2 - drop p2*V(u)^k2 06Feb2023 p3c2h0.9 Integrating (2.11) from t_bar to t, using t_bar ~= t0 05Feb2023 Overall conclusions regarding Lemma 4 Proof #24************************24 #] "Howell's Flat Liner Notation" (HFLN) - selected symbols (background information) $ find "$d_web" -type f \( -name "*.txt" \) -maxdepth 3 | grep --invert-match "z_Old" | grep --invert-match "z_Archive" | sort | tr \\n \\0 | xargs -0 -IFILE grep --with-filename --line-number -i 'flatliner' "FILE" | sed "s|$d_web||;s|:.*||" | sort -u >"$d_temp"'find-grep-sed temp.txt' >> Lucas/context/Howell - Variables, notations, styles for Bill Lucas, Universal Force.txt +-----+ Notations for [indexing, inequalities, super, sub]-script, calculus, series [sums, products]] Indexing : yi y(i), simple concatenation (might be confused with y*i) y(i+1) array type notation Note the more clear & easy to read indexing used in this review for mixing indexes and t or other variables ... example ai(t) -> a(i,t) Inequalities (for faster typing, symbolic processing) ≤ <= ≥ >= ≠ != +-----+ Calculus notations : d[dt: x] total derivative of x with respect to t dp[dt: x] partial derivative of x with respect to t d^n[dt^n: x] nth total derivative of x with respect to t dp^n[dt^n: x] nth partial derivative of x with respect to t ∫[ds: f] indefinite integral of f with respect to s ∫[ds, a to b: f] definite integral of f with respect to s, from a to b ∮[ds: f(t)] integral of f(t) over the closed [2D curve, 3D surface] S ∮[dl: f(l)] closed-loop integral f(l) wrt dl (pathway) ∮[dl: f(l)] closed-loop integral with dot product of integranddl (eg in Green's theorem etc) +-----+ Other : sum[i=1 to n: f(n,t)] sum of a series LHS = Left-Hand Side of equation double [parenthesis, bracket, brace]s are sometimes used to clearly delimit sub-expressions #24************************24 #] SYMBOLS and notes I did not create a list of the symbols, as per some of my past math checks... Quick notes and reminders for the reviewer The following notes were made to help focus my reviewer work, but have no effect on review results : p4c1h0.7 Remark 2 "... Letting M (t) ≡ 0, (2.4) will reduce to (2.2) in [21]. ..." (2.4) V̇(u) ≤ M(t)*V(u) - p1*V(u)^k1 - p2*V(u)^k2, u ∈ Rn \{0}, for M(t)=0, reduces to [21] and [4] : V̇(u) ≤ - p1*V(u)^k1 - p2*V(u)^k2, u ∈ Rn \{0}, (2.2) from [21] A,B > 0, 0 < K < 1 < H as in this paper p1,p2 > 0, 0 < k1 < 1 < k2 >> so the statement is correct p4c2h0.18 Consider the following discontinuous RDCGNNs: (2.13) dp[dt: u_i(t, R) = sum(k=1 to l: c_ik*dp[d(R^2): u_i(t, R_k)]) - a_i(t)*[ b_i(t)*u_i(t, R) - - sum(j=1 to n: h_ij(t)*f_j(u_j(t, R))) - sum(j=1 to n: l_ij(t)*f_j(u_j(t - σ_ij(t), R))) ] + I_i(t) p5c1h0.51 σ_ij(s) = c*σ_ij(t), at time t and t - σ_ij(t) respectively p4c2h0.48 σ_ij(t) is the discrete time-varying delay at time t >> note on t -> s transitions as reviewer reminder p5c1h0.40 "Let u_i(t, R) = z_i(s), s = R + c*t, be the solution of (2.13), and let σ_ovr_ij(s) = c*σij(t), where c ∈ R and c <> 0. Then (2.13) is transformed into the following form : " (3.1) c*ż_i(s) = sum(k=1 to l: c_ik*z̈_i(s) - a_ovr_i(s) *[ b_ovr_i(s)*z_i(s) - sum(j=1 to n: h_ovr_ij(s)*f_j(z_j(s)) ) - sum(j=1 to n: l_ovr_ij(s)*f_j(z_j(s - σ_ovr_ij(s)))) + I_ovr_i(s) where z_ovr_i(s) = z_i*((s-R)/c), z ∈ [a,b,h,l,I] #24************************24 #] "Quick notes" as a reminder to myself : p4c2h0.18 Consider the following discontinuous RDCGNNs: (2.13) dp[dt: u_i(t, R) = sum(k=1 to l: c_ik*dp[d(R^2): u_i(t, R_k)]) - a_i(t)*[ b_i(t)*u_i(t, R) - - sum(j=1 to n: h_ij(t)*f_j(u_j(t, R))) - sum(j=1 to n: l_ij(t)*f_j(u_j(t - σ_ij(t), R))) ] + I_i(t) p5c1h0.51 σ_ij(s) = c*σ_ij(t), at time t and t - σ_ij(t) respectively p4c2h0.48 σ_ij(t) is the discrete time-varying delay at time t >> note on t -> s transitions as reviewer reminder p5c1h0.40 "Let u_i(t, R) = z_i(s), s = R + c*t, be the solution of (2.13), and let σ_ovr_ij(s) = c*σij(t), where c ∈ R and c <> 0. Then (2.13) is transformed into the following form : " (3.1) c*ż_i(s) = + sum(k=1 to l: c_ik*z̈_i(s) - a_ovr_i(s) * [ b_ovr_i(s)*z_i(s) - sum(j=1 to n: h_ovr_ij(s)*f_j(z_j(s)) ) - sum(j=1 to n: l_ovr_ij(s)*f_j(z_j(s - σ_ovr_ij(s)))) ] + I_ovr_i(s) where z_ovr_i(s) = z_i*((s-R)/c), z ∈ [a,b,h,l,I] 08********08 Step-by-step re-derivation of Lemma 4 Lemma 4 is very important, as it starts to break the ~150? year [Hamilton, Lyapunov-Krasovskii] assumption that d[dt: V(t)] is negative (convex)? >>c to check later #24************************24 #] Preliminaries : Lemma 3 given u(t) != 0, 0 < [d,A,B], 0 < K < 1 < H (2.3) d[dt: V(u)] <= d*V(u) - A*V(u)^H - B*V(u)^K Assume that V : R^n → R+ ∪{0} is C-regular, and there are an indefinite function M (t) and constants p1 > 0, p2 > 0, such that for a.e. t > t0 , where 0 < k1 < 1 < k2, and M(t) satisfies (2.4) d[dt: V(u)] <= M(t)*V(u) - p1*V(u)^k1 - p2*V(u)^k2, u ∈ Rn \{0}, (2.5) ∫[dv: 0 to +∞: M_hat(v)*dv] < α1 where M_hat(v) = max{M(v), 0} (constant >= 0 over interval) (2.6) ∫[ds: 0 to +∞: M(s)*ds] <= -μ(t - t0) + α2, , t > t0, where μ, α1 and α2 are positive constants. p3c1h0.8 Tmax = + 1/{p2*(k2 - 1)} + ln( μ/p1 + e^{(k1 - 1)*α2} + (1 - k1)*α2 ) / (μ*(1 - k1) #24************************24 #] +-----+ #] p3c1h0.77 Lemma 4 proof by [contradiction, Tmax derivation] Proof: Assume that there is a t > 0 such that p3c1h0.8 V(u(t)) ≤ 1 p3c1h0.85 t_bar <= t0 + 1/(p2*(k2 - 1)) = T1 If not, let V(u(t)) > 1, ∀t ∈ [t0, T1], then we can get V(z(T1)) > 1 (counter result to disprove) >> note that z is not [defined, used] until p4c2h0.0 The authors make the assumption that V(z(T1)) > 1, then proceed to show contradictions. They then drop consecutively the [p1*V(u)^k1, p2*V(u)^k2] terms, and for each show : - p1*V(u)^k1 -> a contradiction - p2*V(u)^k2 -> Tmax expression #24************************24 #] Part 1 - drop p1*V(u)^k1 p3c1h0.98 d[dt: V(u)] <= M(t) *V(u) - p1*V(u)^k1 - p2*V(u)^k2 <= M_hat(t)*V(u) - p2*V(u)^k2 >> This is permissible as BOTH [p1*V(u)^k1, p2*V(u)^k2] are positive, because p1,p2 > 0 from (2.2) conditions V(z(T1)) > 1 is an assumption in contradiction V(u(t)) is not otherwise constrained within the proof 0 < k1 < 1 < k2 has no effect here +--> p3c1h0.98 looking to find expression for : d[dt: V(u)] <= M_hat(t)*V(u) - p2*V(u)^k2 p3c2h0.0 Let Y(t) = V(u(t))^(1 - k2) (r2.8.1) d[dt: Y(t)] = d[dt: V(u(t))^(1 - k2)] = (1 - k2)*V(u(t))^(-k2) *d[dt: V(u(t))] (power rule) = (1 - k2)*V(u(t))^(1 - k2)/V(u(t)) *d[dt: V(u(t))] = (1 - k2)*Y(t) /V(u(t)) *d[dt: V(u(t))] <= (1 - k2)*Y(t) /V(u(t)) *{ M_hat(t)*V(u) - p2*V(u)^k2 } <= (1 - k2)*Y(t) *{ M_hat(t) - p2*V(u)^(k2 - 1) } <= (1 - k2)*{ M_hat(t)*Y(t) - p2*V(u)^(k2 - 1)*Y(t) } but V(u(t))^(k2 - 1)*Y(t) = V(u(t))^(k2 - 1)*V(u(t))^(1 - k2) = 1 so (r2.8.2) d[dt: Y(t)] <= (1 - k2)*{ M_hat(t)*Y(t) - p2 } This is the same as the authors' result : ( 2.8 ) d[dt: Y(t)] ≤ (1 - k2)*[ M_hat(t)*Y(t) - p2 ] >> so (2.8) is confirmed +-----+ Let eTrm(t) = e^{ -(1 - k2)*∫[ds, t0 to t: M_hat(s)] } check : Multiplying (2.8) by eTrm(t) (r2.9.1) d[dt: Y(t)] *e^{ -(1 - k2)*∫[ds, t0 to t: M_hat(s)] } <= (1 - k2)*[ M_hat(t)*Y(t) - p2 ] *e^{ -(1 - k2)*∫[ds, t0 to t: M_hat(s)] } +--+ looking at derivative term in LHS of (2.9) : d[dt: Y(t) *eTrm(t)] = + Y(t) *d[dt: eTrm(t)] + d[dt: Y(t)] *eTrm(t) from (2.8), use t for s <= + Y(t) * -(1 - k2)* M_hat(t) *eTrm(t) + (1 - k2)*[ M_hat(t)*Y(t) - p2 ] *eTrm(t) rearrange d[dt: Y(t)*eTrm(t)] / (1 - k2) <= - Y(t) * M_hat(t) *eTrm(t) + [ M_hat(t)*Y(t) - p2 ] *eTrm(t) <= Y(t)*M_hat(t)*eTrm(t) * (-1 + 1) -p2*eTrm(t) <= -p2*eTrm(t) Full form (r2.9.3) d[dt: Y(t)*e^{ -(1 - k2)*∫[ds, t0 to t: M_hat(s)] } ] / (1 - k2) <= -p2 *e^{ (k2 - 1)*∫[ds, t0 to t: M_hat(s)] } This is the same as the authors' result : ( 2.9 ) d[dt: Y(t)*e^{ -(1 - k2)*∫[ds, t0 to t: M_hat(s)] } ] / (1 - k2) <= -p2 *e^{ (k2 - 1)*∫[ds, t0 to t: M_hat(s)] } >> so (2.9) is confirmed +--+ p3c2h0.2 Integrate (2.9) from t0 to T1 ( 2.9 ) d[dt: Y(t)*e^{ -(1 - k2)*∫[ds, t0 to t: M_hat(s)] } ] / (1 - k2) <= -p2 *e^{ (k2 - 1)*∫[ds, t0 to t: M_hat(s)] } so (r2.9.10) ∫[ds, t0 to T1: d[dt: Y(t)*e^{ -(1 - k2)*∫[ds, t0 to t: M_hat(s)] } ] / (1 - k2)] <= ∫[ds, t0 to T1: -p2 *e^{ (k2 - 1)*∫[ds, t0 to t: M_hat(s)] } ] <= -p2 * ∫[ds, t0 to T1: e^{ (k2 - 1)*∫[ds, t0 to t: M_hat(s)] } ] looking at LHS of (r2.9.10) : (r2.9.11) ∫[ds, t0 to T1: d[dt: Y(t)*e^{ -(1 - k2)*∫[ds, t0 to t: M_hat(s)] } ] / (1 - k2)] = ( Y(T1)*e^{ -(1 - k2)*∫[ds, t0 to T1: M_hat(s)] } - Y(t0)*e^{ -(1 - k2)*∫[ds, t0 to t0: M_hat(s)] } ) / (1 - k2) but ∫[ds, t0 to t0: M_hat(s)] -> is zero as bounds (upper=lower) so 1 = e^{ -(1 - k2)*∫[ds, t0 to t0: M_hat(s)] } (r2.9.12) ∫[ds, t0 to T1: d[dt: Y(t)*e^{ -(1 - k2)*∫[ds, t0 to t: M_hat(s)] } ] / (1 - k2)] = ( Y(T1)*e^{ -(1 - k2)*∫[ds, t0 to T1: M_hat(s)] } - Y(t0) ) / (1 - k2) p3c2h0.25 this is the same as the authors' LHS ( Y(T1)*e^{ -(1 - k2)*∫[dv, t0 to T1: M_hat(v)] } - Y(t0) ) / (1 - k2) simplified ( Y(T1)*eTrm(T1) - Y(t0)) / (1 - k2) looking at RHS of (r2.9.10) : (r2.9.15) ∫[ds, t0 to T1: -p2* e^{(k2 - 1)*∫[ds, t0 to t: M_hat(s)] } ] = -p2* ∫[ds, t0 to T1: e^{(k2 - 1)*∫[ds, t0 to t: M_hat(s)] } ] looking at (2.5) ∫[dv: 0 to +∞: M_hat(v)*dv] < α1 where M_hat(v) = max{M(v), 0} (constant >= 0 over interval) By this definition the integral of (t0 to t) <= integral of (0 to +∞) continuing ∫[ds, t0 to T1: -p2* e^{(k2 - 1)*∫[ds, t0 to t: M_hat(s)] } ] <= -p2* ∫[ds, t0 to T1: e^{(k2 - 1)*α1} ] but e^{ (k2 - 1)*α1} is a constant, therefore (r2.9.16) ∫[ds, t0 to T1: -p2* e^{(k2 - 1)*∫[ds, t0 to t: M_hat(s)] } ] <= -p2 *e^{(k2 - 1)*α1} * ∫[ds, t0 to T1: 1 ] <= -p2 *e^{(k2 - 1)*α1} *(T1 - t0) p3c2h0.33 this is the same as the authors' RHS <= -p2 *e^{(k2 - 1)*α1} *(T1 - t0) Full form (r2.9.20) ( Y(T1)*eTrm(T1) - Y(t0) ) / (1 - k2) <= -p2 *e^{(k2 - 1)*α1} *(T1 - t0) This is the same as the authors' result : p3c2h0.33 ( Y(T1)*eTrm(T1) - Y(t0) ) / (1 - k2) <= -p2 *e^{(k2 - 1)*α1} *(T1 - t0) or exanding eTrm(T1) p3c2h0.33 ( Y(T1)*e^{ -(1 - k2)*∫[dv, t0 to T1: M_hat(v)] } - Y(t0)) / (1 - k2) <= -p2 *e^{(k2 - 1)*α1 }* (T1 - t0) >> so p3c2h0.33 is confirmed +--+ p3c2h0.45 Thus, we further get Note that the RHS of p3c2h0.45 has not changed, and we are looking for a more compact version of the LHS. (r2.9.20) ( Y(T1)*eTrm(T1) - Y(t0) ) / (1 - k2) <= -p2 *e^{(k2 - 1)*α1} *(T1 - t0) LHS (r2.9.25) ( Y(T1)*eTrm(T1) - Y(t0) ) / (1 - k2) = ( Y(T1)*e^{ -(1 - k2)*∫[dv, t0 to T1: M_hat(v)] } - Y(t0)) / (1 - k2) >> this is the same as the 3rd line (2nd inequality) p3c2h0.6 note that from (2.5) ∫[dv, t0 to T1: M_hat(v)] < α1 (r2.9.26) ( Y(T1)*eTrm(T1) - Y(t0) ) / (1 - k2) = ( Y(T1)*e^{ -(1 - k2)*∫[dv, t0 to T1: M_hat(v)] } - Y(t0)) / (1 - k2) >= ( Y(T1)*e^{ -(1 - k2)*α1 } - Y(t0)) / (1 - k2) note that >= applies above as α1 is a positive constant so exponential is smaller +ve finally for LHS >= Y(T1)*e^{ -(1 - k2)*α1 } / (1 - k2) p3c2h0.5 Full expression from LHS (r2.9.26), RHS of (r2.9.20) (r2.9.27) Y(T1)*e^{ -(1 - k2)*α1 } / (1 - k2) <= -p2 *e^{(k2 - 1)*α1} *(T1 - t0) This is the same as the authors' result : p3c2h0.45 Y(T1)*e^{ -(1 - k2)*α1 } / (1 - k2) <= -p2 *e^{(k2 - 1)*α1} *(T1 - t0) >> so p3c2h0.33 is confirmed #24************************24 #] Part 2 - drop p2*V(u)^k2 This part is very similar to Part 1, using the following symbol exchanges : From Y(t), k2, p2, M_hat(t), ∫[ds, t0 to t: M_hat(s)], ∫[ds, t0 to T1: M_hat(s)] To X(t), k1, p1, M(t), ∫[ds, t_bar to t: M(s)], ∫[dv, t_bar to s: M(v)], also : From eTrm(t) = e^{ -(1 - k2)*∫[ds, t0 to t: M_hat(s)] } To eTrm2(t) = e^{ -(1 - k1)*∫[ds, t0 to t: M(s) ] } I simply copied Part 1 to a separate file, made the simple substitutions, then fixed linePositions (eg p3c2h0.75), equation numbers, etc. Howeverm there are bound to be errors in Part 2 below partially due to this simple conversion. As for Part 1, on the other hand, since p2 > 0, from (2.4), it gives p3c2h0.75 d[dt: V(u)] <= M(t) *V(u) - p1*V(u)^k1 - p1*V(u)^k1 <= M(t)* V(u) - p1*V(u)^k1 >> This is permissible as BOTH [p1*V(u)^k1, p1*V(u)^k1] are positive, because p1,p1 > 0 from (2.2) conditions V(z(T1)) > 1 is an assumption in contradiction V(u(t)) is not otherwise constrained within the proof 0 < k1 < 1 < k1 has no effect here +-----+ p3c2h0.70 X(t) = V(u(t))^(1 - k1) p3c2h0.75 looking to find expression for : d[dt: V(u)] <= M(t)*V(u) - p1*V(u)^k1 p3c2h0.8 Let X(t) = V(u(t))^(1 - k1) (r2.10.1) d[dt: X(t)] = d[dt: V(u(t))^(1 - k1)] = (1 - k1)*V(u(t))^(-k1) *d[dt: V(u(t))] (power rule) = (1 - k1)*V(u(t))^(1 - k1)/V(u(t)) *d[dt: V(u(t))] = (1 - k1)*X(t) /V(u(t)) *d[dt: V(u(t))] <= (1 - k1)*X(t) /V(u(t)) *{ M(t)*V(u) - p1*V(u)^k1 } <= (1 - k1)*X(t) *{ M(t) - p1*V(u)^(k1 - 1) } <= (1 - k1)*{ M(t)*X(t) - p1*V(u)^(k1 - 1)*X(t) } but V(u(t))^(k1 - 1)*X(t) = V(u(t))^(k1 - 1)*V(u(t))^(1 - k1) = 1 so (r2.10.2) d[dt: X(t)] <= (1 - k1)*{ M(t)*X(t) - p1 } This is the same as the authors' result : ( 2.10 ) d[dt: X(t)] ≤ (1 - k1)*[ M(t)*X(t) - p1 ] >> so (2.10) is confirmed >> result is very similar to Part 1 with symbol changes +-----+ Let eTrm2(t) = e^{ -(1 - k1)*∫[ds, t_bar to t: M(s)] } check : Multiplying (2.10) by eTrm2(t) (r2.11.1) d[dt: X(t)] *e^{ -(1 - k1)*∫[ds, t_bar to t: M(s)] } <= (1 - k1)*[ M(t)*X(t) - p1 ] *e^{ -(1 - k1)*∫[ds, t_bar to t: M(s)] } +--+ looking at derivative term in LHS of (2.11) : d[dt: X(t) *eTrm2(t)] = + X(t) *d[dt: eTrm2(t)] + d[dt: X(t)] *eTrm2(t) from (2.10), use t for s <= + X(t) * -(1 - k1)* M(t) *eTrm2(t) + (1 - k1)*[ M(t)*X(t) - p1 ] *eTrm2(t) rearrange d[dt: X(t)*eTrm2(t)] / (1 - k1) <= - X(t) * M(t) *eTrm2(t) + [ M(t)*X(t) - p1 ]*eTrm2(t) <= X(t) *M(t) *eTrm2(t) * (-1 + 1) -p1*eTrm2(t) <= -p1*eTrm2(t) Full form (r2.11.3) d[dt: X(t)*e^{ -(1 - k1)*∫[ds, t_bar to t: M(s)] } ] / (1 - k1) <= -p1 *e^{ (k1 - 1)*∫[ds, t_bar to t: M(s)] } This is the same as the authors' result : ( 2.11 ) d[dt: X(t)*e^{ -(1 - k1)*∫[ds, t_bar to t: M(s)] } ] / (1 - k1) <= -p1 *e^{ (k1 - 1)*∫[ds, t_bar to t: M(s)] } >> so (2.11) is confirmed >> result is very similar to Part 1 with symbol changes +--+ #] 06Feb2023 p3c2h0.9 Integrating (2.11) from t_bar to t, using t_bar ~= t0 # see 'http://www.BillHowell.ca/Neural nets/Paper reviews/230120 journal paper review - math discarded scribblings.txt' for using t_bar <= t0 + 1/(p2*(k2 - 1)) p3c2h0.9 Integrating (2.11) from t_bar to t looking at LHS of (2.11) : (r2.11.11) ∫[ds, t_bar to t: d[dt: X(t)*e^{ -(1 - k1)*∫[ds, t_bar to t: M(s)] } ] / (1 - k1)] = ( X(t) *e^{ -(1 - k1)*∫[ds, t_bar to t : M(s)] } - X(t_bar)*e^{ -(1 - k1)*∫[ds, t_bar to t_bar: M(s)] } ) / (1 - k1) but ∫[ds, t_bar to t_bar: M(s)] -> is zero as bounds (upper=lower) so 1 = e^{ -(1 - k1)*∫[ds, t_bar to t_bar: M(s)] } (r2.11.12) ∫[ds, t_bar to t: d[dt: X(t)*e^{ -(1 - k1)*∫[ds, t_bar to t: M(s)] } ] / (1 - k1)] = ( X(t) *e^{ -(1 - k1)*∫[ds, t_bar to t: M(s)] } - X(t_bar) ) / (1 - k1) simplified ( X(t)*eTrm2(t) - X(t_bar)) / (1 - k1) looking at RHS of (2.11) : (r2.11.15) ∫[ds, t_bar to t: -p1* e^{(k1 - 1)*∫[ds, t_bar to t: M(s)] } ] = -p1 *∫[ds, t_bar to t: e^{(k1 - 1)*∫[ds, t_bar to t: M(s)] } ] |--> looking at givens (2.6) ∫[ds, t0 to t: e^{(k1 - 1)*∫[ds, t_bar to t: M(s)] } ] <= - μ*(t - t0) + α2 where t > t0 p3c1h0.85 t_bar <= t0 + 1/(p2*(k2 - 1)) = T1` (r2.11.16) t0 >= t_bar - 1/(p2*(k2 - 1)) >> I don't use this here, I tried it in : '230120 journal paper review - math discarded scribblings.txt' HOWEVER, here I will try (r2.6.1) t_bar = t0 <--| combine (r2.6.1) and (r2.11.15) (r2.11.17) -p1 *∫[ds, t_bar to t: e^{(k1 - 1)*∫[ds, t_bar to t: M(s)] } ] <= -p1 *(( μ*(t - t_bar) + α2 )) Let (r2.11.20) eTrm3(t) = e^{(1 - k1) *(( μ*(t - t_bar) - α2 ))} |--> take derivative for subsequent use (r2.11.25) d[dt: eTrm3(t)] = d[dt: e^{(1 - k1) *( μ*(t - t_bar) - α2 ) } ] = e^{(1 - k1) *( μ*(t - t_bar) - α2 ) } * d[dt: (1 - k1) *( μ*(t_bar - t_bar) - α2 ) ] but d[dt: μ*(t_bar- t_bar)] = 0 (r2.11.26) d[dt: eTrm3(t)] = e^{(1 - k1) * ( μ*(t - t_bar) - α2 ) } >> this is close to the correct functional form p4c1h0.12 <--| |--> integrate eTrm3(t) from (r2.11.20) generic d[dt: e^x(t) ] = e^x(t) *d[dt: x(t) ] therefore ∫[dt, ti to tf: d[ds: e^x(s)] ] = ∫[dt, ti to tf: e^x(t) *d[dt: x(t) ] ] apply this to eTrm3(t) (r2.11.30) ∫[dt, t_bar to t: d[ds: eTrm3(s)] ] = ∫[dt, t_bar to t: eTrm3(t) *d[dt: eTrm3(t)] ] consider LHS of (r2.11.30) (r2.11.35) ∫[dt, t_bar to t: d[ds: eTrm3(s)] ] = eTrm3(t) - eTrm3(t_bar) = ∫[ds, t_bar to t: e^{(1 - k1) *(( μ*(t - t_bar) - α2 ))} ] - ∫[ds, t_bar to t_bar: e^{(1 - k1) *(( μ*(t_bar - t_bar) - α2 ))} ] but as with (r2.11.11), 2nd expression = 0, so = ∫[ds, t_bar to t: e^{(k1 - 1) *(( μ*(t - t_bar) - α2 ))} ] consider RHS of (r2.11.30) (r2.11.38) ∫[dt, t_bar to t: eTrm3(t) *d[dt: eTrm3(t)] ] subbing for d[dt: eTrm3(t)] from (r2.11.26), and eTrm3(t) from (r2.11.20) = ∫[dt, t_bar to t: e^{(1 - k1) *((μ*(t - t_bar) - α2))} *e^{(1 - k1) *((μ*(t - t_bar) - α2))} ] <--| looking again at LHS of (2.11) : (r2.11.11) ∫[ds, t_bar to t: d[dt: X(t)*e^{ -(1 - k1)*∫[ds, t_bar to t: M(s)] } ] / (1 - k1)] (r2.11.12) = (( X(t) *e^{ -(1 - k1)*∫[ds, t_bar to t: M(s)] } - X(t_bar) )) / (1 - k1) simplified = ( X(t)*eTrm2(t) - X(t_bar) ) / (1 - k1) looking again at RHS of (2.11) : (r2.11.15) ∫[ds, t_bar to t: -p1* e^{(k1 - 1)*∫[ds, t_bar to t: M(s)] } ] = -p1 *∫[ds, t_bar to t: e^{(k1 - 1)*∫[ds, t_bar to t: M(s)] } ] (r2.11.17) <= -p1 *(( μ*(t - t_bar) + α2 )) >> note that this causes a problem later as it is NOT an exponential term!! Combine LHS (r2.11.12) & RHS (r2.11.17) to get full form (r2.11.40) ( X(t)*eTrm2(t) - X(t_bar) ) / (1 - k1) <= -p1 *(( μ*(t - t_bar) + α2 )) re-arrange, subbing eTrm2(t) (r2.11.41) X(t) *e^{ - (1 - k1)*∫[ds, t_bar to t: M(s)] } <= X(t_bar) + (1 - k1)*(( -p1*( μ*(t - t_bar) + α2 ) )) <= X(t_bar) - p1*(1 - k1)*(( -( μ*(t - t_bar) + α2 ) )) This is NOT the same as the authors' result : p3c2h0.9 (r2.11.42) X(t) *e^{ - (1 - k1)*∫[ds, t_bar to t: M(s)] } <= X(t_bar) - p1/μ*(( e^{(1 - k1)*( μ*(t - t_bar) - α2)} - e^{-(1 - k1)*α2} )) >> so p3c2h0.33 is NOT confirmed, but as I have run out of time, I suspect that the authors may be right and I have made a mistake. p4c1h0.12 the last expression should be <= rather than = X(t) *e^{ -(1 - k1)*∫[ds, t_bar to t: M(s)] } <= X(t_bar) - p1/μ*(( e^{(1 - k1)*( μ*(t - t_bar) - α2)} - e^{-(1 - k1)*α2} )) >> Actually, the derivative expression (r2.11.17) seems to have been used, rather than the integral eTrm3(t)? +--+ p4c1h0.15 By using the fact (assumption for Proof) p3c1h0.8 V(u(t)) ≤ 1 also, given earlier p3c1h0.5 0 < k1 < 1 < k2 p3c2h0.8 X(t) = V(u(t))^(1 - k1) therefore (r2.12.01) X(t) <= 1 (r2.12.02) X(t_bar) = V(u(t_bar))^(1 - k1) <= 1 using authors' preceding result p4c1h0.12 (r2.11.42) (r2.11.42) X(t) *e^{ -(1 - k1)*∫[ds, t_bar to t: M(s)] } <= X(t_bar) - p1/μ*(( e^{(1 - k1)*( μ*(t - t_bar) - α2)} - e^{-(1 - k1)*α2} )) multiply both sides by *e^{ (1 - k1)*∫[ds, t_bar to t: M(s)] } (r2.12.05) X(t) <= e^{ (1 - k1)*∫[ds, t_bar to t: M(s)] } * {{ X(t_bar) - p1/μ*(( e^{(1 - k1)*( μ*(t - t_bar) - α2)} - e^{-(1 - k1)*α2} )) }} from (r2.12.02), I can substitute 1 for X(t_bar) (r2.12.06) X(t) <= e^{ (1 - k1)*∫[ds, t_bar to t: M(s)] } * {{ 1 - p1/μ*(( e^{(1 - k1)*( μ*(t - t_bar) - α2)} - e^{-(1 - k1)*α2} )) }} <= e^{ (1 - k1)*∫[ds, t_bar to t: M(s)] } * {{ 1 - p1/μ *e^{(1 - k1)*( μ*(t - t_bar) - α2)} + p1/μ*e^{-(1 - k1)*α2} }} This (r2.12.06) is the same as the authors' result : ( 2.12 ) X(t) <= e^{ (1 - k1)*∫[ds, t_bar to t: M(s)] } * {{ 1 - p1/μ *e^{(1 - k1)*( μ*(t - t_bar) - α2)} + p1/μ*e^{-(1 - k1)*α2} }} >> so (2.12) is confirmed IF the derivative term (r2.11.17) is used instead of the expected integral term eTrm3(t). ??? +--+ p4c1h0.35 Since e^{ (1 - k1)*∫[ds, t_bar to t: M(s)] } > 0, in (2.12), we have note : see (2.6) as well, (r2.12.02) REQUIRES a negative RHS (r2.12.10) 1 - p1/μ*e^{(1 - k1)*( μ*(t - t_bar) - α2)} + p1/μ*e^{-(1 - k1)*α2} <= 0 >> confirms that step by inspection +--+ p4c1h0.5 then it implies that V(u(t)) ≡ 0 for all multiply (r2.12.10) by -1, reverse <= to >= then rearrange (r2.12.11) -1 + p1/μ*e^{ (1 - k1)*( μ*(t - t_bar) - α2)} - p1/μ*e^{-(1 - k1)*α2} >= 0 (r2.12.12) e^{ (1 - k1)*( μ*(t - t_bar) - α2)} >= μ/p1 + e^{ (k1 - 1)*α2} take ln of each side (r2.12.13) ln( e^{ (1 - k1)*( μ*(t - t_bar) - α2)} ) >= ln( μ/p1 + e^{ (k1 - 1)*α2} ) (r2.12.14) (1 - k1)*( μ*(t - t_bar) - α2 ) >= ln( μ/p1 + e^{ (k1 - 1)*α2} ) re-arrange, notice (1 - k1)* un front of (r2.12.15) μ*(t - t_bar) >= (( ln( μ/p1 + e^{ (k1 - 1)*α2} ) + (1 - k1)*α2 )) / (1 - k1) (r2.12.16) t - t_bar >= (( ln( μ/p1 + e^{ (k1 - 1)*α2} ) + (1 - k1)*α2 )) / (μ*(1 - k1)) (r2.12.17) t >= t_bar + (( ln( μ/p1 + e^{ (k1 - 1)*α2} ) + (1 - k1)*α2 )) / (μ*(1 - k1)) +--+ p4c1h0.45 Since t ≤ T1, it is valid that V(u(t)) ≡ 0 for all Given assumption : p3c1h0.85 t_bar <= t0 + 1/(p2*(k2 - 1)) ~= T1 then replace t_bar with t0 in (r2.12.17) (r2.12.20) t >= t0 + 1/(p2*(k2 - 1)) + (( ln( μ/p1 + e^{ (k1 - 1)*α2} ) + (1 - k1)*α2 )) / (μ*(1 - k1)) (r2.12.21) t ~= t0 + T_max >> as an approximate relation? +--+ Therefore, the origin of (2.1) can achieve FxT stabilization, and (r2.12.25) T_max = + 1/(p2*(k2 - 1)) + (( ln( μ/p1 + e^{ (k1 - 1)*α2} ) + (1 - k1)*α2 )) / (μ*(1 - k1)) comparing to authors' expression (at p3c1h0.8 and p4c1h0.65) p3c1h0.8 Tmax = + 1/{p2*(k2 - 1)} + (( ln( μ/p1 + e^{ (k1 - 1)*α2} ) + (1 - k1)*α2 )) / (μ*(1 - k1) >> confirms authors' Tmax result for approximate inequality (r2.12.21) #24************************24 #] 05Feb2023 Overall conclusions regarding Lemma 4 Proof >> Given that most (not all) of Parts [1, 2] are confirmed, then the Proof of Lemma 4 is accepted, with the reservations that : (r2.11.17) <= -p1 *(( μ*(t - t_bar) + α2 )) >> note that this causes a problem later as it is NOT an exponential term!! reviewer result (r2.11.41) X(t) *e^{ - (1 - k1)*∫[ds, t_bar to t: M(s)] } <= X(t_bar) - p1*(1 - k1)*(( -( μ*(t - t_bar) + α2 ) )) This is NOT the same as the authors' result : p3c2h0.9 (r2.11.42) X(t) *e^{ - (1 - k1)*∫[ds, t_bar to t: M(s)] } <= X(t_bar) - p1/μ*(( e^{(1 - k1)*( μ*(t - t_bar) - α2)} - e^{-(1 - k1)*α2} )) >> so p3c2h0.33 is NOT confirmed, but as I have run out of time, I suspect that the authors may be right and I have made a mistake. (2.12) is confirmed IF the derivative term (r2.11.17) is used instead of the expected integral term eTrm3(t). ??? 06Feb2023 out of time - have to submit before travelling. # enddoc