Upstreaming dashboard

Files ready to upstream

The following files are sorry-free and do not depend on any other files, meaning they can be readily PRed to Mathlib.

• PrimeNumberTheoremAnd.HoffsteinLockhart
• PrimeNumberTheoremAnd.ZetaConj
• PrimeNumberTheoremAnd.Sobolev
• PrimeNumberTheoremAnd.Auxiliary
• PrimeNumberTheoremAnd.BorelCaratheodory
• PrimeNumberTheoremAnd.HadamardFactorization
• PrimeNumberTheoremAnd.ZetaDefinitions
• PrimeNumberTheoremAnd.Rectangle
• PrimeNumberTheoremAnd.Tactic.AdditiveCombination
• PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults
• PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support
  • chore(Data/Set/Image): move BooleanAlgebra material to Order #26777
• PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Function.LocallyIntegrable
  • WIP: generalise lemmas to ENorm #21375
  • feat(LocallyIntegrable): generalise more to enorms #24862
  • chore: make finiteness a default tactic #26090
  • refactor: unbundle algebra from ENormed* #28803
  • feat(MeasureTheory): add MemLp.Const class and instances to unify p = ∞ and μ.IsFiniteMeasure cases #30030
  • feat: define Sobolev Spaces #32305
• PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics
  • feat: generalize isLittleO_const_id_atTop/atBot #12192
  • chore: attribute [induction_eliminator] #12605
  • chore: use open scoped #4960
• PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic
  • chore: change some linariths to linear_combinations #18841
  • feat(Tactic/Push): add basic tags and tests #29000
  • feat: new isolate tactic #29982
  • chore: remove declarations deprecated between 2020-10-21 and 2025-04-21 #30759
  • Lean pr testing 11156 #31587

Files easy to unlock

The following files do not depend on any other PNT+ file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.