[tlaplus] Proving linearity of Fourier Transform

[marta zhango <martazhango@xxxxxxxxx>]

Although TLAPS cannot handle reals, I would like to try using TLA

as a hierarchical proof.  Have done as follows

Constant t, omega, a, b

Constant h, f, g

Constant h \in [Real -> Real]

Constant f \in [Real -> Real]

Constant g \in [Real -> Real]

Constant F \in [Real -> Real]

<1>1. F(h(t)) == Integral ( h(t) * exp( -i * omega * t) , t)

<1>2. h(t) == a * f(t) + b * g(t)

Prove:  F(h(t)) = a * F(f(t)) + b * F (g(t))

Proof:

<1>3. F(h(t)) =  Integral ( (a * f(t) + b * g(t) ) * exp( -i * omega * t) , t)  [by <1>2, <1>1 ]

                      =  Integral ( (a * f(t) * exp( -i * omega * t))   + (b * g(t) * exp( -i * omega * t)) , t)

                      =   a * Integral ( f(t) * exp( -i * omega * t) , t ) 

                                 + b * Integral ( g(t) * exp( -i * omega * t) , t)

                      = a * F(f(t)) + b * F (g(t))     [ by <1>1 ]

<1>4 Q.E.D.

Would be grateful if other can comment and point out improvements

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/f77e5ebc-ec7e-47ce-8f5c-6d8d090a335en%40googlegroups.com.