chore: LSP-verified proof-golf leftovers — Crossings, AntitoneLimit, EndpointCommon (−20)#113
Merged
Conversation
…endpoints
A dozen targeted simp/simpa/rfl collapses across three files. Each site
was probed individually rather than via blanket `exact?` (which tends to
time out on measure-heavy goals).
`Crossings/Bounds.lean`:
* L69 `congr 1; ext ω; exact ENNReal.ofReal_add ...` → `simp [ENNReal.ofReal_add]`.
* L72 `rw [lintegral_add_right ..., lintegral_const]; simp [...]` →
`simp [lintegral_add_right, lintegral_const, IsProbabilityMeasure.measure_univ]`.
* L78 eLpNorm-from-lintegral block (three lines) →
`simpa [Real.enorm_eq_ofReal_abs] using
(MeasureTheory.eLpNorm_one_eq_lintegral_enorm ...).symm`.
`Crossings/AntitoneLimit.lean`:
* L65 two-step `calc` (eLpNorm → ↑R) → `simpa [hR] using hL1_bdd n`.
* L103 `h_rev_eq` is now just `rfl` (definitional).
* L150 the `filter_upwards`/`unfold upcrossings`/`congr 1; ext M; congr 1;
apply upcrossingsBefore_congr` block collapses to a single
`simp [MeasureTheory.upcrossings, upcrossingsBefore_congr (fun k _ => hω k)]`.
* L225 / L237 / L270: three near-identical
`simp only [Xlim]; rw [dif_pos hω]; exact Classical.choose_spec hω`
blocks each collapse to `simpa [Xlim, hω] using Classical.choose_spec hω`.
`AlphaConvergence/EndpointCommon.lean`:
* L106 final 4-line `simpa using h_eq; linarith; rwa [this]` →
`have : L ω = c := sub_eq_zero.mp (abs_eq_zero.mp h_eq);
simpa [this] using h_ae`.
`AlphaConvergence/EndpointAtTop.lean` + `EndpointAtBot.lean` (parallel changes):
* `h_tendsto_ennreal` `have ... simp only [h_empty, measure_empty] at this; simpa ...`
collapses to a single
`simpa [h_empty, Function.comp] using
tendsto_measure_iInter_atTop (μ := μ) h_meas h_antitone h_fin`.
* The `ENNReal.toReal_zero` / `h_zero_ne_top` pair collapses to a single
`simpa using (ENNReal.continuousAt_toReal (by norm_num : (0:ENNReal) ≠ ⊤))
.tendsto.comp h_tendsto_ennreal`.
* The squeeze conclusion `refine ... ?_ ...; intro n; exact integral_nonneg ...`
collapses to a single term-mode `exact tendsto_of_tendsto_of_tendsto_of_le_of_le
tendsto_const_nhds h_indicator_tendsto (fun _ => integral_nonneg ...) h_contraction`.
Net: 5 files, +26 / −52 (−26 lines).
cameronfreer
force-pushed
the
golf-leftovers
branch
from
May 25, 2026 19:13
0d8edf0 to
2ec75e1
Compare
cameronfreer
changed the title
Reviewer feedback on the v1 PR landed 4 of the 12 sites in the "interesting attempt but not actually an improvement" bucket. Reverting those to keep the PR focused on the 8 wins that were endorsed. * `Bounds.lean` L78 — the `eLpNorm`-from-`lintegral` `simpa using (eLpNorm_one_eq_lintegral_enorm ...).symm` doesn't read more clearly than the original `rw`/`congr 1; ext ω; exact (Real.enorm_eq_ofReal_abs _).symm` and saves only one line; revert. * `EndpointAtTop.lean` + `EndpointAtBot.lean` — three parallel cleanups in each (the `tendsto_measure_iInter_atTop` simpa, the `ENNReal.toReal_zero` / `h_zero_ne_top` `simpa`, and the term-mode squeeze) save a line apiece but obscure the proof structure; revert all six. The 8 kept sites (`Bounds.lean` L69/L72, all 6 in `AntitoneLimit.lean`, and `EndpointCommon.lean` L106) remain unchanged.
cameronfreer
force-pushed
the
golf-leftovers
branch
from
May 25, 2026 19:19
2ec75e1 to
20c1ad4
Compare
3 tasks
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
1 participant
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.
Summary
Eight targeted manual simp/simpa/rfl collapses across three files, each LSP-probed before applying. Same shape as PR #112 — small, localized reductions in spots that the bulk autoGolf run from PR #16 either skipped or wasn't a good fit for.
Two-commit history: commit 1 contains the full v1 set of 12 attempts; commit 2 reverts the 4 the reviewer judged were not real improvements (kept in history for context).
Crossings/Bounds.lean(2 sites kept)congr 1; ext ω; exact ENNReal.ofReal_add (abs_nonneg _) (abs_nonneg _)simp [ENNReal.ofReal_add]rw [lintegral_add_right _ measurable_const, lintegral_const]; simp [...]simp [lintegral_add_right, lintegral_const, IsProbabilityMeasure.measure_univ]Crossings/AntitoneLimit.lean(6 sites kept)calc eLpNorm (...) ≤ ... = Rsimpa [hR] using hL1_bdd nh_rev_eqviaext n ω'; simp [...]rflfilter_upwards/unfold upcrossings/congr 1; ext M; congr 1; apply upcrossingsBefore_congr; intro k _; exact hω k(8 lines)filter_upwards [h_ae_eq] with ω hω; simp [MeasureTheory.upcrossings, upcrossingsBefore_congr (fun k _ => hω k)]simp only [Xlim]; rw [dif_pos hω]; exact Classical.choose_spec hωblockssimpa [Xlim, hω] using Classical.choose_spec hωAlphaConvergence/EndpointCommon.lean(1 site kept)have h_diff_zero ...; have : L ω = c; rwa [this] at h_aehave : L ω = c := sub_eq_zero.mp (abs_eq_zero.mp h_eq); simpa [this] using h_aeReverted in commit 2 (in v1 commit 1, then undone): the 3-line
eLpNorm-from-lintegralcollapse atBounds.lean:78, and the paralleltendsto_measure_iInter_atTop/ENNReal.toReal_zero/ term-mode squeeze cleanups in both endpoint files. Each saved a line but obscured the proof structure.Combined diff vs main: 3 files, +11 / −31 (−20 lines).
Test plan
lake buildclean (3527/3527 jobs) on the final HEAD#print axiomsondeFinetti,deFinetti_viaL2,deFinetti_viaKoopman— all[propext, Classical.choice, Quot.sound]lake exe checkdecls blueprint/lean_declspassespython3 blueprint/check_blueprint.py— 52 cites, 52 labels, 50 refs/uses, 52 lean_decls, all consistent