OAI/NumberTheory/Ostmann/Arithmetic/MovingSamplePrior.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The original independent compensation samples

Section 7.4, equations (7.10)--(7.11), samples one compensation vector at each node. That vector is shared by its two children; samples subsequently made in the children are independent. These are the literal finite priors, before any distinctness or equality-pattern restriction.

  1. def OAI.Ostmann.movingSampleNodeEquiv line 17
  2. def OAI.Ostmann.movingSampleZeroEquiv line 25
  3. instance OAI.Ostmann.movingSampleSlotsFintype line 31
  4. def OAI.Ostmann.movingCompensationPrior line 39
  5. def OAI.Ostmann.movingSamplesPrior line 44
  6. theorem OAI.Ostmann.movingCompensationPrior_nonneg line 50
  7. theorem OAI.Ostmann.movingSamplesPrior_nonneg line 57
  8. theorem OAI.Ostmann.movingCompensationPrior_mass line 65
  9. theorem OAI.Ostmann.sum_movingSample_node line 78
  10. theorem OAI.Ostmann.movingSamplesPrior_mass line 99
  11. theorem OAI.Ostmann.movingSamplesPrior_node_product line 114

    Source documentation

    Independent descendants factor, while the single root vector is retained outside both child expectations. No prime-distinctness event is conditioned on.

    theorem movingSamplesPrior_node_product {A : Type*} [Fintype A]
    (μ : ℕ → A → ℝ) (n : ℕ)
    (c : TreeLeafTuple (Fin 4 → A) n → ℂ)
    (L R : TreeLeafTuple (Fin 4 → A) n → MovingSampleSlots A n → ℂ) :
    (∑ a : MovingSampleSlots A (n + 1), (movingSamplesPrior μ a : ℂ) *
      (match a with | .node u l r => c u * L u l * star (R u r))) =
      ∑ u : TreeLeafTuple (Fin 4 → A) n, (movingCompensationPrior (μ n) n u : ℂ) * c u *
        (∑ l : MovingSampleSlots A n, (movingSamplesPrior μ l : ℂ) * L u l) *
          star (∑ r : MovingSampleSlots A n, (movingSamplesPrior μ r : ℂ) * R u r) := by
…

    Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingSamplesPrior, OAI.Ostmann.movingCompensationPrior