OAI/NumberTheory/Ostmann/Arithmetic/MovingRootedSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingRootedFrequencyTree_root line 10
2. theorem OAI.Ostmann.scheduledFrequencyIndex_sum_split line 15
3. theorem OAI.Ostmann.scheduledFrequencyHistory_from_root line 23
4. theorem OAI.Ostmann.scheduledFrequency_bilinear_sum line 32

   Source documentation

   The two histories are independent after their roots are fixed. No number of histories occurs in this exact distributive identity. The child functions may depend on both roots through the reconstructed pivot.

   theorem scheduledFrequency_bilinear_sum (V : ℕ → ℕ) (n : ℕ)
       (W : ℤ → ℤ → ℂ)
       (L R : ℤ → ℤ → FrequencyTree ℤ n → ℂ) :
       (∑ l : ScheduledFrequencyIndex V n, ∑ r : ScheduledFrequencyIndex V n,
         W (frequencyRoot n (scheduledFrequencyHistory V n l))
             (frequencyRoot n (scheduledFrequencyHistory V n r)) *
           L (frequencyRoot n (scheduledFrequencyHistory V n l))
             (frequencyRoot n (scheduledFrequencyHistory V n r)) (scheduledFrequencyHistory V n l) *
           star (R (frequencyRoot n (scheduledFrequencyHistory V n l))
             (frequencyRoot n (scheduledFrequencyHistory V n r)) (scheduledFrequencyHistory V n r))) =
         ∑ v : transferFrequencyRange (V n), ∑ w : transferFrequencyRange (V n),
           W v.val w.val *
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.ScheduledFrequencyIndex, OAI.Ostmann.frequencyRoot, OAI.Ostmann.scheduledFrequencyHistory, OAI.Ostmann.transferFrequencyRange