OAI/NumberTheory/Ostmann/Construction/PairedScheduledHistory.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.pairFrequencyTrees line 11
2. theorem OAI.Ostmann.frequencyPairProjection_pair line 17
3. theorem OAI.Ostmann.pairFrequencyTrees_projections line 29
4. def OAI.Ostmann.pairedFrequencyEquiv line 47

   Source documentation

   No multiplicity is lost when the two independent descendant histories are placed in the paired tree used by the arithmetic norm estimate.

   def pairedFrequencyEquiv (S : Finset ℤ) (n : ℕ) :
       (FrequencyTree S n × FrequencyTree S n) ≃ FrequencyTree (S × S) n where
   …

   Mentions: OAI.Ostmann.FrequencyTree

5. def OAI.Ostmann.pairedScheduledHistoryEmbedding line 54
6. theorem OAI.Ostmann.pairedScheduledHistoryEmbedding_projection line 61
7. theorem OAI.Ostmann.pairedScheduledHistoryEmbedding_leaf line 75

   Source documentation

   Passing to a common internal cutoff retains the actual bottom cutoff on both sides of the original square.

   theorem pairedScheduledHistoryEmbedding_leaf (V : ℕ → ℕ) (hV : Monotone V) (n : ℕ)
       (a : NonzeroScheduledHistory V n × NonzeroScheduledHistory V n) :
       frequencyLeafWeight (pairedFrequencyLeaf ((transferFrequencyRange (V n)).erase 0) (V 0)) n
         (pairedScheduledHistoryEmbedding V hV n a) = 1 := by
   …

   Mentions: OAI.Ostmann.NonzeroScheduledHistory, OAI.Ostmann.frequencyLeafWeight, OAI.Ostmann.pairedFrequencyLeaf, OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.pairedScheduledHistoryEmbedding