OAI/NumberTheory/Ostmann/Arithmetic/BulkSlotPolynomials.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotData.CompensationAbsent line 12

   Source documentation

   A bulk coordinate never occurs in any compensation denominator.

   def MovingSlotData.CompensationAbsent {σ : Type*} (i : σ) :
       {n : ℕ} → MovingSlotData σ n → Prop
     | _, .leaf _ _ => True
     | _, .node _ _ _ u left right =>
         i ∉ u ∧ left.CompensationAbsent i ∧ right.CompensationAbsent i

   Mentions: OAI.Ostmann.MovingSlotData

2. theorem OAI.Ostmann.MovingSlotData.compensationAbsent_of_levels line 18
3. def OAI.Ostmann.bulkSlotProduct line 29
4. theorem OAI.Ostmann.bulkSlotProduct_eval line 33
5. theorem OAI.Ostmann.bulkSlotProduct_degree line 51
6. theorem OAI.Ostmann.realSlotProduct_update_of_absent line 62
7. def OAI.Ostmann.MovingSlotReversal.bulkPivotPolynomial line 75
8. theorem OAI.Ostmann.MovingSlotReversal.bulkPivotPolynomial_eval line 83
9. theorem OAI.Ostmann.MovingSlotReversal.bulkPivotPolynomial_degree line 92