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
This is part of #25140, and is the special case of Hahn embedding theorem applied to archimedean group. The construction is rather unpleasant as it uses explicit Cauchy sequence with essentially the binary representation of numbers, but I haven't found a better way to do this. Rewritten with Dedekind cut
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
I don't really know how difficult this is to implement, but in informal mathematics, I would start attacking this problem by attaching to each element m the set of rational numbers a/b such that a/b • one < m, interpreted as a • one < b • m. By the archimedean property, this set has an upper bound, and we can assign the least upper bound as a real number. This approach may produce more reusable intermediate results (or have parts that are already implemented).
I got most of the proof with the new approach, except for one sorry left. It looks like something obvious but it might take me a while to figure out figured it out, though that particular part is not pretty
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is part of #25140, and is the special case of Hahn embedding theorem applied to archimedean group.
The construction is rather unpleasant as it uses explicit Cauchy sequence with essentially the binary representation of numbers, but I haven't found a better way to do this.Rewritten with Dedekind cut