PR summary d51b0adb3d

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

./scripts/technical-debt-metrics.sh pr_summary

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

After comparing with existing code, I decided to make a few changes

• rename to trunc (similar to PowerSeries.trunc)
• upgrade the base trunc to a ZeroHom, similar to HahnSeries.single
• also add the AddMonoidHom version
• manual simp lemma to get the correct name (though this ended up creating ambiguity with PowerSeries.coeff_trunc in LaurentSeries.lean where both HahnSeries and PowerSeries are opened, so I marked the new one with protected

Sorry for making big change after review

@YaelDillies sure, let me see if I can explain this well...

The proof I am following is https://www.ams.org/journals/proc/1952-003-06/S0002-9939-1952-0052045-1/. (The proof shown there is for a special case where the ordered group is a real vector space. Generalization is explained here). The truncation operation is called "cut" on page 980.

The proof is a process of transfinite induction starting from a partial map and adding new elements to the domain (Theorem 3.2). Whenever a new element is added, one needs to assign appropriate output to that element and preserve desired properties (strict monotone & linear). This turns out pretty hard on its own (maybe impossible?), so one strengthen the induction hypothesis with an extra condition on the partial map $F$:

• if $f \in Range(F)$, then $Trunc(f, \Gamma) \in Range (F)$ for all $\Gamma$

Because of linearity of $F$, this can be rephrased in terms of the upward truncation $Trunc'(f, \Gamma) = f - Trunc(f, \Gamma) \in Range (F) $. I doubt that it will make the proof simpler, though.

This condition means that all values of $F$ is a limit point of a sequence by progressively adding more terms. It goes hand-in-hand with how $F(x)$ for a new element $x$ is chosen: we progressively add terms to $F(x)$ equal to a neighbor $F(y)$ in a ball defined by Archimedean class. if there is no such neighbor $y$ with $F(y)$ defined, we stop adding more terms to $F(x)$ and leave the rest as zero. One can then show that $F(x)$ respects the order embedding: as $x$ slightly deviates from $y$, $F(x)$ does so from $F(y)$ in the same direction.

Don't forget to remove awaiting-author if you want me to look at a PR again!

@YaelDillies Thanks for the reminder. Could you take a look now?

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

✌️ wwylele can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

:/ another weird CI error. Going to merge from master

bors r+

Pull request successfully merged into master.

Build succeeded:

• CI Success