You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Remove c param from I & integrate. Also improve integrate
In `integrate` when an integral of `f` is not known, leave as `I f`,
so that approximative numerical methods can be applied later (during
`eval`), instead of just crashing.
These were all suggestions by Patrik
Copy file name to clipboardExpand all lines: Physics/src/Calculus/IntegralCalc.lhs
+87-66Lines changed: 87 additions & 66 deletions
Original file line number
Diff line number
Diff line change
@@ -116,7 +116,7 @@ that's our the type of our semantics!). So, we simply say that when
116
116
integrating a function, the constant term must be supplied in order to
117
117
nail the result down to a single function!
118
118
119
-
< | IRealNumFunExpr
119
+
< | IFunExpr
120
120
121
121
122
122
@@ -265,66 +265,67 @@ Let's implement these rules as a function for symbolic (indefinite)
265
265
integration of functions. We'll start with the nicer cases, and
266
266
progress to the not so nice ones.
267
267
268
-
`integrate` takes a function to symbolically integrate, and a real
269
-
number that decides the vertical offset (i.e. the value of $f(0)$ /
270
-
the constant term) of the function. The antiderivative with the given
271
-
vertical offset is returned.
268
+
`integrate` takes a function to symbolically integrate, and returns
269
+
the antiderivative where $F(0) = 0$.
272
270
273
271
Important to note is that not all functions are integrable. Unlike
274
272
derivatives, some antiderivatives of elementary functions simply
275
273
cannot be expressed as elementary functions themselves, according to
276
274
[Liouville's
277
275
theorem](https://en.wikipedia.org/wiki/Liouville%27s_theorem_%28differential_algebra%29). Some examples include $e^{-x^2}$, $\frac{sin(x)}{x}$, and $x^x$.
278
276
279
-
> integrate::FunExpr->RealNum->FunExpr
277
+
> integrate::FunExpr->FunExpr
280
278
281
279
First, our elementary functions. You can prove them using the methods
282
280
described above, but the easiest way to find them is to just look them
283
281
up in some table of integrals (dust of that old calculus cheat sheet)
284
282
or on WolframAlpha (or Wikipedia, or whatever. Up to you).
285
283
286
-
> integrate Exp c =Exp:+Const c
287
-
> integrate Log c =Id:* (Log:-Const1) :+Const c
288
-
> integrate Sin c =Const0:-Cos:+Const c
289
-
> integrate Cos c =Sin:+Const c
290
-
> integrate Asin c = (Const1:-Id:^(Const2)):^(Const0.5)
291
-
>:+Id:*Asin
292
-
>:+Const c
293
-
> integrate Acos c =Id:*Acos
294
-
>:- (Const1:-Id:^(Const2)):^(Const0.5)
295
-
>:+Const c
284
+
> integrate Exp=Exp:-Const1
285
+
286
+
Note that $log(x)$ is not defined in $x=0$, so we don't have to add
287
+
any corrective constant as $F(0)$ wouldn't make sense anyways.
0 commit comments