CandidatePairSum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The latent kernel as a local sum over its two endpoint splits

theorem OAI.JointDickman.candidate_pair_sum line 12

theorem OAI.JointDickman.latentCandidateKernel_pair line 54

Source documentation

For i<k only the forward orientation contributes.

theorem latentCandidateKernel_pair {M : ℕ} (B L T H : ℕ) (τ C : ℝ)
    (S : Fin M → Finset ℕ) (χ : BlockCandidateIndex M → ℝ) (i k : Fin M) (hik : i < k) :
    latentCandidateKernel B L T H M τ C S χ i k =
      ∑ A ∈ endpointSplits B L τ C (S i),
        ∑ D ∈ endpointSplits B L τ C (S k),
          if BlockCandidateAdmissible B L T H τ C ((i,k),(A,D))
          then candidateMeanWeight B L τ C S χ ((i,k),(A,D)) else 0 := by
…

Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.latentCandidateKernel, OAI.JointDickman.endpointSplits, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.candidateMeanWeight