OAI/NumberTheory/JointDickman/Amplification/CandidateRowMajorant.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.candidateMeanWeight_le_endpointTest line 13

   Source documentation

   Every actual candidate supplies one term of the fixed-endpoint box test.

   theorem candidateMeanWeight_le_endpointTest {M B L T H : ℕ} {τ C : ℝ}
       (S : Fin M → Finset ℕ) (χ : BlockCandidateIndex M → ℝ)
       (hB : 10 ≤ B) (hT : 0 < T) (hTs : (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B))
       {e : BlockCandidateIndex M} (he : BlockCandidateAdmissible B L T H τ C e)
       (hχ : χ e ≤ 1) :
       candidateMeanWeight B L τ C S χ e ≤
         independentRootMean B L τ C/(B : ℝ)*
           (endpointSplitWeight B L τ C (S e.1.1) e.2.1*
             (endpointSplitWeight B L τ C (S e.1.2) e.2.2*
               supportedEndpointTest B T (candidateLow e) (candidateLag e) (candidateHigh e))) := by
   …

   Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.candidateMeanWeight, OAI.JointDickman.independentRootMean, OAI.JointDickman.endpointSplitWeight, OAI.JointDickman.supportedEndpointTest, OAI.JointDickman.candidateLow, OAI.JointDickman.candidateLag, OAI.JointDickman.candidateHigh

2. theorem OAI.JointDickman.latentCandidateKernel_le_rowEnvelope line 46

   Source documentation

   This is a pointwise comparison for the actual finite candidate list, valid for every choice of the other endpoint types.

   theorem latentCandidateKernel_le_rowEnvelope {M B L T H : ℕ} {τ C : ℝ}
       (S : Fin M → Finset ℕ) (χ : BlockCandidateIndex M → ℝ)
       (hB : 10 ≤ B) (hT : 0 < T) (hTs : (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B))
       (hχ : ∀ e, χ e ≤ 1) (i k : Fin M) (hik : i < k) :
       latentCandidateKernel B L T H M τ C S χ i k ≤
         endpointRowEnvelope B L T (k.val-i.val) τ C (S i) (S k) := by
   …

   Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.latentCandidateKernel, OAI.JointDickman.endpointRowEnvelope