[codex] Add finset supremum and infimum convergence lemmas - #8
Draft
CoolRmal wants to merge 1303 commits into
Draft
[codex] Add finset supremum and infimum convergence lemmas#8CoolRmal wants to merge 1303 commits into
CoolRmal wants to merge 1303 commits into
Conversation
CoolRmal
changed the title
CoolRmal
force-pushed
the
codex/tendsto-finset-sup-isup
branch
5 times, most recently
from
June 14, 2026 09:08
ddb55b8 to
7602123
Compare
Teaching tactic: `assume p` is short for `intro (_ : p)`. Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
…-community#39269) Adds `spectrum.resolvent_sub_resolvent`: For `a b : A` in an `R`-algebra and `r` in the resolvent set of both, `resolvent a r - resolvent b r = resolvent a r * (a - b) * resolvent b r`. Companion to `spectrum.resolvent_eq`.
…unity#42173) ... and syntactically generalise `{I : Finset ι}` to `{I : Set ι} (hI : I.Finite)`. The new proofs also happen to not abuse the `Set α := α → Prop` defeq.
…ver-community#39818) This pr adds the functionality to transfer Lie brackets along equivalences (additive, linear and plain ones). I followed the scheme of the existing `TransferInstance.lean` file. For one of the proofs, I also needed `linearEquiv_apply `, which seemed missing so I added it. AI use disclaimer: I used claude to search for lemmas/ understand error messages / proofreading and feedback, but wrote the whole code myself.
…#41701) The old proof abuses defeq in a subtle way, which makes painful reading for the kernel. This one is easier to swallow.
…leanprover-community#41707) `cache get` downloads files in multiple rounds (corresponding to azure containers, e.g. `master` then `forks` for a fork PR) and decompresses them in a pipeline while the download streams. Each round started from a fresh pipeline state and the round loop kept only the last round's state, so some files queued for decompression plus the in-flight leantar batch was dropped: the .ltars were on disk but never unpacked, and the next lake build recompiled those modules. The in-flight leantar was also never awaited, so it could still be writing build outputs while lake build read them. Reported in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/cache.20issues/with/609923362 The fix makes the pipeline state an explicit value threaded through the rounds: a DecompState structure (pending files, in-flight batch, counters) embedded in TransferState, and finalizeDecomp drain after the last round. Also adds related tests in Cache/Test.lean.
) Project started during the May 2026 workshop "Techniques and Tools for the Formalization of Analysis" at ICERM. Co-authored-by: Jon Bannon <jbannon@siena.edu> Co-authored-by: Yongxi (Aaron) Lin <aaronlin@andrew.cmu.edu> Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
…community#42038) They should not be instance reducible (their entire raison d'être is to be a type synonym to disambiguate typeclass synthesis), but they can be implicit_reducible just fine. This allows removing another 10-20 backcompat options.
…group homs `G → H` (leanprover-community#41995) ... for abelian groups `G` and `H`. Furthermore, the convolution product on bialgebra homs corresponds to pointwise addition on group homs. Also generate more lemmas through `to_additive`, remove some unused `set_option`s and relocate `MonoidAlgebra.toAdditive`/`AddMonoidAlgebra.toMultiplicative` to existing sections. From Toric
…-community#42199) In the review of leanprover-community#42173, it was asked if the `have` in `Matrix.ker_diagonal_toLin'` could be removed. This PR does so, and is a bit faster.
…2114) This complements the existing `isOpen_Ioo`. Co-authored-by: NoahW314 <noahwalker3.14@gmail.com>
Notation: - `K∞` : `NumberField.InfiniteAdeleRing K`; - `𝔸ᶠ[R, K]`: `IsDedekindDomain.FiniteAdeleRing R K`; - `𝔸[R, K]` : `NumberField.AdeleRing R K`; - specialisations `𝔸ᶠ[K]` and `𝔸[K]` to `R = RingOfIntegers K`.
…eanprover-community#42212) Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
…es (leanprover-community#41978) Add the `Finite` analogue for `induction_subsingleton_or_nontrivial`.
…y#40879) We prove various lemmas about the `smallInductiveDimension` of a topological space, as well as interactions with the `HasSmallInductiveDimensionLT` and `HasSmallInductiveDimensionLE` typeclasses.
Inspired by leanprover-community#42205. I searched for ` _ _ _]` in vscode and manually went through all ~25 and see if they could be removed (and in some cases some minor style improvement). For ` _ _]` it is already over 100, so that work ought to be automatised Co-authored-by: Batixx <s59fpern@uni-bonn.de>
…ces (leanprover-community#42222) `inferInstance` works in place of `inferInstanceAs` in both places. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/583339-AI-authored-projects/topic/Comparator-related.20import.20subtleties/with/613349677)
…anprover-community#41654) The additive lemma states `(mk g).out = g + h`, so by the `to_additive` naming convention its name should end in `add`, not `mul`. Rename it to `QuotientAddGroup.mk_out_eq_add` (a copy-paste error inherited from mathlib3) and deprecate the old name.
) This is just a general good practice these days. Two specific reasons are: - the module system makes thing faster, for example by reducing how much stuff has to be imported. - In the long run, we want to only support the module system, and not any non-module system uses of mathlib. leanprover-community#41950 signals this. That way, we can use no_expose, without needing to worry about uses without the module system where the definition will be exposed anyways. The migration is mostly mechanical, akin to what `modulize.lean` would do: make all imports `public`, and add `@[expose] public section` at the beginning of each file. (In a few cases of files without definitions, omit the expose attribute.) Inspired by leanprover-community#36236; re-done by hand. All files omitted there are actually fine to hand-convert.
…onway_99` (leanprover-community#42233) Kevin's Claude noticed that the `proof_wanted` for `conway_99` is misformalized. It asserts the existence of a simple graph `g` but then refers to the variable `G`. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…over-community#41248) This PR deprecates `NumberTheory/RamificationInertia/Basic.lean` in favor of `RingTheory/RamificationInertia/Basic.lean`. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
leanprover-community#42514) We have separate theorems for `ℤ` and `ℚ`, but one is enough for all rings.
…or `JordanHolderLattice` (leanprover-community#42556)
* Remove trailing underscores in names `simps`-errors would erroneously print * Restore Lean 3 error message tests.
… of composition products (leanprover-community#42292) This PR resolves the TODO in this file by adding `rnDeriv_measure_compProd_right` and `rnDeriv_measure_compProd`, which replace `∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η)` by `∂κ/∂η` under the suitable assumptions.
…prover-community#42075) `Mathlib.Util.MemoFix` is directly removed since all deprecations in it are more than 6 months old. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
This PR defines the continuous version of `PositiveLinearMap` via `extend`ing this structure as well as `ContinuousLinearMap`. In the process, we also create `Is{Add,Zero,SMul}Apply` instances for `PositiveLinearMap`.
…anprover-community#33664) - Define PointedCone.IsFaceOf, for a pointed cone being a face of another pointed cone. - Prove some basic properties, that faces are extreme sets of their cone, and how they behave under intersection, map and product operations. - Define `Face` by bundling the `IsFaceOf` structure, and show the complete lattice structure on it. - Prove that taking the product of two faces is an order isomorphism. Co-authored-by: Martin Winter Co-authored-by: ovi <ovi@posteo.de> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: M. Winter <112132359+martinwintermath@users.noreply.github.com>
…ty#41154) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…niverses (leanprover-community#41244) For theorems involving a category `C : Type u` (with `Category.{v} C`), the smallness assumptions or the existence of limits/colimits are expressed relative to an arbitrary universe `w` (instead of `w = v`), provided the assumption `LocallySmall.{w} C` is added. (This makes this more coherent with the API about locally presentable/accessible categories.)
…esults (leanprover-community#40510) This PR reorganizes the Topology/EMetricSpace/Defs so that various results that previously only held for `PseudoEMetricSpace` now also hold for `WeakPseudoEMetricSpace` (in particular, `ENNReal`). This is a necessary stepping stone to generalise many definitions and theorems to `WeakPseudoEMetricSpace`. Co-authored-by: Batixx <s59fpern@uni-bonn.de>
…eanprover-community#38965) If `X` is a simplicial set, `R₁ →+* R₂` is a morphism of commutative rings, and `M₁` is a `R₁`-module, then the chain complex of `R₂`-modules of `X` with coefficients in `R₂ ⊗[R₁] M₁` identifies to the extensions of scalars of the chain complex of `R₁`-modules of `X` with coefficients in `M₁`. In this file, we obtain a formulation of this result where the extension of scalars functor `ModuleCat R₁ ⥤ ModuleCat R₂` is replaced by an arbitrary functor `F : C ⥤ D` which commutes with coproducts. (As `SimplicialObject` is now an `abbrev` for a category of functors, `SimplicialObject.whiskering` is also made an abbrev here.)
…#42131) In this PR, we define a topology on the standard simplex `StdSimplex R M`. When `M` is finite, this is the topology that is induced by the embedding `StdSimplex R M → (M → R)`. In general, we use the supremum of the coinduced topologies for the maps `StdSimplex.map f : StdSimplex R ι → StdSimplex R M` where `f : ι → M` is a map from a finite set `ι`.
…42640) These changes concern the following four equivalences: ```lean variable {α β : Type*} example (e : α ≃ β) : Set α ≃ Set β := Equiv.Set.congr e -- No change example (e : α ≃ β) : Finset α ≃ Finset β := Equiv.finsetCongr e -- Rename to `Equiv.Finset.congr` example {s t : Set α} (h : s = t) : s ≃ t := Equiv.setCongr h -- No change example {s t : Finset α} (h : s = t) : s ≃ t := sorry -- Missing: add as `Equiv.finsetCongr` ``` In summary we essentially implement two changes: 1. Rename the existing `Equiv.finsetCongr` to `Equiv.Finset.congr` since it is currently inconsistent with both `Equiv.Set.congr` and `Equiv.setCongr` 2. Fill a gap by giving the the now-available `Equiv.finsetCongr` name to the `Finset` version of `Equiv.setCongr`
…2651) This PR updates the Mathlib dependencies.
…class assumptions (leanprover-community#42539) `IsReduced` and `NoZeroDivisors` can already be inferred from `LinearOrderedCommMonoidWithZero`. Co-authored-by: NoahW314 <noahwalker3.14@gmail.com> Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
This PR removes namespaces from `open` commands when no declaration of the scope uses them. Found the candidates with metaprogramming, then double checked file by file. The linter used for this itself is not proposed for adoption (the approach is prone to false positives) but these verified removals still stand. Unused `open` declarations carry two costs: they invite ambiguous-reference errors for later edits in the scope, and they misdescribe the dependencies of the file to readers. There is no performance effect. Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Removing.20unnecessary.20.60open.60.20declarations/with/613515627 Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Yongxi (Aaron) Lin <aaronlin@andrew.cmu.edu>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.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
20 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.
Summary
Adds finset-indexed monotone convergence lemmas for suprema and infima:
tendsto_finset_sup_iSupfor complete lattices.tendsto_finset_sup_ciSupfor conditionally complete lattices withOrderBot, assuming a nonempty index type and bounded-above range.tendsto_finset_inf_iInffor complete lattices.tendsto_finset_inf_ciInffor conditionally complete lattices withOrderTop, assuming a nonempty index type and bounded-below range.The conditional versions use the existing
tendsto_atTop_ciSupandtendsto_atTop_ciInftheorems after showing that the indexed supremum/infimum over finite folds agrees with the bounded supremum/infimum of the original family.Validation
lake env lean Mathlib/Topology/Order/MonotoneConvergence.leangit diff --checkEarlier,
lake env scripts/lint-style.py Mathlib/Topology/Order/MonotoneConvergence.leancrashed before checking this file withNameError: name 'nonterminal_simp_check' is not defined.