OAI/NumberTheory/JointDickman/Amplification/CandidateFairArithmetic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.regularRetainedArithmeticKernel line 11
2. theorem OAI.JointDickman.candidateSiteKernel_eq_regularArithmetic line 24

   Source documentation

   Exact normalization of the smooth latent kernel. In particular, its arithmetic coefficient, coprimality, endpoint and remainder restrictions are all the same ones estimated separately in the regularity argument.

   theorem candidateSiteKernel_eq_regularArithmetic {B L T H M V : ℕ} {τ C : ℝ}
       (hB : 1 < B) (hT : 0 < T)
       (hV : ⌊Real.exp (2*(B : ℝ))⌋₊ ≤ V)
       (i t : Fin M) (hit : i < t)
       (hH : H < t.val-i.val) (hjT : t.val-i.val < T)
       {S R : Finset ℕ} (hS : S ⊆ auxiliaryPrimes B) (hR : R ⊆ auxiliaryPrimes B) :
       candidateSiteKernel B L T H M τ C
         (candidateCutoff (amplificationOuterWeight B) (amplificationInnerWeight T)) i t S R =
         independentRootMean B L τ C*
           regularRetainedArithmeticKernel B L (t.val-i.val) τ C T V S R := by
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.candidateSiteKernel, OAI.JointDickman.candidateCutoff, OAI.JointDickman.amplificationOuterWeight, OAI.JointDickman.amplificationInnerWeight, OAI.JointDickman.independentRootMean, OAI.JointDickman.regularRetainedArithmeticKernel