OAI/NumberTheory/JointDickman/Probability/CandidateSiteKernel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The latent graph as a kernel of its two endpoint types

  1. theorem OAI.JointDickman.latentCandidateKernel_symm line 12
  2. theorem OAI.JointDickman.latentCandidateKernel_diag line 22
  3. theorem OAI.JointDickman.latentCandidateKernel_nonneg line 36
  4. theorem OAI.JointDickman.latentCandidateKernel_local line 47

    Source documentation

    Other endpoint types have no effect on this entry, even though the full candidate list depends on the entire configuration.

    theorem latentCandidateKernel_local {B L T H M : ℕ} {τ C : ℝ}
    (S R : Fin M → Finset ℕ) (χ : BlockCandidateIndex M → ℝ)
    (i k : Fin M) (hi : S i = R i) (hk : S k = R k) :
    latentCandidateKernel B L T H M τ C S χ i k =
      latentCandidateKernel B L T H M τ C R χ i k := by
…

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

  5. def OAI.JointDickman.candidateSiteKernel line 66
  6. theorem OAI.JointDickman.candidateSiteKernel_realizes line 70
  7. theorem OAI.JointDickman.candidateSiteKernel_diag line 78
  8. theorem OAI.JointDickman.candidateSiteKernel_nonneg line 83
  9. theorem OAI.JointDickman.candidateSiteKernel_symm line 89