OAI/NumberTheory/JointDickman/Probability/UniformResidueFibers.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform conditional residues, including null observation fibers

  1. theorem OAI.JointDickman.uniformImageMass_eq_push line 10
  2. theorem OAI.JointDickman.uniformConditionalMass_sum line 17
  3. def OAI.JointDickman.totalUniformConditionalMass line 29

    Source documentation

    Null fibers are assigned a point mass. Their observation mass is zero, so this makes a probability kernel without changing any joint law.

    noncomputable def totalUniformConditionalMass {Ω α : Type*} [Fintype Ω] [Inhabited Ω]
    (f : Ω → α) (y : α) (x : Ω) : ℝ :=
…
  4. theorem OAI.JointDickman.totalUniformConditionalMass_nonneg line 34
  5. theorem OAI.JointDickman.totalUniformConditionalMass_sum line 39
  6. theorem OAI.JointDickman.total_uniform_image_conditional line 46
  7. theorem OAI.JointDickman.total_uniform_product_disintegration line 60