CandidateReverseMajorant.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Domination of the actual latent candidate kernel by its row majorant

theorem OAI.JointDickman.candidateMeanWeight_le_reverseEndpointTest line 13

Source documentation

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

theorem candidateMeanWeight_le_reverseEndpointTest {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.2) e.2.2*
          (endpointSplitWeight B L τ C (S e.1.1) e.2.1*
            reverseSupportedTest B T (candidateHigh e) (candidateLag e) (candidateLow e))) := by
…

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

theorem OAI.JointDickman.latentCandidateKernel_le_reverseRowEnvelope 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_reverseRowEnvelope {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 ≤
      reverseEndpointRowEnvelope B L T (k.val-i.val) τ C (S k) (S i) := by
…

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