Earlier quoted context omitted.
So ∫f(x)g(x)dx = (f.g)·dx?
No, f·g = ∫f(x)g(x)dx.
But don't you need to account for the width dx of the slices you sum up? I.e. wouldn't f.g = f(x_0)g(x_0) + f(x_1)g(x_1) + … over a real interval blow up?
Calculus for mathematicians (1997) [pdf]
71–80 of 89 posts
Re: Calculus for mathematicians (1997) [pdf]
#72Earlier quoted context omitted.
Streams are coinductive, thus reals are the type of final coalgebras of (rat * -) which satisfy the Cauchy condition. So something like (Sigma (mu (rat * -)) isCauchy).
Don't you need to quotient after you've got Cauchy sequences? For example, (0,0,0,0,....) is a representative of the same real number (as Cauchy sequence) same as (1,0,0,0,0,0,....), but both are different as streams.
Yeah, depends on how you're encoding it. Quotient types are to my knowledge still tricky to implement, but you can try to make a setoid and structure this type with some kind of equality. Of course, now we run directly into totality and semi-decidability.
Re: Calculus for mathematicians (1997) [pdf]
#73Earlier quoted context omitted.
You also need to translate "with" as a forall (pi binder) as well. Then, you'll merely note that the formula is unsatisfiable without demonstrating a proof that y is within the proper bounds.
Oh good , so I'm not the only one whose mind tries to translate mathematical prose into the notation of dependent type theory!
Sometimes your problem really does just call for a hammer :)
Re: Calculus for mathematicians (1997) [pdf]
#74Earlier quoted context omitted.
No, f·g = ∫f(x)g(x)dx.
But don't you need to account for the width dx of the slices you sum up? I.e. wouldn't f.g = f(x_0)g(x_0) + f(x_1)g(x_1) + … over a real interval blow up?
The point is that f.g (or, as a mathematician or physicist might write it, ⟨f, g⟩ or ⟨f|g⟩) has no independent meaning, but must be defined; and one way to define it (for `L^2` functions, the only one compatible with the `L^2` norm) is as stephencanon did at https://news.ycombinator.com/item?id=9620263 .
Re: Calculus for mathematicians (1997) [pdf]
#75The hardest ( ie , best) math prof I ever had (I was in EE, he was in the math department) used to say that "engineers can teach calculus, but their students cannot go on to teach calculus". I'm impressed by someone who knows a subject deeply enough to take that long of a view. Personally, I just like the engineering view of dx and dy as simply being new variables (with caveats that we immediately forget). Which is w…
> An integral is the inner product of a function and a suitably-dimensioned unit. Does that mean that ∫f(x)dx is f.(dx, dx, …) = f(x_0)·dx + f(x_1)·dx + f(x_2)·dx + … for all x in the domain?
> Does that mean that ∫f(x)dx is f.(dx, dx, …) = f(x_0)·dx + f(x_1)·dx + f(x_2)·dx + … for all x in the domain?
I think that that is what is meant, except that it's not clear what you mean by "for all `x` in the domain"—`x` occurs bound on both sides. Of course this interpretation requires that one understand it as a philosophy rather than a calculation; for example, as your explicit version points out, one really needs tag points spaced `dx` apart to define the inner product, and (absent infinitesimals) the result will be only an approximation to the true integral.
stephencanon (https://news.ycombinator.com/item?id=9620263) gives another interpretation that is unimpeachably mathematically correct, but (a) it is so nearly circular that I think it must be not what bandrami (https://news.ycombinator.com/item?id=9616961) meant, and (b) (perhaps more importantly) the unit there is built into the definition of the inner product itself, rather than being part of the second "inner multiplicand".
Re: Calculus for mathematicians (1997) [pdf]
#76Earlier quoted context omitted.
How did you get that information? How did you, in a non-magical way, go from information about an angle to information about a ratio? If students don't know this information, then perhaps they are studying applications. So, what applications are students taught in typical trigonometric texts? Periodic behavior perhaps? Like sound? Only perhaps a brief blurb in the text that application is even possible. Perhaps they…
> How did you, in a non-magical way, go from information about an angle to information about a ratio? By having a right triangle? The rest of your post seems to show that you want trig to be about periodic behavior, when it really is about triangles. That's what trigonometry means - measuring triangles. Yes, trig has applications to periodic behavior, projectiles, differential equations, inclined planes, and all kind…
But that's my point: it's not really about triangles; that's just a rather mundane application. Trig is really about complex exponentials that solve f'' + f = 0.
Re: Calculus for mathematicians (1997) [pdf]
#77Earlier quoted context omitted.
> An integral is the inner product of a function and a suitably-dimensioned unit. Does that mean that ∫f(x)dx is f.(dx, dx, …) = f(x_0)·dx + f(x_1)·dx + f(x_2)·dx + … for all x in the domain?
> Does that mean that ∫f(x)dx is f.(dx, dx, …) = f(x_0)·dx + f(x_1)·dx + f(x_2)·dx + … for all x in the domain? I think that that is what is meant, except that it's not clear what you mean by "for all `x` in the domain"—`x` occurs bound on both sides. Of course this interpretation requires that one understand it as a philosophy rather than a calculation; for example, as your explicit version points out, one really ne…
No, stephencanon's comment is what I mean, and this may be an example of what my prof. meant that my students would not then be able to teach calculus.
By that point (this course was "differential operators", 700-level stuff) we all had a decent intuition of what inner and outer products are. The prof's comment was that looking at f(x) as an infinite-dimensioned vector, there is a unit *-cube g(x)=1 of compatible dimensions that can produce an inner product f|g (I'm not going to hunt through my character map for the dot or the integral sign). That inner product is the same as Integral(f(x), dx). This was in analogy to the differential operator being the exterior ("wedge") product of a function and its field.
The real point of the definition was relating y' and Integral(y) to div y and grad y: in y' you're going from vectors to tensors, and in Integral(y) you're going from vectors to scalars. Or, Integral(y) is a projection of y on some unit cube, and y' is finding the function of which y is the projection on an appropriate unit cube.
Re: Calculus for mathematicians (1997) [pdf]
#78Earlier quoted context omitted.
But don't you need to account for the width dx of the slices you sum up? I.e. wouldn't f.g = f(x_0)g(x_0) + f(x_1)g(x_1) + … over a real interval blow up?
The point is that f.g (or, as a mathematician or physicist might write it, ⟨f, g⟩ or ⟨f|g⟩) has no independent meaning, but must be defined ; and one way to define it (for `L^2` functions, the only one compatible with the `L^2` norm) is as stephencanon did at https://news.ycombinator.com/item?id=9620263 .
Well, it's not just any arbitrary definition, it's the projection of f onto g. Intuitively, sum(f_i * g_i).
Re: Calculus for mathematicians (1997) [pdf]
#79Definition 5.1/5.2 is interesting. It defines derivative at point c, not the derivative function of f. Note that f1(x) is not equal to f'(x) for all x, but f1(c) = f'(c).
Yeah. The paper says: The derivative of f at c is written f'(c). The derivative of f, written f', is the function c -> f'(c). So the derivative (f') is the result of substituting c for x in f1. For example, if f1 = (x -> x + c) then we would have f' = (c -> c + c) = (c -> 2c).
[deleted]
Re: Calculus for mathematicians (1997) [pdf]
#80try to get the derivative of sin(x) from his approach.