Measure and integration
The Lean Pool projects whose card's first MSC2020 code is in class 28, Measure and integration: 5 articles, one per card.
TheoremA machine-checked bound of 0.6934 for Besicovitch's 1/2-problem#
Proves the planar Besicovitch threshold is at most 6934/10000, improving the published 7/10 record. The development formalizes the finite six-point reduction, thirty rational Gram certificates, the endpoint isolation argument, and Besicovitch's classical lower-bound example.
Quoted from the card LeanPool/projects/besicovitchs-1-2.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
LeanPool.Besicovitch.sigmaOne_plane_le_barS(theorem; a main declaration), declared in LeanPool/Besicovitch/Main/RationalBound.lean, line 32: “The planar one-dimensional rectifiability threshold is at most 6934/10000, improving the published upper bound 7/10.”LeanPool.Besicovitch.forcesOneRectifiability_plane_of_barS_lt(theorem), declared in LeanPool/Besicovitch/Main/RationalBound.lean, line 26: “Every threshold strictly above 6934/10000 forces countable one-rectifiability in the plane.”LeanPool.Besicovitch.Example.one_half_le_sigmaOne_plane(theorem), declared in LeanPool/Besicovitch/Example/LowerBound.lean, line 102: “The planar threshold is at least one half, witnessed by Besicovitch's purely unrectifiable example.”LeanPool.Besicovitch.weightedPairScore_le_of_separated(theorem), declared in LeanPool/Besicovitch/SixPoint/GramWeightedBound.lean, line 33: “Thirty exact rational Gram certificates prove the weighted six-point score is at most -1/2000 for every separated admissible pair in the unit ball.”
Project
- Authors: Yongxi Lin.
- Source: The bound sigma_1(R^2) <= 6934/10000 for Besicovitch's 1/2-problem by Yongxi Lin.
- Project repository: CoolRmal/Besicovitchs-1-2, at commit 17c9597b.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 28A75, 28A78, 49Q15, 68V20, 90C05.
- In Lean Pool: LeanPool/Besicovitch, from the card LeanPool/projects/besicovitchs-1-2.yaml.
Sources
TheoremBicausalOT: measurable selection and coupling strategies#
Develops Kuratowski–Ryll-Nardzewski selection, Jankov–von Neumann uniformization, and finite-horizon Bellman identities for locally feasible coupling strategies. Exact Borel measurable optimal strategies and initial couplings are obtained on Polish Borel spaces for weakly continuous probability kernels and nonnegative extended-real lower semicontinuous costs. Equivalence with optimization over bicausal path laws is not established.
Quoted from the card LeanPool/projects/bicausalot-palomar.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
MeasurableSelection.exists_measurable_selection(theorem; a main declaration), declared in LeanPool/BicausalOT/Solution.lean, line 56: “A weakly measurable multifunction from an arbitrary measurable space to a Polish space with nonempty closed values admits an everywhere-defined Borel-measurable selector.”
Project
- Authors: KT. Wu.
- Project repository: maxwellapexlab/bicausalot-palomar, at commit 3fe500ff.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 28B20, 54C65, 54H05, 03E15, 28A20, 68V20.
- In Lean Pool: LeanPool/BicausalOT, from the card LeanPool/projects/bicausalot-palomar.yaml.
Sources
TheoremFormalizing geometric measure theory#
A development of foundations and central results in geometric measure theory, including Hausdorff content and density bounds, weak convergence and compactness for Radon measures, tangent-measure machinery, Mattila's Lemmas 14.5--14.7, and Marstrand's integrality theorem for positive finite densities.
Quoted from the card LeanPool/projects/formalizing-gmt.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
mattila_14_10(theorem; a main declaration), declared in LeanPool/FormalizingGMT/MarstrandTheorem.lean, line 854: “If a Radon measure on Euclidean n-space has positive finite s-dimensional density on a set of positive measure, then s is a natural number.” Its source, as the card gives it: “Mattila, Theorem 14.10 (Marstrand's theorem).”mattila_14_11(theorem; a main declaration), declared in LeanPool/FormalizingGMT/MarstrandTheorem.lean, line 879: “Every n-uniform measure on Euclidean n-space is a constant multiple of Lebesgue measure.” Its source, as the card gives it: “Mattila, Theorem 14.11.”MeasureTheory.Measure.weaklyConverges_iff_compactOpenBounds(theorem), declared in LeanPool/FormalizingGMT/WeakConvergence/Basic.lean, line 306: “Vague convergence of Radon measures on Euclidean space is equivalent to the Portmanteau compact-set upper and open-set lower bounds.” Its source, as the card gives it: “Evans--Gariepy, revised edition, Theorem 1.40.”MeasureTheory.exists_vaguelyConvergent_subseq_of_compact_bounded(theorem), declared in LeanPool/FormalizingGMT/WeakConvergence/CompactnessCriterion.lean, line 496: “A sequence of Radon measures on Euclidean space that is uniformly bounded on every compact set has a vaguely convergent subsequence.” Its source, as the card gives it: “Evans--Gariepy, revised edition, Theorem 1.41.”
Project
- Authors: Theodore Meek, Ignacio Tejeda, Annie Cao, Nathan Pao.
- The card's note on its source: “The geometric-measure-theory results follow Mattila, Geometry of Sets and Measures in Euclidean Spaces, Chapter 14. The weak-convergence, compactness, covering, and density results follow Evans--Gariepy, Measure Theory and Fine Properties of Functions, revised edition.”
- Project repository: uw-math-ai/FormalizingGMT, at commit 0acca38a.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 28A75, 28A78, 49Q15.
- In Lean Pool: LeanPool/FormalizingGMT, from the card LeanPool/projects/formalizing-gmt.yaml.
Sources
TheoremMoreira's version of Sard's theorem#
Formalizes Moreira's strengthening of Sard's theorem, bounding the Hausdorff dimension of critical-value images of C^{k+alpha} maps.
Quoted from the card LeanPool/projects/sardmoreira.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
hausdorffMeasure_sardMoreiraBound_image_null_of_finrank_le(theorem), declared in LeanPool/SardMoreira/MainTheorem.lean, line 700: “Proves Hausdorff-measure nullity for images of points where the derivative rank is bounded by p, at Moreira's Sard bound.” Its source, as the card gives it: “Moreira 2001, http://dmle.icmat.es/pdf/PUBLICACIONSMATEMATIQUES_2001_45_01_06.pdf”dimH_image_le_sardMoreiraBound_of_finrank_le(theorem; a main declaration), declared in LeanPool/SardMoreira/MainTheorem.lean, line 745: “Converts the measure-null theorem into the headline Hausdorff-dimension upper bound for critical-value images.” Its source, as the card gives it: “Moreira 2001, http://dmle.icmat.es/pdf/PUBLICACIONSMATEMATIQUES_2001_45_01_06.pdf”
Project
- Authors: Yury G. Kudryashov.
- Source: doi:10.5565/PUBLMAT_45101_06, paper.
- Project repository: urkud/SardMoreira.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 28A78, 58C25.
- In Lean Pool: LeanPool/SardMoreira, from the card LeanPool/projects/sardmoreira.yaml.
Sources
TheoremPrekopa-Leindler, Brunn-Minkowski, and the isoperimetric inequality#
Formalizes the Prekopa-Leindler inequality, Brunn-Minkowski inequality, and an isoperimetric inequality.
Quoted from the card LeanPool/projects/isoperimetric.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
prekopa_leindler(theorem; a main declaration), declared in LeanPool/Isoperimetric/PrekopaLeindler.lean, line 625: “Proves the Prekopa-Leindler inequality.”brunn_minkowski(theorem; a main declaration), declared in LeanPool/Isoperimetric/BrunnMinkowski.lean, line 86: “Proves the Brunn-Minkowski inequality.”isoperimetric_inequality(theorem; a main declaration), declared in LeanPool/Isoperimetric/Isoperimetric.lean, line 41: “Proves the isoperimetric inequality derived from Brunn-Minkowski.”
Project
- Authors: Jonathan Ho.
- Source: https://terrytao.wordpress.com/2011/09/16/the-brunn-minkowski-inequality-for-nilpotent-groups/.
- Project repository: hojonathanho/isoperimetric.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 28A75, 52A40, 49Q20.
- In Lean Pool: LeanPool/Isoperimetric, from the card LeanPool/projects/isoperimetric.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.