minor improvements

[yuxi-liu-wired]

1. The leanprover-community/mathlib4 should be named upstream rather than origin.

Compiling it using lake throws the following warning:

Warning: Some Mathlib ecosystem tools assume that the git remote for leanprover-community/mathlib4 is named upstream. You have named it origin instead. We recommend changing the name to upstream. Moreover, origin should point to your own fork of the mathlib4 repository. You can set this up with git remote add upstream https://github.com/leanprover-community/mathlib4.git.

2. Unpleasant warnings

lake build gives the following results, which shows the use of sorry in a particular file in PrimeNumberTheoremAnd. This is not a problem, because lake build -KleanArgs=-DwarningAsError=true compiles. Despite this, it might be good to somehow avoid this.

info: StrongPNT/PNT1_ComplexAnalysis.lean:2969:0: 'borel_caratheodory_II' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [6921/6932] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:2274:6: declaration uses 'sorry'
warning: PrimeNumberTheoremAnd/Wiener.lean:2299:6: declaration uses 'sorry'
warning: PrimeNumberTheoremAnd/Wiener.lean:2321:6: declaration uses 'sorry'
ℹ [6927/6932] Replayed StrongPNT.PNT4_ZeroFreeRegion
info: StrongPNT/PNT4_ZeroFreeRegion.lean:6619:0: 'ZetaZeroFree_p' depends on axioms: [propext, Classical.choice, Quot.sound]
info: StrongPNT/PNT4_ZeroFreeRegion.lean:6620:0: 'LogDerivZetaBndUnif2' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [6930/6932] Replayed StrongPNT.PNT5_Strong
info: StrongPNT/PNT5_Strong.lean:6599:0: 'Strong_PNT' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully.