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.BorelCaratheodory
• PrimeNumberTheoremAnd.ZetaConj
• PrimeNumberTheoremAnd.HadamardFactorization
• PrimeNumberTheoremAnd.Rectangle
• PrimeNumberTheoremAnd.Auxiliary
• PrimeNumberTheoremAnd.HoffsteinLockhart
• PrimeNumberTheoremAnd.RosserSchoenfeldPrime_tables
• PrimeNumberTheoremAnd.Li2Bounds
• PrimeNumberTheoremAnd.BKLNW_app_tables
• PrimeNumberTheoremAnd.Sobolev
• PrimeNumberTheoremAnd.LogTables
• PrimeNumberTheoremAnd.Tactic.AdditiveCombination
• PrimeNumberTheoremAnd.Unused.MyMV_A3a
• PrimeNumberTheoremAnd.Unused.Hardy_Tauberian_theorem
• PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks
• PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults
• PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support
• 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
  • feat(NumberTheory/Height): formula for logHeight₁ #35919
  • feat(NumberTheory/Height/NumberField): lemmas/positivity extension for totalWeight #35924

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.

• PrimeNumberTheoremAnd.IwaniecKowalskiCh1 5 sorries