Proof of the (Subscript[J, uv])-property

Pensieve header: Proof of the $J_{uv}$ property.

SetDirectory["C:\\drorbn\\AcademicPensieve\\2013-04"];
<< CheatSheetJ-Verification.m;
$SeriesCompareDegree = 6;

The (Subscript[J, uv]) equation

(Subscript[J, u])[α]+(β // (Subscript[RC, u])[α] // (Subscript[J, v])// (Subscript[CC, u])[-α]) ≡ (Subscript[J, v])[β]+(α // (Subscript[RC, v])[β] // (Subscript[J, u]) // (Subscript[CC, v])[-β])

The radial α-variation of the (Subscript[J, uv]) equation

Congruent[
(1/ϵ)((Subscript[J, u])[(1+ϵ)α]+(β // (Subscript[RC, u])[(1+ϵ)α] // (Subscript[J, v])// (Subscript[CC, u])[-(1+ϵ)α]) - (Subscript[J, u])[α]-(β // (Subscript[RC, u])[α] // (Subscript[J, v])// (Subscript[CC, u])[-α])),
(1/ϵ)((Subscript[J, v])[β]+((1+ϵ)α // (Subscript[RC, v])[β] // (Subscript[J, u])// (Subscript[CC, v])[-β]) - (Subscript[J, v])[β]-(α // (Subscript[RC, v])[β] // (Subscript[J, u])// (Subscript[CC, v])[-β]))
]

The radial α-variation of the LHS

Congruent[
(1/ϵ)((Subscript[J, u])[(1+ϵ)α]+(β // (Subscript[RC, u])[(1+ϵ)α] // (Subscript[J, v])// (Subscript[CC, u])[-(1+ϵ)α]) - (Subscript[J, u])[α]-(β // (Subscript[RC, u])[α] // (Subscript[J, v])// (Subscript[CC, u])[-α])),
Plus[
α // (Subscript[RC, u])[α] // (Subscript[div, u]) // (Subscript[CC, u])[-α],
β // (Subscript[RC, u])[α] // (Subscript[ad, u])[α // (Subscript[RC, u])[α]] // adSeries[((1-(E^(-ad)))/ad), β // (Subscript[RC, u])[α]] // (Subscript[RC, v])[β // (Subscript[RC, u])[α]] // (Subscript[div, v]) // (Subscript[CC, v])[-β // (Subscript[RC, u])[α]] // (Subscript[CC, u])[-α],
β // (Subscript[RC, u])[α] // (Subscript[J, v]) // (Subscript[ad, u])[-α // (Subscript[RC, u])[α]] // (Subscript[CC, u])[-α]
]
]

The radial α-variation of the RHS

Congruent[
(1/ϵ)((Subscript[J, v])[β]+((1+ϵ)α // (Subscript[RC, v])[β] // (Subscript[J, u])// (Subscript[CC, v])[-β]) - (Subscript[J, v])[β]-(α // (Subscript[RC, v])[β] // (Subscript[J, u])// (Subscript[CC, v])[-β])),
α // (Subscript[RC, v])[β] // (Subscript[RC, u])[α//(Subscript[RC, v])[β]] // (Subscript[div, u]) // (Subscript[CC, u])[-α//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β]
]

The radial α-variation equation

Congruent[Plus[
α // (Subscript[RC, u])[α] // (Subscript[div, u]) // (Subscript[CC, u])[-α],
β // (Subscript[RC, u])[α] // (Subscript[ad, u])[α // (Subscript[RC, u])[α]] // adSeries[((1-(E^(-ad)))/ad), β // (Subscript[RC, u])[α]] // (Subscript[RC, v])[β // (Subscript[RC, u])[α]] // (Subscript[div, v]) // (Subscript[CC, v])[-β // (Subscript[RC, u])[α]] // (Subscript[CC, u])[-α],
β // (Subscript[RC, u])[α] // (Subscript[J, v]) // (Subscript[ad, u])[-α // (Subscript[RC, u])[α]] // (Subscript[CC, u])[-α]
],
α // (Subscript[RC, v])[β] // (Subscript[RC, u])[α//(Subscript[RC, v])[β]] // (Subscript[div, u]) // (Subscript[CC, u])[-α//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β]]

Simplify using (Subscript[C, u])(Subscript[C, v]) and (Subscript[RC, u])(Subscript[RC, v]) and cancel (Subscript[CC, u])[-α] on the right

{(γ  // (Subscript[RC, v])[β] // (Subscript[RC, u])[α//(Subscript[RC, v])[β]]) ≡ (γ  // (Subscript[RC, u])[α] // (Subscript[RC, v])[β//(Subscript[RC, u])[α]]),
(γ  // (Subscript[CC, u])[-α//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β]) ≡ (γ  // (Subscript[CC, v])[-β//(Subscript[RC, u])[α]] // (Subscript[CC, u])[-α])}

Congruent[Plus[
α // (Subscript[RC, u])[α] // (Subscript[div, u]),
β // (Subscript[RC, u])[α] // (Subscript[ad, u])[α // (Subscript[RC, u])[α]] // adSeries[((1-(E^(-ad)))/ad), β // (Subscript[RC, u])[α]] // (Subscript[RC, v])[β // (Subscript[RC, u])[α]] // (Subscript[div, v]) // (Subscript[CC, v])[-β // (Subscript[RC, u])[α]],
β // (Subscript[RC, u])[α] // (Subscript[J, v]) // (Subscript[ad, u])[-α // (Subscript[RC, u])[α]]
],
α // (Subscript[RC, u])[α] // (Subscript[RC, v])[β//(Subscript[RC, u])[α]] // (Subscript[div, u]) // (Subscript[CC, v])[-β//(Subscript[RC, u])[α]]]

Rename α // (Subscript[RC, u])[α]->α and β // (Subscript[RC, u])[α]-> β. The equation below is “Equation Jad” used also in tJ.nb.

Congruent[Plus[
α // (Subscript[div, u]),
β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[CC, v])[-β],
β // (Subscript[J, v]) // (Subscript[ad, u])[-α]
],
α // (Subscript[RC, v])[β] // (Subscript[div, u]) // (Subscript[CC, v])[-β]]

Now take the β-radial variation

Congruent[
(1/ϵ)((α // (Subscript[RC, v])[(1+ϵ)β] // (Subscript[div, u]) // (Subscript[CC, v])[-(1+ϵ)β])-(α // (Subscript[RC, v])[β] // (Subscript[div, u]) // (Subscript[CC, v])[-β])),
Plus[
α // (Subscript[RC, v])[β] // (Subscript[ad, v])[β//(Subscript[RC, v])[β]] // (Subscript[div, u]) // (Subscript[CC, v])[-β],
α // (Subscript[RC, v])[β] // (Subscript[div, u]) // (Subscript[ad, v])[-β//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β]
]
]

D[((1-(E^(-s ad)))/(s ad)), s] /. s-> 1//Simplify

Congruent[Plus[
β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[CC, v])[-β],
β // (Subscript[ad, u])[α] // adSeries[(((E^(-ad)) (1+ad-(E^ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[CC, v])[-β],
β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[ad, v])[β//(Subscript[RC, v])[β]] // (Subscript[div, v]) // (Subscript[CC, v])[-β],
β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, v])[-β//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β],
β // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[CC, v])[-β] // (Subscript[ad, u])[-α]
],
Plus[
α // (Subscript[RC, v])[β] // (Subscript[ad, v])[β//(Subscript[RC, v])[β]] // (Subscript[div, u]) // (Subscript[CC, v])[-β],
α // (Subscript[RC, v])[β] // (Subscript[div, u]) // (Subscript[ad, v])[-β//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β]
]
]

Merge the first two terms

((1-(E^(-ad)))/ad)+(((E^(-ad)) (1+ad-(E^ad)))/ad) // Simplify

Congruent[Plus[
β // (Subscript[ad, u])[α] // adSeries[(E^(-ad)), β] // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[CC, v])[-β],
β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[ad, v])[β//(Subscript[RC, v])[β]] // (Subscript[div, v]) // (Subscript[CC, v])[-β],
β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, v])[-β//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β],
β // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[CC, v])[-β] // (Subscript[ad, u])[-α]
],
Plus[
α // (Subscript[RC, v])[β] // (Subscript[ad, v])[β//(Subscript[RC, v])[β]] // (Subscript[div, u]) // (Subscript[CC, v])[-β],
α // (Subscript[RC, v])[β] // (Subscript[div, u]) // (Subscript[ad, v])[-β//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β]
]
]

Use div property uv on the last two terms

Congruent[Plus[
β // (Subscript[ad, u])[α] // adSeries[(E^(-ad)), β] // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[CC, v])[-β],
β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[ad, v])[β//(Subscript[RC, v])[β]] // (Subscript[div, v]) // (Subscript[CC, v])[-β],
β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, v])[-β//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β],
β // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[CC, v])[-β] // (Subscript[ad, u])[-α]
],
Plus[
β // (Subscript[RC, v])[β] // (Subscript[ad, u])[α//(Subscript[RC, v])[β]] // (Subscript[div, v]) // (Subscript[CC, v])[-β],
β // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, u])[-α//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β]
]
]

The infinitesimal (Subscript[C, u])(Subscript[C, v]) property

(γ // (Subscript[CC, u])[α // (Subscript[RC, v])[-β]] // (Subscript[CC, v])[β]) ≡(γ // (Subscript[CC, v])[β // (Subscript[RC, u])[-α]] // (Subscript[CC, u])[α])

Congruent[
γ // (Subscript[ad, u])[α//(Subscript[RC, v])[-β]] // (Subscript[CC, v])[β],
Plus[γ // (Subscript[ad, v])[β // (Subscript[ad, u])[-α] // adSeries[(((E^ad)-1)/ad), β] // (Subscript[RC, v])[-β]] // (Subscript[CC, v])[β],
γ // (Subscript[CC, v])[β] // (Subscript[ad, u])[α]]]

Congruent[Plus[
β // (Subscript[ad, u])[α] // adSeries[(E^(-ad)), β] // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[CC, v])[-β],
β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[ad, v])[β//(Subscript[RC, v])[β]] // (Subscript[div, v]) // (Subscript[CC, v])[-β],
β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, v])[-β//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β],
β // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, u])[-α//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β]
],
Plus[
β // (Subscript[RC, v])[β] // (Subscript[ad, u])[α//(Subscript[RC, v])[β]] // (Subscript[div, v]) // (Subscript[CC, v])[-β],
β // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, u])[-α//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β],
β // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, v])[-β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β]] // (Subscript[CC, v])[-β]
]
]

Cancel (Subscript[CC, v])[-β] on the right and one repeating term

Congruent[Plus[
β // (Subscript[ad, u])[α] // adSeries[(E^(-ad)), β] // (Subscript[RC, v])[β] // (Subscript[div, v]),
β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[ad, v])[β//(Subscript[RC, v])[β]] // (Subscript[div, v]),
β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, v])[-β//(Subscript[RC, v])[β]]
],
Plus[
β // (Subscript[RC, v])[β] // (Subscript[ad, u])[α//(Subscript[RC, v])[β]] // (Subscript[div, v]),
β // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, v])[-β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β]]
]
]

Use div property vv on terms 2&3

Congruent[Plus[
β // (Subscript[ad, u])[α] // adSeries[(E^(-ad)), β] // (Subscript[RC, v])[β] // (Subscript[div, v]),
β//(Subscript[RC, v])[β] // (Subscript[ad, v])[β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β]] // (Subscript[div, v]),
-β//(Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, v])[β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β]],
b[β//(Subscript[RC, v])[β], β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β]] // (Subscript[div, v])
],
Plus[
β // (Subscript[RC, v])[β] // (Subscript[ad, u])[α//(Subscript[RC, v])[β]] // (Subscript[div, v]),
β // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, v])[-β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β]]
]
]

Cancel terms 3&5, pull (Subscript[RC, v])[β] out of the bracket in term 4

Congruent[Plus[
β // (Subscript[ad, u])[α] // adSeries[(E^(-ad)), β] // (Subscript[RC, v])[β] // (Subscript[div, v]),
β//(Subscript[RC, v])[β] // (Subscript[ad, v])[β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β]] // (Subscript[div, v]),
b[β, β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β]] //(Subscript[RC, v])[β] // (Subscript[div, v])
],
β // (Subscript[RC, v])[β] // (Subscript[ad, u])[α//(Subscript[RC, v])[β]] // (Subscript[div, v])
]

Collapse bracket in term 3 into the adSeries, parially cancel against term 1, undiv

Congruent[Plus[
β // (Subscript[ad, u])[α] // (Subscript[RC, v])[β],
β//(Subscript[RC, v])[β] // (Subscript[ad, v])[β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β]]
],
β // (Subscript[RC, v])[β] // (Subscript[ad, u])[α//(Subscript[RC, v])[β]]
]

Re-evaluate on γ // (Subscript[CC, v])[-β], post-compose with (Subscript[CC, v])[-β]

Congruent[Plus[
γ // (Subscript[CC, v])[-β] // (Subscript[ad, u])[α],
γ // (Subscript[ad, v])[β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β]] //  (Subscript[CC, v])[-β]
],
γ // (Subscript[ad, u])[α//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β]
]

Negate β

Congruent[Plus[
γ // (Subscript[CC, v])[β] // (Subscript[ad, u])[α],
-γ // (Subscript[ad, v])[β // (Subscript[ad, u])[α] // adSeries[(((E^ad)-1)/ad), β] // (Subscript[RC, v])[-β]] //  (Subscript[CC, v])[β]
],
γ // (Subscript[ad, u])[α//(Subscript[RC, v])[-β]] // (Subscript[CC, v])[β]
]

This is the infinitesimal (Subscript[C, u])(Subscript[C, v]) property!

Recycling

(γ // (Subscript[CC, v])[-β] // (Subscript[ad, u])[-α])≡(γ // (Subscript[ad, u])[-α//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β])

β // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[ad, u])[-α//(Subscript[RC, v])[β]] // (Subscript[CC, v])[-β]

β≡(β // adSeries[((1-(E^(-ad)))/ad), β])

Simplify (Subscript[J, v]) // (Subscript[ad, u])[α]

(β // (Subscript[J, v]) // (Subscript[ad, u])[α])

(β // (Subscript[ad, u])[α] // adSeries[((1-(E^(-ad)))/ad), β] // (Subscript[RC, v])[β] // (Subscript[div, v]) // (Subscript[CC, v])[-β]) ≡ (β // (Subscript[ad, u])[α] // (Subscript[J, v]))

(β+(β // (Subscript[ad, u])[α])) // (Subscript[J, v])