feat(Topology/Algebra/Order): regular grid helpers and piecewise linear interpolation

[Vilin97]

Make API for piecewise linear interpolation on regular grids. I need these to for ODE time-stepping methods, like forward Euler, and later Runge–Kutta methods.

Follow-up PR: #35755 (forward Euler method convergence).

I don't know if these numerical analysis ODE-solving methods even belong in mathlib. If someone could advise me on it, I would appreciate it.

---

The initial proof was produced by Aristotle. The code was iteratively refined (factoring out lemmas, golfing, simplifying proofs) using Claude Code.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 47ed25d3ca

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Algebra.Order.PiecewiseLinear (new file)	1818

---

Declarations diff

+ continuous_of_regularGrid
+ continuous_piecewiseLinear
+ hasDerivWithinAt_piecewiseLinear
+ locallyFinite_Icc_regularGrid
+ piecewiseLinear
+ piecewiseLinear_apply_grid
+ piecewiseLinear_eq_on_Ico

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[Copilot]

Pull request overview

This PR adds helper lemmas for working with regular grids and defines piecewise linear interpolation on such grids. It extends Topology/Algebra/Order/Floor.lean with four new theorems relating Nat.floor to membership in regular grid intervals, and introduces a new file Topology/Algebra/Order/PiecewiseLinear.lean containing definitions and lemmas for piecewise linear and piecewise constant interpolation.

Changes:

• Added grid-related helper lemmas to Floor.lean that characterize when points belong to regular grid intervals
• Introduced piecewiseLinear and piecewiseConst functions with evaluation, continuity, and derivative results
• Added new file to the module import list in Mathlib.lean

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
Mathlib/Topology/Algebra/Order/Floor.lean	Adds RegularGrid section with 4 theorems: Nat.floor_div_eq_of_mem_Ico, mem_Ico_Nat_floor_div, locallyFinite_Icc_grid, and ContinuousOn.of_Icc_grid
Mathlib/Topology/Algebra/Order/PiecewiseLinear.lean	New file defining piecewise linear/constant interpolation with 6 main theorems about evaluation, continuity, and derivatives
Mathlib.lean	Adds public import for the new PiecewiseLinear module

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[grunweg]

Another high-level question: is it important to have regularly spaced grids, or do application also consider other grids? (I'm not a numerical analyst, but the answer will influence the PR!) If the latter, can you generalise your PR accordingly?

[Vilin97]

@grunweg , good question! In my experience, regular grids are used 99.9% of the time. Many theorems in NA of ODEs are of the form "If $\Delta t < X$, then Y" or "As $\Delta t \to 0$, Y follows". For a specific example of this, the very first theorem in most NA textbooks is the convergence of the Forward Euler Method, which states "As $\Delta t \to 0$, the numerical solution converges to the true solution of the ODE" -- I formalized it in my second PR that depends on this PR.

[Vilin97]

Thank you, all. Claude and I

• weakened the typeclass assumptions on K from a field to an Archimedean ordered additive group (as per Eric's suggestion)
• changed the indices from \N to \Z, which allowed for slightly easier proofs
• tagged piecewiseLinear_apply_grid with @[simp]

[Vilin97]

@botbaki review

[botbaki-review]

@Vilin97 Here's my review of this PR at commit 578863b3:

[j-loreaux]

I understand that your motivation for this is numerical analysis, and I saw your response to @grunweg about regularity, but I would prefer if we did not require regularity here for two primary reasons:

1. In some cases within numerical analysis, one does not require / need regular grids, and so this is an unnecessary assumption. Such unnecessary assumptions have a habit of coming back to bite you. Just imagine, someone wants irregular grids in the future, and they have to completely rework the definition of grids just to state their result.
2. I would like to use piecewiseLinear for things other than numerical analysis (e.g., building piecewise linear functions for use with the continuous functional calculus), and in that case we will definitely not want them to be regular.