feat(ForMathlib): index-image diameter bound (2/4) - #14
Merged
Merged
Conversation
This was referenced Jun 19, 2026
Stacked on 1/4. Adds the ceiling-subadditivity helper `ceil_natCast_mul_le_ceil_natCast_mul_add` (introduced here, next to its first use) and `ncard_index_image_le_of_diam_le`: a set of diameter `≤ r` meets at most `(2⌈n·r⌉₊ + 1)ᵈ` grid cells. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Collaborator
|
Merge with master |
| /-- **Bounded-diameter cell incidence.** A set `T ⊆ ι → ℝ` of diameter `≤ r` meets at most | ||
| `(2⌈n·r⌉₊ + 1)ᵈ` cells of the `n⁻¹ℤ^ι` grid, i.e. its `index n`-image has at most that many | ||
| points. (Here `ι → ℝ` carries the sup metric, so a cube of side `1/n` has diameter `1/n`.) -/ | ||
| theorem ncard_index_image_le_of_diam_le (n : ℕ) [NeZero n] {T : Set (ι → ℝ)} {r : ℝ} |
Collaborator
There was a problem hiding this comment.
Is NeZero n really needed? Same for hr.
Owner
Author
There was a problem hiding this comment.
Done in fcf600f (and 22b3aac on development) — neither is needed:
NeZero n: mathlib definesunitPartition.indexfor everyn(index_applyis even stated for an arbitrarym : ℕwith no instance), and atn = 0the statement is trivially true —index 0 x = fun _ ↦ -1, so the image has at most one point while the RHS is1. The one proof covers it uniformly, no case split needed.hr : 0 ≤ r: onceTis nonempty it follows from the diameter hypothesis (Metric.diam_nonneg.trans hdiam), and the empty case was already discharged bysimp. It is now ahaveinside the proof.
(After the master merge the lemma also carries its own [Fintype ι] binder — the section-level instance was generalised away during the #13 review.)
Collaborator
|
Can you have a look at my comment? Also, isn't this PR to merge into master? |
- ncard_index_image_le_of_diam_le: NeZero n is unneeded (index is total and the n = 0 bound is trivially true); 0 <= r now derived inside the proof via Metric.diam_nonneg once T is nonempty (riccardobrasca, PR 14) - lemma now carries [Fintype i] itself since the master merge removed the section-level instance (generalised away in the PR 13 review) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Owner
Author
|
Both done:
|
CBirkbeck
added a commit
that referenced
this pull request
Jul 9, 2026
…o [Finite ι] Per @xroblot's review (PR #13): put each private helper next to its first use, and weaken `setFinite`'s hypothesis. - `setFinite_index_image_of_isBounded` now takes `[Finite ι]`, recovering `Fintype` via `Fintype.ofFinite` inside the proof — dropping the `set_option linter.unusedFintypeInType false` workaround (the conclusion never mentions `Fintype.card`). - `ceil_natCast_mul_le_ceil_natCast_mul_add` moved next to its only consumer `ncard_index_image_le_of_diam_le`; `abs_sub_le_one_div_of_ceil_natCast_mul_eq` next to `ncard_index_image_chart_le`. This re-slices the stack so each helper lands in the PR that first uses it (#14, #15) instead of #13. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
Adds the ceiling-subadditivity helper
ceil_natCast_mul_le_ceil_natCast_mul_add(introduced here, next to its first use per @xroblot's review) andncard_index_image_le_of_diam_le: a set of diameter≤ rmeets at most(2⌈n·r⌉₊ + 1)ᵈcells of then⁻¹ℤ^ιgrid.Builds green on the
v4.31.0-rc1/ mathlib-master pin.🤖 Generated with Claude Code