OAI/NumberTheory/Ostmann/Construction/ScheduledHistoryEmbedding.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.frequencyTreeInFinset line 11
2. theorem OAI.Ostmann.frequencyTreeInFinset_map line 21
3. abbrev OAI.Ostmann.NonzeroScheduledHistory line 32
4. instance OAI.Ostmann.nonzeroScheduledHistoryFintype line 36
5. def OAI.Ostmann.scheduledHistoryEmbedding line 40
6. theorem OAI.Ostmann.scheduledHistoryEmbedding_map line 53
7. theorem OAI.Ostmann.scheduledFrequencyHistory_leaf_cutoff line 59
8. theorem OAI.Ostmann.scheduledHistoryEmbedding_leaf_cutoff line 71
9. theorem OAI.Ostmann.scheduled_history_sum_le line 81

   Source documentation

   Only internal frequencies are enlarged to the largest cutoff. Zero frequencies contribute nothing, and every bottom frequency keeps cutoff V 0.

   theorem scheduled_history_sum_le (V : ℕ → ℕ) (hV : Monotone V) (n : ℕ)
       (F : FrequencyTree ℤ n → ℝ) (hF : ∀ t, 0 ≤ F t)
       (hzero : ∀ a : ScheduledFrequencyIndex V n,
         ¬(∀ s ∈ allFrequencyList n (scheduledFrequencyHistory V n a), s ≠ 0) →
           F (scheduledFrequencyHistory V n a) = 0) :
       (∑ a, F (scheduledFrequencyHistory V n a)) ≤
         ∑ t : FrequencyTree ((transferFrequencyRange (V n)).erase 0) n,
           if frequencyLeafWeight (singleFrequencyLeaf ((transferFrequencyRange (V n)).erase 0)
             (V 0)) n t = 1 then F (frequencyTreeMap Subtype.val n t) else 0 := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.ScheduledFrequencyIndex, OAI.Ostmann.allFrequencyList, OAI.Ostmann.scheduledFrequencyHistory, OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.frequencyLeafWeight, OAI.Ostmann.singleFrequencyLeaf, OAI.Ostmann.frequencyTreeMap