OAI/NumberTheory/Ostmann/Construction/ScheduledSourceScheme.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.ancestorNodeIndex_injective line 11
2. def OAI.Ostmann.scheduledSourceScheme line 29

   Source documentation

   Every ancestor is a genuine proper prefix of this node. The source products are constructed from H slots, rather than assumed coefficients.

   noncomputable def scheduledSourceScheme : PivotDependencyScheme (2 ^ n - 1) where
   …

   Mentions: OAI.Ostmann.PivotDependencyScheme

3. theorem OAI.Ostmann.scheduledSourceScheme_left line 43
4. theorem OAI.Ostmann.scheduledSourceScheme_right line 54
5. theorem OAI.Ostmann.scheduledSourceScheme_depth line 65
6. theorem OAI.Ostmann.scheduledSourceScheme_root_ne_zero line 69
7. theorem OAI.Ostmann.scheduledSourceScheme_frequency_dvd line 74
8. theorem OAI.Ostmann.scheduledSourceScheme_valid line 85

   Source documentation

   Literal integer node relations and coefficient units give the sampled history used by the existing residue-support estimate.

   theorem scheduledSourceScheme_valid
       (hinjL : ∀ j, Function.Injective (left j))
       (hinjR : ∀ j, Function.Injective (right j))
       (Q : ℕ) (a : SampledPivotHistory n Q)
       (hnode : ∀ j : Fin (2 ^ n - 1),
         let f := singleTreeNodeFrequencies S n t j.val
   …

   Mentions: OAI.Ostmann.SampledPivotHistory, OAI.Ostmann.singleTreeNodeFrequencies