Partial differential equations
The Lean Pool projects whose card's first MSC2020 code is in class 35, Partial differential equations: 10 articles, one per card.
TheoremAnomalous diffusion by fractal homogenization#
For each positive Hölder exponent below one third, constructs a divergence-free periodic drift on the two-dimensional torus exhibiting anomalous dissipation for every mean-zero periodic H1 initial datum. The same drift admits uniform Hölder time estimates along a sequence of diffusivity intervals and two distinct vanishing-diffusivity limits for an explicit nonempty class of smooth data. Includes weak existence and uniqueness, Sobolev and Fourier/Galerkin infrastructure, flow derivatives, quantitative homogenization, and the multiscale construction. The no-selection result is the corrected version documented upstream, not the printed generality of the original paper's Proposition 5.5.
Quoted from the card LeanPool/projects/anomalous-diffusion-fractal-homogenization.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.
AVenhance.anomalous_dissipation_full(theorem; a main declaration), declared in LeanPool/AnomalousDiffusion/AVenhance/Statements/FullTheorem/AnomalousDissipationFull.lean, line 49: “For every alpha strictly between zero and one third, one periodic, divergence-free drift has joint spatial and temporal alpha-Hölder regularity and continuity into the spatial Hölder class. It exhibits anomalous dissipation with a positive rate depending only on the initial L2-to-gradient ratio, uniform Hölder-in-time L2 bounds along diffusivity intervals accumulating at zero, and two distinct transport limits along separated diffusivity sequences for a smooth mean-zero data class containing arbitrarily high cosine modes.” Its source, as the card gives it: “Upstream Statements/FullTheorem/AnomalousDissipationFull.lean and CITATION.cff, date-released 2026-10-02; the pinned completion commit is fad71d10bff031522cc598a37770238248186964, with committer timestamp 2026-10-02 16:04:04 UTC. Anomalous dissipation is the dimension-two case of Theorem 1.1 of arXiv:2305.05048; uniform time regularity and no-selection use upstream's documented corrections to Sections 5.4 and 5.5. The README explicitly records predominantly AI-produced proofs under the authors' supervision.”AVenhance.anomalous_dissipation(theorem), declared in LeanPool/AnomalousDiffusion/AVenhance/Statements/Roots/AnomalousDissipation.lean, line 26: “For every positive alpha below one third there exists a periodic, divergence-free alpha-Hölder drift and a rate function taking values in (0,1], depending only on the initial L2-to-gradient ratio, such that the limsup as positive diffusivity tends to zero of integrated gradient dissipation is at least the squared rate times the initial L2 energy, for every mean-zero periodic H1 datum and corresponding weak solutions.”AVenhance.weak_wellposed(theorem), declared in LeanPool/AnomalousDiffusion/AVenhance/Statements/Roots/WeakWellposed.lean, line 21: “Every bounded measurable periodic drift with positive diffusivity and periodic-cell L2 initial datum has a weak solution, unique up to spatial almost-everywhere equality at every time in [0,1].”
Project
- Authors: Scott Armstrong, Vlad Vicol.
- Source: Anomalous diffusion by fractal homogenization, Lean formalization, arXiv:2305.05048.
- Project repository: scottnarmstrong/AVAnomalousDiffusion, at commit fad71d10.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 35B27, 35Q35, 76F30.
- In Lean Pool: LeanPool/AnomalousDiffusion, from the card LeanPool/projects/anomalous-diffusion-fractal-homogenization.yaml.
Sources
TheoremCaffarelli–Kohn–Nirenberg partial regularity#
Partial regularity for three-dimensional incompressible Navier–Stokes suitable weak solutions with locally L^q forcing, q > 5/2: quantitative epsilon regularity and vanishing parabolic one-dimensional Hausdorff measure of the singular set. Includes the supporting Sobolev, singular integral, pressure, heat-potential and parabolic Morrey infrastructure, equivalence of suitable-solution formulations, and a nonzero shear-flow example. Includes the completed Leray, pressure, and linear regularity support needed by further Navier–Stokes regularity projects.
Quoted from the card LeanPool/projects/caffarelli-kohn-nirenberg.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 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.
CKN.epsilonRegularityL3(theorem; a main declaration), declared in LeanPool/CaffarelliKohnNirenberg/Statements/TheoremA.lean, line 35: “For q > 5/2, sufficiently small unit-cylinder L^3 velocity, L^(3/2) pressure and L^q force masses give an almost-everywhere equal quantitatively bounded parabolic Holder representative on the closed half-cylinder and regularity at each point of its open interior.”CKN.epsilonRegularityGradient(theorem), declared in LeanPool/CaffarelliKohnNirenberg/Statements/TheoremB.lean, line 34: “A sufficiently small extended nonnegative limsup of the normalized squared weak-gradient mass implies regularity at an interior point of a suitable weak solution.”CKN.caffarelliKohnNirenberg(theorem; a main declaration), declared in LeanPool/CaffarelliKohnNirenberg/Statements/TheoremC.lean, line 35: “The singular set of a suitable weak solution with locally L^q forcing, q > 5/2, has zero one-dimensional Hausdorff measure in the parabolic metric.”CKN.isSuitableWeakSolution_iff_integrable(theorem), declared in LeanPool/CaffarelliKohnNirenberg/ClassEquivalence/MainTheorems.lean, line 87: “The manuscript's suitable weak-solution predicate is equivalent to the predicate that explicitly requires integrability of all tested weak-equation and local-energy integrands.”CKN.isSuitableWeakSolutionIntegrable_shearFlow(theorem), declared in LeanPool/CaffarelliKohnNirenberg/Setting/Examples/ShearFlowSuitable.lean, line 27: “The nonzero decaying sinusoidal shear flow with zero pressure and force is a suitable weak solution on all space and times in (0,1).”
Project
- Authors: Scott Armstrong, Vlad Vicol.
- Project repository: scottnarmstrong/CaffarelliKohnNirenberg, at commit 381d658e.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 35Q30, 35B65, 42B20, 28A78.
- In Lean Pool: LeanPool/CaffarelliKohnNirenberg, from the card LeanPool/projects/caffarelli-kohn-nirenberg.yaml.
Sources
TheoremClawristotle: Vlasov-Maxwell-Landau steady-state classification#
Formalizes a steady-state classification result for the Vlasov-Maxwell-Landau system with Coulomb kernel.
Quoted from the card LeanPool/projects/clawristotle.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.
VML.Theorem42(theorem; a main declaration), declared in LeanPool/Clawristotle/Theorem42.lean, line 152: “States the abstract steady-state classification theorem for the Vlasov-Maxwell-Landau framework.”VML.CoulombConcreteTheorem42(theorem; a main declaration), declared in LeanPool/Clawristotle/CoulombConcreteTheorem42.lean, line 84: “Specializes the steady-state classification theorem to the Coulomb kernel.”
Project
- Authors: Vasily Ilin.
- Source: arXiv:2603.15929.
- Project repository: Vilin97/Clawristotle.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 35Q83, 82C40, 35Q61.
- In Lean Pool: LeanPool/Clawristotle, from the card LeanPool/projects/clawristotle.yaml.
Sources
TheoremEscauriaza–Seregin–Šverák and Ladyzhenskaya–Prodi–Serrin regularity#
Endpoint and Serrin regularity criteria for three-dimensional incompressible Navier–Stokes Leray–Hopf solutions: bounded L-infinity-in-time L3 velocity implies L5 integrability, uniqueness, and a smooth representative on positive times including the final time. Includes local endpoint regularity, both Carleman inequalities, spatial unique continuation, and half-space backward uniqueness. Retains the complete ESS production formalization.
Quoted from the card LeanPool/projects/escauriaza-seregin-sverak.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 10 main results, each with its informal statement quoted from the card. The scan finds 10 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.
ESS.essSmooth(theorem; a main declaration), declared in LeanPool/EscauriazaSereginSverak/Statements/EssSmooth.lean, line 39: “A Leray–Hopf solution whose spatial L3 mass is essentially bounded in time belongs to space-time L5, is unique among Leray–Hopf solutions with the same initial datum, and has an almost-everywhere equal smooth representative on all positive times through the final time.”ESS.ladyzhenskayaProdiSerrin(theorem; a main declaration), declared in LeanPool/EscauriazaSereginSverak/Statements/LadyzhenskayaProdiSerrin.lean, line 40: “A Leray–Hopf solution satisfying the critical Serrin mixed-norm condition with spatial exponent greater than three, including the L2-in-time L-infinity-in-space endpoint, is unique and has a smooth representative on positive times through the final time.”ESS.serrinCriterion(theorem; a main declaration), declared in LeanPool/EscauriazaSereginSverak/Statements/SerrinCriterion.lean, line 36: “The endpoint L-infinity-in-time L3 criterion and the Serrin criteria for all spatial exponents greater than three jointly imply uniqueness and existence of a smooth representative up to the final time.”ESS.essLocal(theorem), declared in LeanPool/EscauriazaSereginSverak/Statements/EssLocal.lean, line 30: “A weak Navier–Stokes solution on the unit cylinder with finite energy, L3/2 pressure, and velocity essentially bounded in time in spatial L3 has an almost-everywhere equal parabolically Holder representative on the closure of the half cylinder.”ESS.essGlobal(theorem), declared in LeanPool/EscauriazaSereginSverak/Statements/EssGlobal.lean, line 29: “A Leray–Hopf solution whose spatial L3 mass is essentially bounded in time has no singular point at an interior positive time.”ESS.essL5Unique(theorem), declared in LeanPool/EscauriazaSereginSverak/Statements/EssL5Unique.lean, line 28: “A Leray–Hopf solution whose spatial L3 mass is essentially bounded in time belongs to space-time L5 and is unique among Leray–Hopf solutions with its initial datum.”ESS.uniqueContinuation(theorem), declared in LeanPool/EscauriazaSereginSverak/Statements/UniqueContinuation.lean, line 38: “A vector field with explicit weak space-time derivatives obeying a parabolic differential inequality has unique continuation across a spatial boundary under the stated decay and boundary hypotheses.”ESS.backwardUniqueness(theorem), declared in LeanPool/EscauriazaSereginSverak/Statements/BackwardUniqueness.lean, line 38: “A vector field on a three-dimensional half-space satisfying the heat differential inequality, growth bound, and zero initial trace vanishes.”ESS.carlemanGaussian(theorem), declared in LeanPool/EscauriazaSereginSverak/Statements/CarlemanGaussian.lean, line 38: “The Gaussian Carleman inequality bounds weighted field and gradient energies by the weighted heat-operator energy under its support hypotheses.”ESS.carlemanHalfSpace(theorem), declared in LeanPool/EscauriazaSereginSverak/Statements/CarlemanHalfSpace.lean, line 38: “The half-space Carleman inequality bounds weighted field and gradient energies by the weighted heat-operator energy under its support hypotheses.”
Project
- Authors: Scott Armstrong.
- Project repository: scottnarmstrong/EscauriazaSereginSverak, at commit ae1a0e46.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 35Q30, 35B65, 35B60.
- In Lean Pool: LeanPool/EscauriazaSereginSverak, from the card LeanPool/projects/escauriaza-seregin-sverak.yaml.
Sources
TheoremFinite-time breakdown for Navier–Stokes and Euler#
Formalizes forced three-dimensional Navier–Stokes breakdown on Euclidean space and the periodic torus for every positive viscosity, and finite-time singularity formation for unforced Euler from smooth, compactly supported, divergence-free initial data. The Euler result specifies maximal Sobolev lifespan, divergence of the velocity C¹ norm, and divergence of the time integral of the vorticity norm.
Quoted from the card LeanPool/projects/navier-stokes-and-euler.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.
NavierStokes.Comparator.navier_stokes_breakdown_R3(theorem; a main declaration), declared in LeanPool/NavierStokesAndEuler/NavierStokes/ComparatorSolution.lean, line 28: “For every positive viscosity, there are smooth divergence-free initial data and smooth forcing on ℝ³, with the prescribed spatial and temporal decay, admitting no global smooth Navier–Stokes solution with uniformly bounded kinetic energy.”NavierStokes.Comparator.navier_stokes_breakdown_periodic(theorem), declared in LeanPool/NavierStokesAndEuler/NavierStokes/ComparatorSolution.lean, line 35: “For every positive viscosity, there are smooth periodic divergence-free initial data and smooth periodic forcing with the prescribed temporal decay, admitting no global smooth periodic Navier–Stokes solution.”Euler.euler_breakdown_R3(theorem; a main declaration), declared in LeanPool/NavierStokesAndEuler/Euler/Solution.lean, line 82: “There exist smooth divergence-free initial data on ℝ³ whose spatial derivatives decay faster than every polynomial and which admit no global smooth unforced Euler solution with uniformly bounded kinetic energy.”Euler.exists_compact_smooth_euler_singularity(theorem), declared in LeanPool/NavierStokesAndEuler/Euler/Solution.lean, line 96: “There exist nonzero smooth compactly supported divergence-free initial data, a maximal time 0 < Tstar ≤ 1, and an unforced Euler solution on [0, Tstar) in the all-order Sobolev class with bounded kinetic energy. Smooth Sobolev solutions on [0, T] exist exactly when T < Tstar. The velocity C¹ norm has infinite left limsup at Tstar, and the time integral of the spatial supremum of the vorticity norm diverges.”
Project
- Authors: OpenAI.
- Source: Finite time blowup for Navier–Stokes and Finite time blowup for the Euler equation by OpenAI.
- Project repository: openai/NavierStokesAndEuler, at commit 8937a8f4.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 35Q30, 35Q31, 35B44.
- In Lean Pool: LeanPool/NavierStokesAndEuler, from the card LeanPool/projects/navier-stokes-and-euler.yaml.
Sources
TheoremHomogenization at a polynomial scale in high contrast#
Formalizes polynomial entry into the small-contrast regime, algebraic convergence of coarse blocks, and quantitative stochastic homogenization with correctors, Liouville classification and large-scale regularity. Uses locally uniformly elliptic measurable coefficient fields modulo almost-everywhere equality. The Dirichlet estimate has the documented negative-Sobolev formulation on adapted cells; the random radius is at least one and the effective matrix is existentially produced. Includes the complete production library and its pinned CoarseGraining dependency closure in an isolated support namespace.
Quoted from the card LeanPool/projects/high-contrast-homogenization.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 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.
HCPoly.polynomial_entry(theorem), declared in LeanPool/HighContrastHomogenization/MainResults.lean, line 77: “Under stationary unit-range assumptions and the source-tail bound, every generation beyond a scale of polynomial length has annealed contrast at most one plus the prescribed tolerance.”HCPoly.algebraic_convergence(theorem), declared in LeanPool/HighContrastHomogenization/MainResults.lean, line 121: “The annealed coarse blocks converge algebraically to a limiting positive-definite block, with two-sided order estimates.”HCPoly.uniform_homogenization(theorem), declared in LeanPool/HighContrastHomogenization/MainResults.lean, line 183: “Uniformly elliptic stationary unit-range laws satisfy the negative-Sobolev Dirichlet estimate, corrector estimates, Liouville classification and first-order approximation obtained by specializing the polynomial homogenization theorem.”HCPoly.polynomial_homogenization(theorem; a main declaration), declared in LeanPool/HighContrastHomogenization/MainResults.lean, line 359: “High-contrast stationary unit-range laws admit an effective matrix and a random homogenization radius with polynomial length and quantitative tails, negative-Sobolev Dirichlet estimates on adapted cells, correctors, Liouville classification and large-scale regularity.”HCPoly.quenched_convergence(theorem), declared in LeanPool/HighContrastHomogenization/MainResults.lean, line 513: “Coarse coefficients converge almost surely beyond a quantitative random scale, with the documented source-tail and stretched-exponential tail estimates.”
Project
- Authors: Scott Armstrong, Tuomo Kuusi, Amélie Loher.
- Source: arXiv:2609.27647.
- Project repository: scottnarmstrong/HighContrastHomogenization, at commit 7a13dbcd.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 35B27, 35J15, 60K37.
- In Lean Pool: LeanPool/HighContrastHomogenization, from the card LeanPool/projects/high-contrast-homogenization.yaml.
Sources
TheoremLinear elliptic PDE: solvability, regularity and spectral theory#
A reusable analytic development of linear uniformly elliptic divergence-form PDE on Euclidean domains: Hilbert graph models of H¹ and H₀¹, bounded coefficient operators, Poincaré inequalities, zero-drift/nonnegative-potential Dirichlet existence and uniqueness, Gårding and Fredholm theory for general drift, interior H² and higher Sobolev regularity, smooth classical representatives, Sobolev and Hölder embeddings, C¹-domain extension and compactness, variational eigenvalues, and maximum principles. AI-generated proofs with human mathematical design and transcription; announced in arXiv:2609.32561 on 2026-09-26. The unfinished boundary-H² program is outside this completed dependency closure.
Quoted from the card LeanPool/projects/elliptic-pde.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 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.
EllipticPdes.Sobolev.FullEllipticOp.weak_solution_L2_of_nonneg_zeroth_of_bounded(theorem), declared in LeanPool/EllipticPDE/Existence/Garding.lean, line 565: “On a bounded domain in positive dimension, a bounded measurable uniformly elliptic operator with zero drift and nonnegative zeroth-order coefficient has a unique H₀¹ weak solution for every L² datum, with a datum-independent norm bound.”EllipticPdes.Regularity.interior_H2_estimate(theorem), declared in LeanPool/EllipticPDE/Regularity/Interior.lean, line 118: “In positive dimension, on an open measurable domain, an H₀¹ weak solution of a bounded measurable uniformly elliptic divergence-form operator with globally Lipschitz principal coefficients and an L² datum has interior L² second weak derivatives, with an estimate whose constant is chosen before the solution and datum.”EllipticPdes.Regularity.higher_interior_regularity(theorem; a main declaration), declared in LeanPool/EllipticPDE/Regularity/HigherInterior.lean, line 549: “In positive dimension, for a uniformly elliptic divergence-form operator with bounded measurable coefficients, globally Lipschitz principal-coefficient representatives in W^{k+1,∞}(ℝ^d), and lower-order coefficients in W^{k,∞}(ℝ^d), every H₀¹ weak solution on an open measurable domain with an H^k datum has interior H^{k+2} regularity. On each compact subset the iterated L² derivative bounds have a constant chosen before the solution, datum and its H^k bound. The pointwise Lipschitz hypothesis is separate from the weak-derivative bundles.”EllipticPdes.Sobolev.embL2_isCompact(theorem), declared in LeanPool/EllipticPDE/Spectrum/RellichDischarge.lean, line 203: “The inclusion H₀¹(Ω) → L²(Ω) is compact for bounded measurable Euclidean domains, discharging the compactness input to the Fredholm and spectral results.”EllipticPdes.Extension.exists_extW12(theorem), declared in LeanPool/EllipticPDE/Extension/GraphOperator.lean, line 188: “In positive dimension, bounded open Euclidean domains with C¹ boundary admit a bounded linear H¹ extension operator with compact support control.”
Project
- Authors: Alejandro José Soto Franco, Kobe Marshall-Stevens.
- Source: arXiv:2609.32561.
- Project repository: alejandro-soto-franco/EllipticPDE, at commit eaf821d3.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 35J15, 35J25, 35B65, 46E35.
- In Lean Pool: LeanPool/EllipticPDE, from the card LeanPool/projects/elliptic-pde.yaml.
Sources
TheoremMean-field derivation and well-posedness of the Vlasov equation#
Formalizes the mean-field limit, Dobrushin stability, and forward-in-time well-posedness for the Vlasov equation via Wasserstein-1 optimal transport.
Quoted from the card LeanPool/projects/vlasov-mean-field.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.
Vlasov.vlasovWellPosedness(theorem; a main declaration), declared in LeanPool/Vlasov/OT/WellPosedness.lean, line 1907: “Forward-in-time existence of a Lagrangian solution to the Vlasov equation on any finite horizon, for interaction forces that are Lipschitz gradients of an even pair potential (class AssW) — with no smallness restriction on the Lipschitz constant.”Vlasov.dobrushin(theorem; a main declaration), declared in LeanPool/Vlasov/OT/WellPosedness.lean, line 2097: “A Wasserstein-1 form of Dobrushin's 1979 stability estimate (the original uses a truncated metric) - two Lagrangian Vlasov solutions with finite first moments at every time separate at most at an exponential Gronwall rate.”Vlasov.meanFieldLimit(theorem; a main declaration), declared in LeanPool/Vlasov/Basic.lean, line 1751: “Conditional mean-field limit - given Wasserstein-1 convergence of the initial empirical data and a uniform Dobrushin stability estimate for the empirical curves, the N-particle empirical measures converge to the Vlasov solution uniformly on any finite horizon.”Vlasov.weak_isLagrangianVlasovSolutionOn(theorem), declared in LeanPool/Vlasov/OT/WeakToLagrangian.lean, line 1224: “On a time window with L * T^2 < 1, a weak solution with the standing regularity (even C^2 pair potential AssW2, finite first moments, narrow continuity, time-continuity of the convolution force at each point, continuity of the convolution-derivative field, and a uniform spatial first-moment bound on the window) is Lagrangian - the pushforward of its initial datum along the characteristic flow.”
Project
- Authors: Joseph K. Miller.
- Source: A Formalization of the Mean-Field Derivation of the Vlasov Equation by Joseph K. Miller, arXiv:2607.08986.
- Project repository: Hydrodynamical/Vlasov_Meanfield_Formalization.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 35Q83, 82C22, 49Q22.
- In Lean Pool: LeanPool/Vlasov, from the card LeanPool/projects/vlasov-mean-field.yaml.
Sources
TheoremRegularity of asymptotically axisymmetric Navier–Stokes solutions#
Proves the Constantin–Ignatova–Vicol regularity theorem for suitable weak solutions of the three-dimensional forced Navier–Stokes equations with analytic forcing, anisotropic Type II bounds on the angular mean, and an axisymmetric core at each time. Includes the fully axisymmetric theorem, meridional smallness, interior spatial analyticity, the nonanalyticity consequence for singular solutions, and the comparison, Serrin, and Gustafson–Kang–Tsai results used in their proofs. Reuses Lean Pool's Caffarelli–Kohn–Nirenberg suitable-solution and analysis library.
Quoted from the card LeanPool/projects/civ-axisymmetric.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 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.
CIV.mainTheorem(theorem; a main declaration), declared in LeanPool/CIVAxisymmetric/Statements/MainTheorem.lean, line 40: “A smooth suitable weak solution on the unit parabolic cylinder with globally finite energy, bounded C^2 spatially analytic force, anisotropic Type II bounds on its angular mean, and a positive axisymmetric core at every time is axisymmetric throughout the cylinder and bounded near the origin up to the terminal time.”CIV.axisymmetricTheorem(theorem; a main declaration), declared in LeanPool/CIVAxisymmetric/Statements/AxisymmetricTheorem.lean, line 38: “An axisymmetric smooth suitable weak solution obeying the stated anisotropic Type II bounds and bounded C^2 force is bounded near the origin up to the terminal time.”CIV.meridionalSmallness(theorem), declared in LeanPool/CIVAxisymmetric/Statements/MeridionalSmallnessProp.lean, line 37: “Under the axisymmetric anisotropic hypotheses, the weighted meridional quantity tends uniformly to zero on a smaller cylinder as the terminal time approaches.”CIV.interiorAnalyticity(theorem), declared in LeanPool/CIVAxisymmetric/Statements/InteriorAnalyticity.lean, line 32: “Smooth solutions with locally uniformly spatially analytic forcing are locally uniformly spatially analytic in the interior.”CIV.forceUnderCore(theorem), declared in LeanPool/CIVAxisymmetric/Statements/ForceUnderCore.lean, line 40: “For a smooth suitable weak solution with globally finite energy, bounded C^2 forcing, angular-mean anisotropic bounds, and an axisymmetric core at every time, failure of boundedness near the origin implies that the force is not spatially analytic, is nonzero somewhere in the unit cylinder, and has a nonzero point in every smaller terminal cylinder.”
Project
- Authors: Scott Armstrong, Vlad Vicol.
- Source: arXiv:2609.20803.
- Project repository: scottnarmstrong/CIVAxisymmetric, at commit 9f539dc7.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 35Q30, 35B65, 35B33.
- In Lean Pool: LeanPool/CIVAxisymmetric, from the card LeanPool/projects/civ-axisymmetric.yaml.
Sources
TheoremViscosity solutions, Aleksandrov differentiability and harmonic Dirichlet problems#
Develops second-order semijets, smooth test-function equivalence, Jensen contact sets, convex Aleksandrov differentiability, the quadratic-penalty Ishii lemma and compact-domain comparison for degenerate elliptic equations. Perron assembly retains explicit comparison, barrier and bumping assumptions; these are discharged for classical harmonic Dirichlet existence on bounded open domains satisfying a uniform exterior sphere condition.
Quoted from the card LeanPool/projects/viscosity-solution-theory.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 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.
AleksandrovDifferentiability.convexAleksandrovAE(theorem), declared in LeanPool/ViscositySolutionTheory/AleksandrovDifferentiability/Statements/Aleksandrov/Final.lean, line 39: “A convex real-valued function on an open subset of any finite-dimensional real inner product space is second-order differentiable at Lebesgue-almost every point.”ViscositySolns.JensenContactSetPositiveMeasureOnClosedBallTheorem.proof(theorem), declared in LeanPool/ViscositySolutionTheory/ViscositySolns/Analysis/SemiconvexJensen/Jensen/MainTheorems.lean, line 538: “Under the localized semiconvexity and strict-contact hypotheses, the contact set arising from sufficiently small linear perturbations has positive Lebesgue measure.”ViscositySolns.QuadraticPenaltyIshiiLemmaOn.proof(theorem), declared in LeanPool/ViscositySolutionTheory/ViscositySolns/Comparison/CILMaximumPrinciple.lean, line 327: “For an upper semicontinuous function and a lower semicontinuous function on locally compact subsets of real coordinate space, doubled-variable maxima with the quadratic penalty yield closed semijets satisfying the Ishii block-matrix bounds.”ViscositySolns.comparison_of_constantShift_boundary_proof(theorem), declared in LeanPool/ViscositySolutionTheory/ViscositySolns/Comparison/ProperComparison/Compact/ConstantShiftBoundary.lean, line 521: “A viscosity subsolution lies below a supersolution on a nonempty locally compact domain with compact closure, assuming boundary comparison, semicontinuity on the closure, properness, operator continuity, the Ishii structural condition and uniform scalar decrease.”ViscositySolns.viscositySubsolution_iff_smoothTestFunctionSubsolution(theorem), declared in LeanPool/ViscositySolutionTheory/ViscositySolns/TestFunctions/Characterization.lean, line 563: “On an open domain, semijet and smooth C² test-function formulations of viscosity subsolutions agree for Hessian-continuous, symmetric-part-invariant operators.”ViscositySolns.dirichlet_harmonic_modulus_of_uniformExteriorSphere(theorem; a main declaration), declared in LeanPool/ViscositySolutionTheory/ViscositySolns/Applications/Laplace/Dirichlet.lean, line 51: “On a bounded open subset of finite-dimensional Euclidean space with a uniform exterior sphere condition, Lipschitz data on its closure admit a continuous extension that agrees on the boundary and is C² and harmonic in the domain, with a boundary modulus depending only on the domain and Lipschitz constant.”
Project
- Authors: William M. Feldman, AleksandrovDifferentiability contributors, The Tau Ceti contributors.
- Source: arXiv:math/9207212.
- Project repository: willmfeldman/viscosity-solution-theory, at commit 067e2540.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 35D40, 35J60, 26B25.
- In Lean Pool: LeanPool/ViscositySolutionTheory, from the card LeanPool/projects/viscosity-solution-theory.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.