OAI/NumberTheory/JointDickman/Amplification/FiniteConditionalProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.uniformFiber line 10
2. def OAI.JointDickman.uniformImageMass line 13
3. def OAI.JointDickman.uniformConditionalMass line 16
4. theorem OAI.JointDickman.uniform_image_conditional line 20
5. theorem OAI.JointDickman.finiteProduct_disintegration line 35

   Source documentation

   Observation kernels can be multiplied before disintegrating, even when the final test depends on the whole observed family.

   theorem finiteProduct_disintegration {ι : Type*} [Fintype ι] [DecidableEq ι]
       {Ω α : ι → Type*} [∀ i, Fintype (Ω i)] [∀ i, Fintype (α i)]
       (f : ∀ i, Ω i → α i) (w : ∀ i, Ω i → ℝ)
       (a : ∀ i, α i → ℝ) (k : ∀ i, α i → Ω i → ℝ)
       (hk : ∀ i y x, a i y*k i y x = if f i x = y then w i x else 0)
       (F : (∀ i, α i) → (∀ i, Ω i) → ℝ) :
       (∑ x, finiteProductMass w x * F (fun i => f i (x i)) x) =
         ∑ y, finiteProductMass a y *
           ∑ x, finiteProductMass (fun i => k i (y i)) x * F y x := by
   …

   Mentions: OAI.JointDickman.finiteProductMass

6. theorem OAI.JointDickman.uniformProduct_disintegration line 65