'>>16139007
i think we had this thread before...';

'>>16139007
I imagine the proof of A1.6 will make it clear.';

'>>16139033
Yeah, sorry. I still don't get it. I can't seem to find this anywhere else except this one, rather well-respected, book. So it's hard to find answers. Also the solutions manual doesn't have the answer to the question that involves proving A1.6.';

'>>16139066
The proof is left as an exceptionally difficult exercise ( two asterisks). Unfortunately it's not in the student solution manual.';

'>>16139066
For the exercise they break it down into three parts. For part a they said: "show that sup_k inf_l>=k f([x_1]_l, ..., [x_n]_l) is well defined (i.e., that the sets of numbers involved are bounded). Looking at the function S ([math] S : \mathbb{D}^2 \to \mathbb{D}[/math] such that [math]S(x,y) = x - y[/math]) from Exercise A1.2, explain why both the sup and the inf are there."';

'Bump';

'>>16139007
What we'd like is

[math]\displaystyle \tilde{f}({\bf x}) = \lim_{l \to -\infty} f([x_1]_l, \ldots, [x_n]_l)[/math]

but presumably they haven't defined limits yet, because the usual definition would require already having defined subtraction and absolute value on the reals. In cases where the limit exists, [math]\sup_k \inf_{l \leq -k} a_l[/math] will be the same thing as [math]\lim_{l \to -\infty} a_l[/math].';

'>>16139426
They've only defined arithmetic on finite decimals. Here they're trying to construct real number arithmetic from the definition of real numbers as infinite decimals [math]\dots 000a_na_{n-1}\dots a_1.a_{-1}a_{-2}000\dots[/math]. I don't understand the purpose of having to take the supremum of the infimum though, in this case. It seems like they're trying to extend the notion of continuity given in Definition A1.4.';

'>>16139426
To be specific. They're trying to define addition or substraction as [math]x + y = \tilde{A}(x, y)[/math] and [math]x - y = \tilde{S}(x, y)[/math].';

'>>16139441
I don't see how A1.8 trivially follows from A1.7 unless sup inf distributes over addition and composition.';

'>>16139426
>In cases where the limit exists, [math]\sup_k \inf_{l \leq -k} a_l[/math] will be the same thing as [math]\lim_{l \to -\infty} a_l[/math]
Why's that?';

'Bump';

'This can be seen as a variation on the usual Cauchy sequence construction. First change from the usual approach is that we're using sequences of finite decimals instead of sequences of rational numbers. Second change is that the sequences are infinite in both directions (in other words, they're functions from [math]\mathbb{Z}[/math] to [math]\mathbb{D}[/math]), and we're interested in sequences that are Cauchy in the [math]k \to - \infty[/math] direction; that is, we say a sequence x is Cauchy iff for every integer n there is an integer m such that [math]i, j \leq -m[/math] implies [math]|x_i - x_j| < 10^{-n}[/math]. This second change ultimately makes very little difference. The third change will come later.

The sequence of k-truncations of an infinite decimal as defined in the OP image is a Cauchy sequence as we defined it above. Given an function on finite decimals [math]f : \mathbb{D}^n \to \mathbb{D}[/math], we can make a function [math]\bar{f}[/math] on sequences of finite decimals by simply applying the operation termwise:
[math]\displaystyle (\bar{f}(x_1, \ldots, x_n))_l = f((x_1)_l, \ldots, (x_n)_l)[/math]
If f is [math]\mathbb{D}[/math]-continuous, we can show that [math]\bar{f}[/math] sends tuples of Cauchy sequences to Cauchy sequences.

We say that two Cauchy sequences x and y are equivalent (written x ~ y) iff for every integer n there is an integer m such that [math]i \leq -m[/math] implies [math]|x_i - y_i| < 10^{-n}[/math]. We can show:
- This is an equivalence relation, reflexive, symmetric, and transitive.
- Two infinite decimals are equivalent (as defined in this text OP pic is from, see >>16130580) if and only if their sequences of k-truncations are equivalent as Cauchy sequences.
- If f is [math]\mathbb{D}[/math]-continuous, then [math]x_i \sim y_i[/math] for each i = 1, ..., n implies [math]\bar{f}({\bf x}) \sim \bar{f}({\bf y})[/math].';

'>>16139731 continued
In the usual approach, we define the real numbers as equivalence classes of Cauchy sequences. The third change is that we will instead take a representative element approach. Every Cauchy sequence is equivalent to the Cauchy sequence obtained from the k-truncations of at least one infinite decimal (and at most two infinite decimals, which will be equivalent). Given a Cauchy sequence x, we can show that

[math]\displaystyle \sup_k \inf_{l \leq -k} x_l[/math]

will pick out the desired infinite decimal or pair of infinite decimals.';

'homework thread';

'>>16139455
You can grind this out using the epsilon-delta definition, but what you probably need more is intuition, so I drew an illustrative sketch.';

'>>16139452
Both sides of the equation are the equal when x,y,z are finite decimals, and both are continuous, so by the uniqueness part of A1.6 they are equal everywhere.';

'If we're talking about ways to define real number arithmetic, I prefer pic related because you can both explain it to a child and implement it on a computer (for computable reals only of course).

Supremums, infimums, and limits of infinite sequences can't be computed in general even if you know the sequence itself is computable; see Specker sequences for an example.';

'>>16139828
Is anything lost in requiring a_n, c_n to be integer multiples of 10^n? If not, I don't see what advantages this has over the usual decimal notation.';

'>>16139843
>10^n
10^-n *';

'>>16139843
>>16139846
>Is anything lost in requiring a_n, c_n to be integer multiples of 10^-n?
No. You can do finite decimal nests instead of rational nests if you want. You can use integer multiples of 2^-n as well.

>If not, I don't see what advantages this has over the usual decimal notation.
Having actual working algorithms for the arithmetic operations. Try computing sqrt(2), then multiplying it by itself, and you'll quickly see the issues you'll run into if you try to use a stream of standard decimal digits to represent the number. (If you don't see it right away, think about what you'd get from doing the same thing to sqrt(2)+10^-1000000 or sqrt(2)-10^-1000000.)';

'>>16139747
a culture war or induced dementia thread died for this.';

'>>16139850
Truncating a computable real to its decimal representation introduces an o(10^-n) error, which is negligible when performing a finite number of arithmetic operations. If your point is that this could cause the leading digits to be wrong, then the best way to ensure exact values is to keep sqrt(2) as a formal expression, with sqrt(2)sqrt(2)=1.999... issues deferred by lazy evaluation. Not coincidentally, this is exactly how humans calculate with the reals on paper (or device screen).
There are situations where a rational endpoint representation can be invoked to save labor, but the effectiveness of this strategy will depend on choosing the right representation in the first place, so even on grounds of practical computability, the stream-of-digits representation seems like the better standard.';

'>>16139882
>If your point is that this could cause the leading digits to be wrong,
Yes, that's the issue.

>then the best way to ensure exact values is to keep sqrt(2) as a formal expression, with sqrt(2)sqrt(2)=1.999... issues deferred by lazy evaluation.
My goal is something that works in all cases. sqrt(2)*sqrt(2) is hardly the only calculation you can do with irrational numbers that yields a terminating decimal as the answer.';

'>>16139756
That would also be true of [math]\tilde{M}(x,A(y,z)) - \tilde{A}(M(x,y),M(x,z))[/math], i.e. without tildes for the functions in the arguments, wouldn't it?';

'>>16140148
Without the tildes the arguments have to be finite decimals. So in that expression x, y, and z can only be finite decimals in the first place.';

'>>16140181
Good point. I don't see why the whole business with sup inf is necessary anyway. Why can't the function just be f([x_1]_l, ..., [x_n]_l). I.e., it takes any real number, truncates it, and then does arithmetic like with finite decimals. Isn't this continuous, well-defined, and everywhere defined?';

'>>16140195
because it's not as complex and cool as whatever is written in OP's pic
t. mathlet and I spit on mathematicians faces daily';

'>>16139750
I think I get it intuitively, but I don't see how to prove it? Is it easy to prove?';

'>>16140195
>Why can't the function just be f([x_1]_l, ..., [x_n]_l).
Because the function is supposed to return an infinite decimal, not a finite decimal or a sequence of finite decimals (not sure which you're trying to indicate here).
>I.e., it takes any real number, truncates it, and then does arithmetic like with finite decimals.
What do you mean by "like"? Truncation gives you a finite decimal, and the function f takes finite decimals as inputs and outputs.';

'>>16140207
Well how do you know that [math]\sup_k \inf_{l \leq -k} f([x_1]_l, \ldots, [x_n]_l)[/math] returns an infinite decimal? We know it has an infinite decimal input, but why does that mean it's output is one?';

'>>16140199
It's not too difficult, although I have no idea what level you're at. You have some number that's the limit and you're trying to prove it's also the supremum of a certain set. Write out the definition of a limit and consider each part of the definition of supremum, thinking about why it can't be otherwise.';

'>>16140224
This is how I understand the limit here: A sequence [math]i \mapsto \textbf{a_i}[/math] of points in [math]\mathbb{R}^n[/math] converges to [math]\textbf{a} \in \mathbb{R}[/math] if [math]\forall \epsilon > 0, \exists M \mid m > M \implies |\textbf{a_m} - \textbf{a}| < \epsilon[/math] we then call [math]\textbf{a}[/math] the limit of the sequence.

The supremum is the least upper bound, i.e. [math]\forall \textbf{a_i}[/math] we have that the supremum is greater than or equal to such that [math]\forall \epsilon > 0, \exists \textbf{a_i} \mid \textbf{a_i} + \epsilon > \sup[/math].

I don't see how that implies that the sup of the inf gives the limit though.';

'>>16140224
I know that the inf are an increasing sequence with increasing k because the inf of a subset is greater than or equal to the inf of the set. I suppose the sup is like taking k to infinity?';

'>>16140224
Wouldn't we need to know that the inf exists for every k? As in, we need to know that the sequence of values of f is bounded. How do we know that?';

'>>16140215
The supremum and infimum operations are being done in the real numbers, which have been defined here as equivalence classes of infinite decimals (each equivalence class containing either one or two infinite decimals). The infimum operation takes a set of finite decimals and gives you the greatest real number that is less than or equal to all the finite decimals. It might be equal to one of the finite decimals (meaning the real number ends in infinite 0s or 9s), and that's alright. The point is that we're working with the right type of object now. The supremum operation takes a set of real numbers (generated by the infimum operation with different values of k), and gives you the least real number that is greater or equal to all of them.';

'>>16140255
So a number greater than or equal to a set of numbers that are less than or equal to a sequence of finite decimals? I.e. sup inf f. Ok I can see how that gives you a real number, partly because real numbers are complete so suprema exist in the real numbers. I don't quite understand how this is equivalent to taking a limit.';

'>>16140252
Yes, that's something we ought to verify too.
>As in, we need to know that the sequence of values of f is bounded.
Assuming you mean the sequence starting at l = -k and going towards negative infinity, then yes. The set of values of f for every integer l doesn't need to be bounded.

Not sure whether you're considering whether the infimums exist under the conditions of my remark in >>16139426 (which didn't mention f) or whether it exists in the conditions of definition A1.5. Those are two different questions that would have different proofs.';

'>>16140277
Could you show it's bounded by the fact that f is finite decimal continuous? So we assume k is a number such that [math]\forall l \leq -k, and for i=1, \dots, n |[x_i]_l - [x_i]_k| \leq 10^{-k}[/math] and that [math]|f([x_1]_l, \dots, [x_n]_l) - f([x_1]_k, \dots, [x_n]_k)| < 10^{-m}[/math] for some integer m, by finite continuity. This would ensure that f is bounded both below and above right?

>The set of values of f for every integer l doesn't need to be bounded.
Presumably you meant for every integer l less than or equal to -k. Why not?';

'>>16140299
Some smart guy posting formulas. Perfect. Satan has been raping me and concussing me while he gaslights me. Assuming A = B, what's the answer here scientist NPC. I know you aren't real like I am.';

'>>16140277
Ignore the last question here, after the greentext >>16140299
as, you did specify it for l<=-k, I clearly didn't read your response properly.';

'Is this a sufficient condition for the sequence to be bounded>>16140299 ?';

'>>16140224
Oh, the supremum is the limit of a bounded nondecreasing sequence?';

'Bump';

'>>16140299
>Could you show it's bounded by the fact that f is finite decimal continuous?
Yes. You're on to the right idea, but you're applying the definition in the wrong direction. The definition lets you choose the integer you've called m and gives you the integer you've called k. You're also going to need to use the fact that [math]\{[x_i]_l | l \leq -j\}[/math] is bounded for any j to choose the other integer called "N" in the definition and satisfy the condition relating to it. Since the definition doesn't let you choose k, you'll need an extra step to prove that your sequence of f values is bounded for any k.';

'>>16140652
So is Proposition A1.6 missing the assumption that f is bounded above and below for each k?';

'>>16140421
>Oh, the supremum is the limit of a bounded nondecreasing sequence?
Using that's a good idea and would probably end up making for a more readable proof than what I was originally thinking. You'll also need to show that if the sequence converges to a limit, then the infimums converge to the same limit.

By the way, are you able to work out the proof of that theorem on your own without looking it up? If so, with those same sort of techniques you ought to be able to prove the remark in >>16139426. If it's something you would struggle with, it might be a good exercise to improve your skills which would be easier than jumping straight into proving that remark.';

'>>16140664
I've seen the proof of the theorem that a nondecreasing sequence converges if and only if it is bounded; it's in the book. I also see how the supremum is the limit.
>You'll also need to show that if the sequence converges to a limit, then the infimums converge to the same limit.
That I don't see how to actually show it, although it makes sense.';

'>>16140657
I don't think that theorem is missing anything. It is assuming f is [math]\mathbb{D}[/math]-continuous; otherwise [math]\tilde{f}[/math] does not exist. We don't need f to be bounded over its entire domain, and clearly A and M from >>16139441 are not bounded. We can show from the fact that f is [math]\mathbb{D}[/math]-continuous that it is bounded on [math]\{(x_1, \ldots, x_n) \in \mathbb{D}^n | |x_1|, \ldots, |x_n| < N\}[/math] for any N. I'm not sure what you mean by "f is bounded above and below for each k".';

'>>16139007
it’s just taking a limit, without having to define what a limit is. as k gets larger, that inf gets bigger (or stays the same) approaching the target value. then the sup grabs that value

what book is this by the way? it looks kinda autistic but foundation-level stuff always does, I guess. still weird that you would say a real is a string of digits (the intuitive approach) and then go autismo mode about it';

'>>16140688
Well how do we know the inf and sup exist if it's not bounded?';

'>>16140694
"Vector Calculus, Linear Algebra, and Differential Forms" by J. H. Hubbard and B. B. Hubbard. It's from the Appendix which is apparently all analysis.';

'>>16140700
the continuity condition says approximately that it is bounded, WHEN you focus on the area close to x. for example if you set k=1, you get m such that any y within 10^-m of x must have |f(x)-f(y)| <10
>>16140702
oh ok I’ve heard of that one but never read it';

'>>16140718
I guess I mean 1/10 not 10. But 10 would be good enough too if all you want is that it’s bounded';

'>>16140718
So in equation A1.5 does k there correspond to what you mean by m? Is k in A1.5 assumed to be a value such that the values of the function are within 10^-m for whatever m you want?';

'>>16140722
Sorry, I meant
>such that the values of the function are within 10^-k if the inputs are within 10^-m';

'>>16140723
Again, I got it wrong. I mean
>such that the values of the function are within 10^-m if the inputs are within 10^-k';

'>>16140723
yeah l just don’t like typing l because it looks like an l';

'>>16140729
So the inf exist by definition as we require k to be a number such that for [math]l \leq -k, |f([x_1]_l, \dots, [x_n]_l) - f([x_1]_k, \dots, [x_n]_k)| < 10^{-m}| \forall m > 0[/math] where [math]m \in \mathbb{N}[/math]?';

'>>16140740
The k in A1.5 ranges over all integers (although you'd lose nothing by making it range over all naturals instead). But what you can do is first use the [math]\mathbb{D}[/math]-continuity condition to find a particular k that makes the infimum exist, then use that to show the infimum exists for all k.

Be careful about your order of quantifiers. It sounds like you're saying that there exists a k such that for all [math]l \leq -k[/math] and for all m,
[math]|f([x_1]_l, \dots, [x_n]_l) - f([x_1]_k, \dots, [x_n]_k)| < 10^{-m}[/math].
But saying that something has an absolute value less than [math]10^{-m}[/math] for all m would make it equal to zero. That's not what we want here.

The way definition A1.4 works is that you pick a number specifying how much of the domain of f we're considering (N in the original) and a number specifying how close together you want the f values to be (m in your post, k in the original), and then it gives you a number specifying how close together the two inputs have to be (k in your post, l in the original) which will in general depend on the two numbers you picked.';

'>>16140822
Why would the infimum exist for smaller k if you find it exists for a given k? If it exists for a given k, then it must also exist for larger k as all such truncations of the input will be k-close and so by continuity the function values are bounded. But I don't see why the infimum must exist for all k.';

'>>16140847
Because you are adding finitely many elements to the set you are taking the infimum of.';

'>>16140853
But couldn't one of those elements be negative infinity or something. I mean what ensures that both the inf and the sup exists for all truncations of the input real numbers?

Just to be clear, this is the largest stumbling block here for me. I don't get how we know the sets of values of the functions for all truncations <= -k and for all k are bounded. I think it is related to finite decimal continuity, but I don't see explicitly why we can expect the infimum to exist for all k and for the supremum of these infimum to exist.';

'>>16140863
>But couldn't one of those elements be negative infinity or something.
No, because negative infinity isn't a finite decimal. In general, the only way to have a set of real numbers that isn't bounded below is to have infinitely many numbers in that set.';

'>>16140878
Ok that makes sense. But the set of function values here is infinitely large as it is for all truncations less than or equal to -k. Now, I can see that for all inputs in f where the truncation is less than or equal to -k are k-close, but that doesn't guarantee that the the function values are m-close (or whatever-close) as the quantitiers are the other way around for continuity. I.e., for all k there exists l (k and l in Definition A1.4) not for all l there exists k.';

'>>16140886
When you change k, the only change to the set in question is adding or removing a finite number of elements. If a nonempty set is bounded below and you add finitely many elements, the new set is bounded below either by the old infimum or by the minimum of the new elements, whichever is smaller.';

'>>16140936
So we choose k such that [math]f([x_1]_l, \dots, [x_n]_l)[/math] is bounded for [math]l \leq -k[/math]. I.e., we choose k such that [math]|f([x_1]_l, \dots, [x_n]_l) - f([x_1]_k, \dots, [x_n]_k)| < 10^{-m}[/math] for some m. Then, it is also bounded for all k as you are just adding finitely many terms and all of those terms are finite numbers so the supremum and infimum exists? Does the continuity come into the proof that the sets of numbers involved are bounded by the fact that for any m such that the outputs are m-close, there exists a k such if the inputs are k-close (or l-close where l <= -k which necessarily is also be satisfied) the outputs are m-close? So all that matters is finding one such k, and then it must be true for all k?';

'>>16140956
Yes, you've mostly got it. One small change, you still need to work in N and the [math]|x_i|, |y_i| < N[/math] condition.';

'>>16140962
Great. How do we show that [math]\tilde{f}[/math] satisfies the continuity condition given in A1.6 though? I'm not sure how to demonstrate that the sup inf f are k-close. I.e. that for all [math]k \in \mathbb{N}[/math] and all [math]N \in \mathbb{N}[/math], there exists [math]l \in \mathbb{N}[/math] such that when [math]\textbf{x}, \textbf{y} \in \mathbb{R}^n[/math] are l-close and all coordinates [math]x_i[/math] of [math]\textbf{x}[/math] satisfy [math]|x_i| < N[/math], then [math]\tilde{f}(\textbf{x})[/math] and [math]\tilde{f}(\textbf{y})[/math] are k-close.';

'>>16140977
Well, we have results about the closeness of values of f, so a good approach would be to relate values of [math]\tilde{f}[/math] to values of f. What can you say about the closeness of [math]\tilde{f}({\bf x})[/math] and [math]f([{\bf x}]_k)[/math]?';

'>>16141016
Presumably they get closer for larger k as that is what sup inf does. But I can't say anything specific, like they are m-close or whatever.';

'>>16141016
I mean, just because the arguments are close doesn't mean the outputs are close. Continuity says that for any k, there exist l; not the other way round. It also doesn't say that l is small.';

'Bump';

'>real number arithmetic
https://www.youtube.com/watch?v=H84VyZCOCew&list=PLIljB45xT85A-qCypcmZqRvaS1pGXpTua&index=2';

'>>16141134
>Presumably they get closer for larger k as that is what sup inf does.
For smaller k, but you get the idea. Now formulate that more precisely and figure out how to prove it, and you should have something to work with.

>>16141322
Not that I have anything against bumping, but if you're worried about the thread dying you could also make a thread on mathchan and/or lambdaplusjs where it would stick around a bit longer.';

'Besides sequences of nested intervals as mentioned in >>16139828, here are some other computation-friendly ways to represent real numbers.

One representation which you've probably used without knowing it is the one in the Android calculator app:
>The library represents real numbers as class CR Java objects with an appr() method. A call to appr(n), where n is typically negative, produces an approximation accurate to [math]2^n[/math]. The actual result returned is implicitly scaled (multiplied) by [math]2^{-n}[/math], so that it can be represented as an integer. For example, if THREE is the constructive real representation of 3, then THREE.appr(−3) would yield 24, that is, 3 multiplied by [math]2^3[/math] or 8. That would be the only acceptable answer, since the result always has an error of < 1.
https://cacm.acm.org/practice/small-data-computing/

Here's another representation from the Coq proof assistant's standard library:
https://coq.inria.fr/doc/V8.19.0/stdlib/Coq.Reals.Cauchy.ConstructiveCauchyReals.html
In this representation, real numbers are represented as Cauchy sequences of rational numbers. If you look at the implementation, you can see they use a variation which are infinite in both directions and converge in the [math]k \to -\infty[/math] direction, the same as the "second change" in >>16139731. But more importantly, there is an explicit guarantee on how fast the sequence converges; specifically, [math]p \le q[/math] and [math]q \leq k[/math] imply [math]|x_p - x_q| < 2^k[/math]. Also, each sequence is accompanied by an explicit bound given in the form of an integer [math]scale[/math] such that [math]|x_k| < 2^{scale}[/math].

If you want to use a stream of digits, one way around the computation issue mentioned in >>16139892 is to increase the available digits. For example, in base 10, instead of using the digits 0 through 9, use the digits -9 through 9.';

'>>16141671
>Now formulate that more precisely
It again seems like trying to show that for any δ there exists ε in the usual definition of continuity. That is to say, the quantifiers are in the wrong order.';

'>>16141796
What's the quantifier order you think you would be able to show?';

'>>16141904
Well, [math]\tilde{f}(\textbf{x})[/math] and [math]f([\textbf{x}]_k)[/math] are k-close in their arguments. Oh, so you can show that for any m, there exists a k such that if the argument of f is k-truncated, the outputs are m-close?';

'>>16141910
Yes, that's the idea. Small thing which you'll need when you go to use this: The usual epsilon-delta formulation is a stronger statement than this. Can you see what you left out that would make it more analogous to epsilon-delta if you included it? Also, can you see how we could use this for the ultimate goal of showing [math]\tilde{f}({\bf x})[/math] is close to [math]\tilde{f}({\bf y})[/math]?';

'>>16141926
Actually, asserting that the two functions are m-close is again assuming that [math]\tilde{f}[/math] is continuous isn't it? We know that it's the limit of f for k-truncations approaching negative infinity, but how do we know how close it is? Sorry, I'm quite confused here.';

'>>16141940
At this point, what you said in >>16141910 is just a conjecture, yet to be proven. So the other thing you should think about is how you might prove it. Once you've proven it, you should be able to use it as part of a proof that [math]\tilde{f}[/math] is continuous.';

'>>16142155
For any m, there exists k such that for all l<=-k we have the difference in function values is less than 10^-m by the continuity of f. [math]\tilde{f}[/math] is the limit of the sequence of function values which must also be within 10^-m by the definition of a limit?';

'>>16142171
Except we can't use limits since we haven't defined them yet.';

'What is the book/branch of mathematics!? This looks neat !';

'>>16142310
With Jews, there's news. Without Jews, there's no news. Wtf? Who wants to live in a werld without news?';

'>>16142253
Could you show me then please? I'm not sure how to proceed.
>>16142310
"Vector Calculus, Linear Algebra, and Differential Forms" by Hubbard & Hubbard.';

'>>16142337
Well, we could do it with limits if we first give a definition of what a limit means. Since this is a sequence of finite decimals, we don't have to define what a limit means in general, just what it means for this particular case. This can be done without having subtraction of real numbers defined.

Also remember we weren't done with our proof that this object was the limit anyway. We still needed to prove that the sequence of infimums converge to the same place the sequence does.';

'>>16142525
Oh, yeah, and the other thing missing is that we haven't proven that the sequence in question actually converges to anything. I remarked that if it did converge to something, the sup-inf device gives its limit, and we had been trying to prove that. There are cases where the sup-inf thing exists but the limit does not exist; consider a sequence alternating between 0 and 1.';

'>>16142525
The sup is the limit of the sequence of infs as it is bounded and nondecreasing. I don't know how to prove that infs converge to the same limit that the sequence does.
>>16142535
The sequence converges because we have that for any m, there exists k such that if l<=-k, the function values are within 10^-m by continuity. I.e. they get arbitrarily close.';

'>>16142541
>The sequence converges because we have that for any m, there exists k such that if l<=-k, the function values are within 10^-m by continuity. I.e. they get arbitrarily close.
They get arbitrarily close to each other. But consider the sequence 1, 1.4, 1.41, 1.414, 1.4142, ... in the terminating decimals, with each term giving one more digit of [math]\sqrt{2}[/math]. The terms certainly get closer to each other, but within the terminating decimals, there's no limit. The whole point of the reals is to make this limit exist.

Anyway, for a start, do you see how we can rewrite the definition of a limit so that we can apply it to a sequence of terminating decimals without having to define subtraction involving real numbers?

Another thing to think about: We're considering a set [math]\{f([{\bf x}]_l) | l \leq -k\}[/math] for which all elements are less than [math]10^{-m}[/math] apart. What can we say about how far the infimum and supremum of the set are from any given element?';

'>>16142541
Also, in general, we shouldn't be using most theorems about reals at this point, because they rely on a bunch of stuff about the reals we haven't proven yet. That includes that "bounded and nondecreasing -> limit is the supremum" result (generally known as the monotone convergence theorem). But it may help to look at its proof for hints and tricks that we can apply to the thing we want to prove.';

'>>16142593
Let a_1, a_2, ... be a sequence of finite decimals. We say that the sequence converges to a limit A if for any m, there exists N such that for n=>N, |a_n - A| < 10^-m.
>What can we say about how far the infimum and supremum of the set are from any given element?
Well it has to be that there exists k, such that for l<=-k |sup - f([X]_l)| < 10^-m. If sup - f([X]_l) > 10^-m, then there exists m such that sup - 10^-m is greater than f([X]_l) for all l<=-k, a contradiction.';

'>>16142639
>a_n - A
This is the part that hasn't been defined yet. But we can rephrase the definition so it doesn't need to be used. (Or you could define it, but then you would need to prove its properties in order to actually use it.)

>Well it has to be that there exists k, such that for l<=-k |sup - f([X]_l)| < 10^-m. If sup - f([X]_l) > 10^-m, then there exists m such that sup - 10^-m is greater than f([X]_l) for all l<=-k, a contradiction.
Even ignoring the undefinedness of the subtraction, I don't think this proof works. The opposite of "for l<=-k |sup - f([X]_l)| < 10^-m" would be "for some l<=-k |sup - f([X]_l)| >= 10^-m".';

'>>16143427
Could you show me? I'm not making any progress.';

'>>16143427
The book says to look at [math]S : \mathbb{D}^2 \to \mathbb{D}, S(x,y) = x - y[/math] to explain why both the sup and inf are there.';

'>>16143514
The rephrasing of the definition I'm thinking of is just a simple algebraic manipulation of |a_n - A| < 10^-m. Remember, all operations done to two finite decimals to get another finite decimal are defined at this point and therefore okay. Also, we know what comparison means for all decimals, whether infinite or finite; it's just the obvious lexicographic ordering.

It's a good idea to make reasonable conjectures about what we can prove before attempting to launch into the proof. So let's say we have an infinite set S of finite decimals for which all elements are less than [math]10^{-m}[/math] apart. Pick a value for m, for example m=0, and look at some examples of sets which have this property and figure out what their supremums and infimums are. Once you have a conjecture, test it a bit by trying to make sets which are counterexamples to your conjecture.';

'>>16141439
1. add digits, writing occurrences of 9 and [math]\bar{9}[/math] as [math]1\bar{1}[/math] and [math]\bar{1}1[/math] respectively
2. add carries from the previous digit';

'>>16143918
Do you mean something like this:
Let a_1, a_2, ... be a sequence of finite decimals. We say that the sequence converges to a limit A if for any m, there exists N such that for n=>N, |a_n - 10^-m| < A.?
>look at some examples of sets which have this property and figure out what their supremums and infimums are.
What do you mean?';

'>>16144013
"Something like that" in the sense that what you wrote is well-defined. But we want something equivalent to the original condition, and |a_n - 10^-m| < A is certainly not equivalent to |a_n - A| < 10^-m.

>What do you mean?
Can you give me a concrete example of an infinite set in which all elements are less than 1 apart? What is its supremum and infimum?';

'>>16144035
>we want something equivalent to the original condition
I can't think of how to do that without relying on undefined arithmetic.
>Can you give me a concrete example of an infinite set in which all elements are less than 1 apart?
The set of [math](\frac{1}{2})^i[/math] for [math]i \in \mathbb{N}[/math] and [math]i \geq 1[/math] ? It's supremum is 1/2 and its infimum is 0.';

'>>16144035
For any m, there exists k such that |S(A,y)| < 10^-m if A and y are k-close?';

'Bump';

'>>16144259
>For any m, there exists k such that |S(A,y)| < 10^-m if A and y are k-close?
There is no such thing as S(A,y). That said, you could use the concept of k-closeness to formulate the idea of the sequence approaching that sup-inf expression. That was my first idea before I realized it would probably be easier to just express it in terms of terminating decimal arithmetic.

>>16144052
>I can't think of how to do that without relying on undefined arithmetic.
When you wrote |a_n - 10^-m| < A you had the right idea of putting [math]a_n[/math] and [math]10^{-m}[/math] on one side and A on the other. What would be the proper way of manipulating [math]|a_n - A| < 10^{-m}[/math] to get A by itself?

>The set of [math](\frac{1}{2})^i[/math] for [math]i \in \mathbb{N}[/math] and [math]i \geq 1[/math] ? It's supremum is 1/2 and its infimum is 0.
Yes, that set qualifies. For that set, every element is less than [math]\frac{1}{2}[/math] away from the supremum and at most [math]\frac{1}{2}[/math] away from the infimum. Now would those two statements apply to any set where pairs of elements have to be less than 1 apart? If not, what statements about the distance between the elements and the supremum/infimum do you think would apply to every such set?';

'>>16144830
If A >= a_n for all n, then for all m, there exists k such that for n>=k, A < 10^-m + a_n?
>Now would those two statements apply to any set where pairs of elements have to be less than 1 apart?
I'm not sure what you're getting at. If pairs of elements have to be less than 1 apart, then all the elements can't be further from the suprema/infima than 1. Could you spell out what you're thinking in regards to defining a limit in this case and proving that sup inf is that limit? It seems I'm not getting any closer.';

'>>16144924
>If A >= a_n for all n, then for all m, there exists k such that for n>=k, A < 10^-m + a_n?
Getting there. That's certainly true for any A that the [math]a_n[/math] converge to, but it's a weak statement. I notice you added a condition "If A >= a_n for all n". Do you need this condition?
>If pairs of elements have to be less than 1 apart, then all the elements can't be further from the suprema/infima than 1.
Yes, now how can you prove this?';

'>>16144955
Well if A wasn't a supremum for the sequence we couldn't say that A - a_n < 10^-m for all n>=k
>Yes, now how can you prove this?
Let A be a supremum for a sequence b_n such that |b_i - b_j| < 1 for all i, j. If |A - b_n| > 1 for some n, then A - b_n > 1 and b_n < A -1 so A is not a supremum contradicting our assumption.';

'>>16144980
>Well if A wasn't a supremum for the sequence we couldn't say that A - a_n < 10^-m for all n>=k
Why not?
>b_n < A -1 so A is not a supremum
This step doesn't follow.';

'>>16144993
>Why not?
Yeah, I guess that's not true.
>This step doesn't follow.
Yes, because it's only for some n, not all n. I don't know how to prove it.';

'>>16144993
Let S be the set of a_n such that |a_i - a_j| < 1 for all i, j. Let A be a supremum of this set. The assertion is that for all a_n, A - a_n < 1. There exists an element a_k of S such that for any ε, A - ε < a_k <= A. So a_k + ε > A for any ε, but also a_k - a_n < 1 for any n so A - ε - a_n < 1 for any ε or A - a_n < 1 + ε for any ε so no elements of S can be further than 1 away from the supremum.';

'>>16145027
I should specify, any ε>0';

'>>16145027
>>16145030
>A - a_n < 1
Do you mean A - a_n <= 1? Other than that it looks good.

Can you do the same proof but make sure the only things we add or subtract are finite decimals? (assuming all the a_n are finite decimals)';

'>>16145073
I'd reword it like this:

Let S be the set of finite decimals a_n such that |a_i - a_j| < 1 for all i, j. Let A be a supremum of this set. The assertion is that for all a_n, A =< a_n + 1. There exists an element a_k of S such that for any integer m, A < a_k + 10^-m, but also a_k - a_n < 1 for any n so A < a_n + 10^-m + 1 for any integer m, so no elements of S can be further than 1 away from the supremum.

But I'm not sure if that works. I've lost the train of thought at this point though, what are we trying to prove?';

'>>16145027
Oh, another thing I noticed that should be fixed:
>There exists an element a_k of S such that for any ε, A - ε < a_k <= A.
should really be
>For any ε, there exists an element a_k of S such that A - ε < a_k <= A.
and the similar fix should be made in >>16145091.

Also, this is more of a clarity issue, but I think instead of writing
>the set of a_n such that
it would be clearer to write
>a set of a_n such that

>But I'm not sure if that works.
Is there a step or two that seems doubtful? If so it might be worth taking a more detailed look at it.

>I've lost the train of thought at this point though, what are we trying to prove?
Well, if we can do this for a set with |a_i - a_j| < 1 we can do a similar thing for a set with |a_i - a_j| < 10^-m. And proving bounds on how close the supremum and infimum of the whole set are to the elements of the set is a step toward proving bounds on how close the elements in that sequence of infimums are to the elements of the set, and then how close their supremum is to the elements of the set.';

'>>16145105
>it would be clearer to write
>>a set of a_n such that
Or "the given set" would work also.
Issue is "the set of a_n such that |a_i - a_j| < 1" sounds like we're saying there's exactly one set matching that description.';

'>>16145105
>Is there a step or two that seems doubtful? If so it might be worth taking a more detailed look at it.
So is what i wrote, with your corrections right? Then I suppose it's trivial to replace 1 with 10^-m for some integer m. I forgot how we even know that the set has a supremum/infimum. But if they exist, then we've shown that they are no further than 10^-m from any elements of the set/sequence.
>proving bounds on how close the elements in that sequence of infimums are to the elements of the set, and then how close their supremum is to the elements of the set.
How do we do that?';

'>>16145114
>So is what i wrote, with your corrections right?
I don't see any problems.

>I forgot how we even know that the set has a supremum/infimum.
That might be worth revisiting. Let's say we have a set S of a_n such that |a_i - a_j| < 10^-m. Can we prove this set has lower and upper bounds? (Also, can we use these bounds to give a simpler proof of sup S <= a_n + 1?)

>How do we do that?
Well, let's say we have a sequence of a_n such that for some k, |a_i - a_j| < 10^-m for i,j >= k. In fact, let's make our lives a bit easier. Just chop off the part of the sequence before k. Now we have a sequence a_n such that |a_i - a_j| < 10^-m is true for the whole sequence.

We can now consider the sequence of infimums [math]b_k = inf_{j \geq k} a_j[/math]. What can we say about how far the [math]b_n[/math] can be from the [math]a_n[/math]? How small are the [math]b_n[/math] allowed to be and how large are they allowed to be?';

'>>16145125
>Can we prove this set has lower and upper bounds?
For any i, j |a_i - a_j| < 10^-m, |a_i| - |a_j| < 10^-m, |a_i| < |a_j| + 10^-m for all i. Thus |a_j| + 10^-m is an upper bound for the set.
>What can we say about how far the [math]b_n[/math] can be from the [math]a_n[/math]?
They can't be further than 10^-m away, so the b_n can be as small as a_j - 10^-m for all j>=k.';

'Bump';

'>>16145183
>Thus |a_j| + 10^-m is an upper bound for the set.
True. (a_j + 10^-m would also work.)

>They can't be further than 10^-m away, so the b_n can be as small as a_j - 10^-m for all j>=k.
Exactly. We should also say how large they can be, compared to the a_j. From here we can say how large and small their supremum can be.';

'>>16145655
The infima can be as large as a_i for some i>=k such that a_i <= a_j for all j>=k. For the supremum, do you mean the supremum of the sequence of infima? I don't know what we can say about that.';

'>>16145696
Maybe let be me more direct in what I'm thinking of.

Let m be an integer. Let a be a sequence such that [math]|a_i - a_j| < 10^{-m}[/math] for all i,j. Let b be the sequence defined by [math]b_i = \inf_{j \geq i} a_j[/math]. Let [math]a_n[/math] be an arbitrarily chosen member of the sequence a. You should be able to show:

[math]a_n - 10^{-m} < a_i < a_n + 10^{-m}[/math] for all i
[math]a_n - 10^{-m} \leq b_i \leq a_n + 10^{-m}[/math] for all i
[math]a_n - 10^{-m} \leq \sup \{b_i\} \leq a_n + 10^{-m}[/math]';

'>>16145731
>Let a be a sequence
I should have specified:
*Let a be a sequence of finite decimals';

'>>16145731
in fact for the second one we can (and may as well) show the stronger
[math]a_n - 10^{-m} \leq b_i < a_n + 10^{-m}[/math] for all i';

'>>16145731
The first one follows naturally from |a_i - a_n| < 10^-m as this means (by definition) -10^-m < a_i - a_n < 10^-m, so we have, for fixed n that: a_n - 10^-m < a_i < a_n + 10^-m.

The second one comes as follows: we assert that b_i <= a_j for any integer n, there exists an element a_l such that b_i > a_l - 10^-n, but also a_j - a_l < 10^-m, so b_i > a_j - 10^-m - 10^-n for any n, j so b_i >= a_j - 10^-m. I'm not sure how to prove the other side of the inequality or the last statement.';

'Bump';

'Bump';

'>>16145731
You've been very helpful so far, thanks, but if you get tired of responding could you please leave your proof in the thread as you seem to be very familiar with the material and I can't find any more information anywhere else. I made a math.stackexchange post but it hasn't had any replies: https://math.stackexchange.com/questions/4901480/how-to-use-finite-decimal-continuity-to-define-real-number-arithmetic';

'>>16139007
>literally writing a book after getting btfo that 0.9999.... is obviously not 1
TOP KEK
mathcucks are shitting themselves that people are catching onto the fraud';

'>>16139869
I mean this is what science is tho… how else would you be able to collect and test new knowledges about the universe without connecting it to the limits of current civ in whatever sector… Apollonian and Dionysian ways of being a human is I think good two sectors to stretch out and test… but w/e… if I’m in an animal farm I can do that';

'>>16145760
>we assert that b_i <= a_j
I'm not sure what this statement is doing here, and this would be only true for [math]j \geq i[/math]. The stuff that follows looks good. (I hope you're not implicitly assuming [math]j \geq i[/math] for that stuff, because you don't need it.)

Here's a simpler proof: notice that [math]a_n - 10^{-m}[/math] is a lower bound for all the [math]\{a_j\}[/math] and therefore also a lower bound for any subset, including [math]\{a_j | j \geq i\}[/math] for any i. Thus if [math]b_i < a_n - 10^{-m}[/math], it could not be the greatest lower bound of [math]\{a_j | j \geq i\}[/math], since [math]a_n - 10^{-m}[/math] would be a greater one.

>>16146638
I wouldn't say I have any special familiarity, anyone with some practice with basic epsilon-delta style proofs ought to be able to read this author's definitions and work through this stuff. I do check the boards in >>16141671 if you want to make a thread somewhere that will stick around longer. For the moment I think you should take some more time to think through the stuff in >>16145731; none of the proofs should be very difficult.';

'>>16146653
This is a construction of the reals based on infinite decimals, so he just defines them to be equivalent.';

'>>16146845
Or rather "they." Authors of this text are husband and wife.';

'>>16146824
Ok, for the inequality here >>16145747 it is asserted that for [math]n\geq i, \forall i b_i < a_n + 10^{-m}[/math]. This follows because we know that [math]a_n + 10^{-m}[/math] is an upper bound for the entire set (and consequently all subsequences). [math]b_i[/math] can't be equal to [math]a_n + 10^{-m}[/math] otherwise it wouldn't be a lower bound and it obviously can't be greater.

For the last inequality we have that [math]a_n - 10^{-m} \leq \sup \{b_i\}[/math] for all i, because we already know that [math]b_i \geq a_n - 10^{-m}[/math] and we also have that [math]\sup \{b_i\} \geq b_j \geq b_i[/math] for [math]j \geq i[/math] because the infimum of a subset is necessarily greater than or equal to the infimum of a set. We also have that [math]\sup \{b_i\} \leq a_n + 10^{-m}[/math] because [math]a_n + 10^-m[/math] is an upper bound for the sequence of infima. I don't know why it could be equal though.';

'>>16146824
By the way, with regards to using the least upper bound property of the real numbers: in the book it's a theorem that is proved, because the real numbers are defined as infinite decimals. It's theorem 0.5.3, so I think it should be fine to use it.';

'>>16146845
see >>16146653';

'>>16146878
>for [math]n\geq i, \forall i b_i < a_n + 10^{-m}[/math]
Why are you adding the condition [math]n\geq i[/math] here? Also if you were to add that condition it should go after the [math]\forall i[/math].

>This follows because we know that [math]a_n + 10^{-m}[/math] is an upper bound for the entire set (and consequently all subsequences). [math]b_i[/math] can't be equal to [math]a_n + 10^{-m}[/math] otherwise it wouldn't be a lower bound
It's possible for the upper bound of a set to equal the lower bound. It can't happen here because we know more than just that [math]a_n + 10^{-m}[/math] is an upper bound; it is strictly greater than every element in the sequence.

Also I realize I wrote something incorrectly in >>16145731. Instead of
[math]a_n - 10^{-m} \leq \sup \{b_i\} \leq a_n + 10^{-m}[/math]
what I intended was
[math]a_n - 10^{-m} \leq \sup \{b_i | i \in \mathbb{N} \} \leq a_n + 10^{-m}[/math].';

'>>16147379
>Why are you adding the condition [math]n \geq i[/math]
So would it be ok if I dropped the condition?
>It's possible for the upper bound of a set to equal the lower bound.
I see that, but if [math]b_i = a_n + 10^{-m}[/math] then [math]a_n[/math] would be less than the greatest lower bound which is contradictory.';

'Bump';

'>>16147439
>So would it be ok if I dropped the condition?
Well, adding a condition means proving a weaker statement than what we wanted to prove. So we want to drop the condition, but that also means the proof of the stronger statement can't use the condition.
>I see that, but if [math]b_i = a_n + 10^{-m}[/math] then [math]a_n[/math] would be less than the greatest lower bound which is contradictory.
If we want to prove this without adding a condition [math]n \geq i[/math], then [math]a_n[/math] isn't necessarily a member of the set.';

'>>16148058
For all [math]i[/math] we have that [math]b_i \leq a_i < a_n + 10^{-m}[/math].';

'>>16148058
Also, [math]\sup \{b_i | i \in \mathbb{N} \} \leq a_n + 10^{-m}[/math] because of the inequality:
[math]b_i < a_n + 10^{-m}[/math].
If [math]\sup \{b_i | i \in \mathbb{N} \} > a_n + 10^{-m}[/math] then [math]\sup \{b_i | i \in \mathbb{N} \}[/math] wouldn't be the least upper bound for [math]b_i[/math] as we know that [math]\forall i, b_i < a_n + 10^{-m}[/math].';

'>>16146653
based';

'Bump';

'Bump';

'>>16148202
Alright, we also need to cover
[math]a_n - 10^{-m} \leq \sup \{b_i | i \in \mathbb{N} \}[/math]
but that should be easy.

Then let's go back to A1.5.
We'll need to show that for any integer m there exists an integer k such that
[math]a_i = f([{\bf x}]_{-(k+i)})[/math]
satisfies
[math]|a_i - a_j| < 10^{-m}[/math] for all [math]i, j \in \mathbb{N} = \{0,1,2,\ldots\}[/math].

Also, continuing to let [math]b_i = \inf_{j \geq i} a_j[/math], we need to show
[math]\sup_j \inf_{i \leq -j} f([{\bf x}]_i) = \sup \{b_i | i \in \mathbb{N} \}[/math].';

'>>16149496
[math]a_n - 10^{-m} \leq b_i \leq \sup \{b_i | i \in \mathbb{N} \}[/math].

As the function [math]f[/math] is [math]\mathbb{D}[/math]-continuous it is true that for any [math]m[/math] there exists [math]k[/math] such that if the inputs are k-close, the outputs are m-close. For all [math]i, j \in \mathbb{N}[/math] we have [math]|[{\bf x}]_{-(k+i)} - [{\bf x}]_{-(k+j)}| < 10^{-k}[/math] as they are the same number truncated at at most the digit corresponding to [math]10^{-k}[/math] so they can't be further than that apart. So by continuity, for [math]a_i = f([{\bf x}]_{-(k+i)})[/math] we have [math]|a_i - a_j| < 10^{-m}[/math].

Isn't that last statement by definition?';

'>>16149621
There exists [math]i \in \mathbb{N}[/math] so
>[math]a_n - 10^{-m} \leq b_i \leq \sup \{b_i | i \in \mathbb{N} \}[/math]
Yes.

>As the function [math]f[/math] is [math]\mathbb{D}[/math]-continuous it is true that for any [math]m[/math] there exists [math]k[/math] such that if the inputs are k-close, the outputs are m-close.
First, it's not correct to use k-close as a synonym for "corresponding numbers are less than [math]10^{-k}[/math] apart." They are non-equivalent statements, and "k-close" is the more complicated, uglier one which we should avoid using where possible. Second, even with that substitution (which I would not expect to affect the truth of the statement), the statement is not true. In particular, it is false for finite decimal multiplication. We need to use the whole definition and not skip parts of it, or we don't have a proof.

>Isn't that last statement by definition?
No, in [math]\sup_j \inf_{i \leq -j} f([{\bf x}]_i)[/math], the [math]j[/math] runs over all integers. So we have to show this doesn't change the result.';

'>>16149946
I don't see what's missing?';

'>>16150069
You're missing the "with all [math]|x_i|, |y_i| < N[/math]" part.';

'>>16150073
So if we replace the k-close statements with the corresponding [math]< 10^{-k}[/math] statements and also require that [math]|x_i| < N[/math] then my proof works?';

'>>16149946
>No, in [math]\sup_j \inf_{i \leq -j} f([{\bf x}]_i)[/math], the [math]j[/math] runs over all integers. So we have to show this doesn't change the result.
So we have to show it's the same whether it is all integers or all natural numbers?';

'>>16150094
If you add conditions then you're proving a different theorem.

>>16150096
You have the general idea, but you should try substituting [math]a_i = f([{\bf x}]_{-(k+i)})[/math] and [math]b_i = \inf_{j \geq i} a_j[/math] into [math]\sup \{b_i | i \in \mathbb{N} \}[/math] to see precisely what we get.';

'>>16150192
What conditions are being added that aren't already in the theorem?';

'>>16150347
I assumed you meant "add a condition [math]|x_i| < N[/math] to the theorem we are trying to prove."';

'>>16150354
Isn't that already in the proposition? So what's left?';

'>>16150364
What we're trying to prove right now is the second part of >>16149496. This will be useful not just for proving the continuity condition, but also for proving that the infimums and supremums in the definition of [math]\tilde{f}[/math] exist in the first place.';

'>>16150439
Ok, what about the proof here >>16149621 if we ignore the first sentence and go with:
Let [math]N = 1+2\lceil |x_1|+...+|x_n|\rceil[/math]. (I got the idea for N from another thread). For all [math]i, j \in \mathbb{N} we have [math]|[{\bf x}]_{-(k+i)} - [{\bf x}]_{-(k+j)}| < 10^{-k}[/math] as they are the same number truncated at at most the digit corresponding to [math]10^{-k}[/math] so they can't be further than that apart. So by continuity, for [math]a_i = f([{\bf x}]_{-(k+i)})[/math] we have [math]|a_i - a_j| < 10^{-m}[/math].';

'>>16150464
This kind of approach will work but there's an issue with the choice of N; the [math]x_i[/math] are infinite decimals, and we haven't defined addition involving infinite decimals yet.';

'>>16150481
So would it work if they were all k-truncated?';

'>>16150505
To what k?';

'>>16150505
>>16150506
But to answer the question, yes, truncating them ought to work, assuming you don't make a silly choice like using [math][x_i]_j[/math] with j > 0. But the addition which is causing the problem isn't really needed anyway. Probably the simplest thing would be to just use
[math]N = \max \{|[x_1]_0|, \ldots, |[x_n]_0|\} + 2[/math].

If you meant k from "there exists k" in >>16149621, then that value isn't available since it depends on N.';

'>>16150685
So if we go with your choice about truncating them at 0 we don't have to worry about confusing k. I'm confused about the quantifier "for any N" in the proposition as this is just one N. How do we know it is satisfied for any N?';

'>>16150722
We're not trying to prove a "for any N, ..." statement at the moment. We are currently proving the statements in >>16149496 given that f is [math]\mathbb{D}[/math]-continuous (I should have mentioned that necessary condition in that post, my mistake), which means that we know that a statement of the form "for any N, ..." is true. Since this statement is true for any N, it is true for a specific N.';

'>>16150728
So it remains to prove the final statement in that post?';

'>>16150759
Yes. Then after that would be proving the continuity condition in A1.6.';

'>>16150764
How do we even know that [math]\sup_j \inf_{i \leq -j} f([{\bf x}]_i)[/math] exists for all integers j? I mean how do we know the [math]f([{\bf x}]_i)[/math] are bounded? Earlier we assumed the j was large enough such that there was m where all the values were within [math]10^{-m}[/math].';

'>>16150788
For showing the infimums exist, the argument given earlier (with the fix of choosing N) should still work. We know there is a k such that [math]\{f([{x}]_i) | i \leq -k\}[/math] is bounded, and for any other j, [math]\{f([{x}]_i) | i \leq -j\}[/math] contains at most finitely many additional elements, so it is also bounded.

I'm not sure if we ever proved that the supremum of the infimums exist, but proving this can be easily combined with the third part of >>16149496. That is, we need to show [math]\sup \{b_i | i \in \mathbb{N} \}[/math] is an upper bound for [math]\{\inf_{i \leq -j} f([{\bf x}]_i) | j \in \mathbb{Z}\}[/math] and that it is its least upper bound.';

'>>16150818
>I'm not sure if we ever proved that the supremum of the infimums exist
How about using the fact that:
[math]a_n - 10^{-m} \leq b_i \leq a_n + 10^{-m}[/math]
and the least upper bound property of real numbers that every nonempty subset of the real numbers that has an upper bound has a least upper bound.';

'>>16151402
Sorry, that last inequality should be strict.';

'>>16151402
>>16151403
That shows the supremum of [math]\sup \{b_i | i \in \mathbb{N} \}[/math] exists, but we still need to show that the supremum of [math]\{\inf_{i \leq -j} f([{\bf x}]_i) | j \in \mathbb{Z}\}[/math] exists and is the same thing.';

'>>16150818
How do we know the set of [math]\{f([{\bf x}]_j) | j \in \mathbb{Z}\}[/math] is bounded? Specifically how do we know that [math]\{f([{\bf x}]_j) | j \in \mathbb{Z}, j < 0\}[/math]? We saw earlier how it can be shown for [math]j \geq 0[/math] by using arguments of [math]\mathbb{D}[/math]-continuity and adding finitely more elements to the set, but here we add an infinity of elements.';

'>>16152046
Sorry, I meant [math]\{f([{\bf x}]_j) | j \in \mathbb{Z}, j > 0\}[/math].';

'>>16152047
And
>We saw earlier how it can be shown for [math]j \leq 0[/math].';

'>>16152046
>>16152047
>>16152048
I don't think we strictly need to prove [math]\{f([{\bf x}]_j) | j \in \mathbb{Z}\}[/math] is bounded here, but if you want to go that route, notice that you're not actually adding an infinity of elements because most of the [math][{\bf x}]_j[/math] are the same.';

'>>16152138
Oh, so there will be a finite number that involve adding/zeroing new digits?';

'>>16152403
Yes.';

'>>16152864
So we need to show that the infima of the expanded set are not any bigger than the infima of the set with just [math]j < 0[/math]?';

'>>16152972
>with just j < 0?
j < 0 is the wrong condition here; as I said in >>16150192, plug those things in and see what you actually get.';

'>>16153309
[math]\sup \{b_i | i \in \mathbb{N} \} = \sup \{\inf_{j \geq i} a_j | i \in \mathbb{N} \} = \sup \{\inf_{j \geq i} f([{\bf x}]_{-(k+i)}) | i \in \mathbb{N} \}[/math]. I'm not sure what I'm supposed to get though, we don't have any values.';

'>>16153362
Or maybe better written as:
[math]\sup \{b_i | i \in \mathbb{N} \}[/math]
[math]\sup \{\inf_{j \geq i} \{a_j\} | i \in \mathbb{N} \}[/math]
[math]\sup \{\inf_{j \geq i} \{f([{\bf x}]_{-(k+i)})\} | i \in \mathbb{N} \}[/math]';

'>>16153362
>>16153368
There's a mistake, it should be:

[math]\sup \{b_i | i \in \mathbb{N} \}[/math]
[math]\sup \{\inf_{j \geq i} \{a_j\} | i \in \mathbb{N} \}[/math]
[math]\sup \{\inf_{j \geq i} \{f([{\bf x}]_{-(k+j)})\} | i \in \mathbb{N} \}[/math]';

'>>16153371
That [math]j \geq i[/math] should go inside the curly braces:
[math]\sup \{\inf \{f([{\bf x}]_{-(k+j)}) | j \geq i\} | i \in \mathbb{N} \}[/math]

We can simplify a little by shifting the i and j indices.';

'>>16153375
and that is to be compared with
[math]\sup_j \inf_{i \leq -j} f([{\bf x}]_i)[/math].';

'>>16153395
Yes. It is worth doing the shift in >>16153375 (and then a sign flip) to make these expressions look as similar as possible.';

'>>16153395
or [math]\sup \{\inf \{f([{\bf x}]_i) | i \leq -j \} | j \in \mathbb{Z} \}[/math]';

'>>16153375
Shifting them by k?';

'>>16153408
Yes.';

'>>16153413
Ok, so we have:
[math]\sup \{\inf \{f([{\bf x}]_{-j}) | j \geq i + k\} | i \in \mathbb{N} \}[/math]';

'>>16153417
Then
[math]\sup \{\inf \{f([{\bf x}]_j) | j \leq -i - k\} | i \in \mathbb{N} \}[/math]';

'>>16153420
Relabelling:
[math]\sup \{\inf \{f([{\bf x}]_i) | i \leq -n - k\} | n \in \mathbb{N} \}[/math]';

'>>16139007
"Real" numbers don't exist (= aren't well defined) anyways.
https://njwildberger.com';

'>>16153425
And we can also shift the n.';

'>>16153447
[math]\sup \{\inf \{f([{\bf x}]_i) | i \leq -p\} | p \in \mathbb{N}, p \geq k \}[/math]';

'Retarded schizo nonsense';

'>>16153518
Exactly, although we never required [math]k \geq 0[/math] so it should properly be [math]p \in \mathbb{Z}, p \geq k[/math].

We need to show this is equal to
[math]\sup \{\inf \{ f([{\bf x}]_i) | i \leq -j \} | j \in \mathbb{Z} \}[/math].';

'>>16153543
So
[math]\sup \{\inf \{f([{\bf x}]_i) | i \leq -p\} | p \in \mathbb{Z}, p \geq k \}[/math]
Are we supposed to show it's the same if we add the elements for [math]p < k[/math]?';

'>>16153607
Exactly.';

'>>16153621
For smaller p we have that [math]f([{\bf x}]_i)[/math] is evaluated at larger i. So if these larger i produce smaller values of the function then the set that includes these values will have infimum on these values. So these infima will be smaller than the infima of the smaller set, therefore they can't be the supremum. If these larger i produce larger values then they won't be infima.';

'>>16153639
Looks good. Now we should be able to combine our results so far to say:
If f is a [math]\mathbb{D}[/math]-continous function from [math]\mathbb{D}^n[/math] to [math]\mathbb{D}[/math], then for every integer m there exists an integer k such that for every [math]i \leq -k[/math] we have
[math]f([{\bf x}]_i) - 10^{-m} \leq \tilde{f}({\bf x}) \leq f([{\bf x}]_i) + 10^{-m}[/math].';

'>>16154268
Oh cool. Thanks for the help.';

'>>16154370
From there it's not too hard to get the continuity condition in A1.6. Basically we need to show [math]\tilde{f}({\bf x})[/math] and [math]\tilde{f}({\bf y})[/math] are close because [math]\tilde{f}({\bf x})[/math] is close to some [math]f([{\bf x}]_i)[/math] which is close to [math]f([{\bf y}]_i)[/math] which is close to [math]\tilde{f}({\bf y})[/math].';

'>>16154379
I suppose we use the inequalities here >>16145731';

'>>16154414
Well, we use those to get >>16154268. In particular, the last inequality. Do you see how it works? You should do the appropriate substitutions yourself to verify that the last inequality in >>16145731 turns to the inequality in >>16154268.';

'>>16154940
Yeah I see how it works. Isn't that what the last flurry of posts was proving?';

'>>16154268
The m here seems rather arbitrary. This can be whatever we want righh and there exists a k by [math]\mathbb{D}[/math]-continuity?';

'>>16156094
Yes.';