MovingSampleCoordinates.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Fixed coordinates for the actual internal prime samples

The coordinates count each sample when it is made, not its later occurrences in descendant lists. Their number is independent of the number of bulk slots.

def OAI.Ostmann.MovingSampleIndex line 15
instance OAI.Ostmann.movingSampleIndexFintype line 19
def OAI.Ostmann.movingSampleTier line 24
theorem OAI.Ostmann.movingSampleTier_lt line 28
theorem OAI.Ostmann.card_movingSampleIndex line 36
def OAI.Ostmann.movingSampleCoordinates line 45
theorem OAI.Ostmann.movingCompensationPrior_indexed line 75
theorem OAI.Ostmann.movingSamplesPrior_coordinates line 93
Source documentation
The tree law is precisely the product of the original coordinate priors. This identity permits the proved equality-pattern comparison to be applied without replacing the law by a conditioned or uniform distribution.
```
theorem movingSamplesPrior_coordinates {A : Type*} (μ : ℕ → A → ℝ) (n : ℕ)
    (a : MovingSampleSlots A n) :
    movingSamplesPrior μ a =
      ∏ i : MovingSampleIndex n, μ (movingSampleTier i) (movingSampleCoordinates A n a i) := by
…
```
Mentions: OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingSamplesPrior, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingSampleTier, OAI.Ostmann.movingSampleCoordinates
theorem OAI.Ostmann.movingSamplesPrior_reindex line 107