MovingTemplatePrior.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The unchanged independent prime law under one template restoration

def OAI.Ostmann.movingRestoreSample line 12
theorem OAI.Ostmann.movingRestoreSample_compensation line 17
theorem OAI.Ostmann.movingRestoreSample_small line 26
theorem OAI.Ostmann.movingRestoreSample_bulk line 35

theorem OAI.Ostmann.movingReverseTemplate_average line 48

Source documentation

This is literal finite Fubini; neither distinctness nor any history support is conditioned into the prime law.

theorem movingReverseTemplate_average {A : Type*} [Fintype A] (n r m : ℕ)
    (ν : MovingRegularSlot n (4 + r) m → A → ℝ)
    (F : (MovingRegularSlot n (4 + r) m → A) → ℂ) :
    (∑ x, ((∏ i, ν i (x i) : ℝ) : ℂ) * F x) =
      ∑ u : TreeLeafIndex n × Fin 4 → A,
        ((∏ i, ν (movingReverseTemplate n r m (.inl i)) (u i) : ℝ) : ℂ) *
        ∑ y : MovingRegularSlot n r m → A,
          ((∏ i, ν (movingReverseTemplate n r m (.inr i)) (y i) : ℝ) : ℂ) *
          F (movingRestoreSample n r m u y) := by
…

Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.movingReverseTemplate, OAI.Ostmann.movingRestoreSample

def OAI.Ostmann.movingTemplateCompensationEquiv line 89
Source documentation
The compensation block is sampled once, in precisely the coordinates of movingCompensationPrior; the two child histories will share this block.
```
def movingTemplateCompensationEquiv (A : Type*) (n : ℕ) :
    TreeLeafTuple (Fin 4 → A) n ≃ (TreeLeafIndex n × Fin 4 → A) :=
…
```
Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex
theorem OAI.Ostmann.movingTemplateCompensationEquiv_prior line 93
theorem OAI.Ostmann.movingReverseTemplate_compensation_average line 99