Conversation
First slice of the normLeOne frontier Lipschitz cover (formerly the whole-file PR #9, split into ~50-LOC stacked PRs). Adds `NormLeOneLipschitz.lean` with the generic `clampUnit` retraction onto the unit cube `[0,1]^ι` and its Lipschitz API: * `clampUnit`, `clampUnit_mem_Icc`, `clampUnit_eq_self` — the coordinatewise retraction and its fixed-point characterisation. * `lipschitzWith_clampUnit` (1-Lipschitz) and `exists_lipschitzWith_comp_clampUnit`. Stated for an arbitrary `Fintype ι` (no number field yet). The face charts and the frontier cover follow in the stacked slices 2/10–10/10. Wired into the umbrella import. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This was referenced Jun 18, 2026
|
|
||
| /-- The coordinatewise retraction of `ι → ℝ` onto the unit cube `Set.Icc 0 1`, given by | ||
| `Set.projIcc` in each coordinate. -/ | ||
| def clampUnit (ι : Type*) (c : ι → ℝ) : ι → ℝ := fun i ↦ (Set.projIcc 0 1 zero_le_one (c i) : ℝ) |
Collaborator
There was a problem hiding this comment.
Use a variable (ι : Type*) {c : ι → ℝ} line in this file. You may need variable (c) in for the def.
Owner
Author
There was a problem hiding this comment.
Done in 46a0903 — added variable (ι : Type*) {c : ι → ℝ} and used variable (c) in so c stays explicit for the clampUnit def, dropping the repeated binders from the lemmas. Module builds.
…iew) Per riccardobrasca's review on PR #19: declare `variable (ι : Type*) {c : ι → ℝ}` once instead of repeating the binders in every signature, with `variable (c) in` to keep `c` explicit for the `clampUnit` def. `c` becomes implicit in the lemmas (recoverable from the goal); the one internal use passes it by name. No statement content changes. 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
2 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.
Part 1 of 10 — the former whole-file PR #9 (
NormLeOneLipschitz.lean, ~670 lines), split into ~50-LOC stacked slices per review that PRs should be ~50 lines of Lean code. Each slice is anchored by a public result and builds green.The file gives a Lipschitz cover of the frontier of the
normLeOnefundamental region of a number field's mixed embedding — the geometric input the effective lattice-point count consumes. mathlib has the regionNumberField.mixedEmbedding.normLeOne(imported here) but not the Lipschitz structure of its frontier. Independent of the IndexImageCount/LatticePointCount stacks (mathlib-only imports), so this stacks directly onmaster.This slice adds the generic
clampUnitretraction onto[0,1]^ιand its 1-Lipschitz API (clampUnit,clampUnit_mem_Icc,clampUnit_eq_self,lipschitzWith_clampUnit,exists_lipschitzWith_comp_clampUnit). Stated for an arbitraryFintype ι. Wired into the umbrellaCebotarevDensityimport.The remaining slices: face charts (2) → boundary-in-faces (3–4) → realSpace cover (5) → phase bounds (6) → mixed-space lift (7–8) → bounded/fibre cover (9) → mixed-space headline + index variant (10).
Builds green on the
v4.31.0-rc1/ mathlib-master pin (identical tomaster's pin).🤖 Generated with Claude Code