OAI/NumberTheory/Ostmann/Construction/FiniteCoordinatePrior.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.finiteCoordinatePrior line 11
2. def OAI.Ostmann.finiteCoordinatePriors line 15
3. theorem OAI.Ostmann.finite_prior_splitAt line 20
4. theorem OAI.Ostmann.piSplitAt_update line 44
5. theorem OAI.Ostmann.finite_prior_coordinate_preserves line 54
6. theorem OAI.Ostmann.finiteCoordinatePriors_preserves line 66
7. theorem OAI.Ostmann.finiteCoordinatePriors_update line 76
8. theorem OAI.Ostmann.finiteCoordinatePriors_all line 96

   Source documentation

   Replacing every coordinate gives exactly the full product-prior mean, regardless of the chosen order.

   theorem finiteCoordinatePriors_all {σ A : Type*} [Fintype σ] [Fintype A]
       (μ : σ → A → ℝ) (hmass : ∀ i, ∑ a, μ i a = 1)
       (l : List σ) (hl : ∀ i, i ∈ l) (F : (σ → A) → ℂ) (x : σ → A) :
       finiteCoordinatePriors μ l F x = ∑ y, ((∏ j, μ j (y j) : ℝ) : ℂ) * F y := by
   …

   Mentions: OAI.Ostmann.finiteCoordinatePriors