MovingCompensationWeight.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The exact compensation factors in the original history weight

Every sampled prime occurs once in the factor u at the node where it is sampled. Its subsequent appearances in descendants do not add factors of u.

def OAI.Ostmann.movingSampleProduct line 16
theorem OAI.Ostmann.movingCompensationProduct_indexed line 23
theorem OAI.Ostmann.movingSampleProduct_coordinates line 40
def OAI.Ostmann.movingCompensationExtra line 53

theorem OAI.Ostmann.movingDataWeight_compensations line 60

Source documentation

Factor all the actual u multipliers out of the scalar history coefficient. Leaf weights and right-branch conjugations are retained.

theorem movingDataWeight_compensations {σ : Type*} (value : σ → ℕ)
    (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
    (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
    (a : MovingSampleSlots σ n) :
    movingDataWeight F (movingCompensationExtra value) (buildMovingSlotData n t small bulk a) =
      (movingSampleProduct value a : ℂ) *
        movingDataWeight F (fun _ _ _ _ => 1) (buildMovingSlotData n t small bulk a) := by
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingDataWeight, OAI.Ostmann.movingCompensationExtra, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.movingSampleProduct

theorem OAI.Ostmann.movingSamples_compensated_prior line 77
Source documentation
Prior times compensation is precisely the dependent pattern weight used in the internal-line comparison, before any coincidences are collapsed.
```
theorem movingSamples_compensated_prior {A : Type*} (μ : ℕ → A → ℝ)
    (value : A → ℕ) {n : ℕ} (a : MovingSampleSlots A n) :
    (movingSampleProduct value a : ℝ) * movingSamplesPrior μ a =
      ∏ i : MovingSampleIndex n,
        (value (movingSampleCoordinates A n a i) : ℝ) *
          μ (movingSampleTier i) (movingSampleCoordinates A n a i) := by
…
```
Mentions: OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingSampleProduct, OAI.Ostmann.movingSamplesPrior, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingSampleCoordinates, OAI.Ostmann.movingSampleTier
theorem OAI.Ostmann.movingSamples_compensated_pattern line 86