OAI/NumberTheory/Ostmann/Construction/SmoothHistoryFactor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.History.compensationProduct line 10
2. def OAI.Ostmann.Construction.History.cellWeight line 13
3. theorem OAI.Ostmann.Construction.History.compensationProduct_node line 17
4. theorem OAI.Ostmann.Construction.History.realWeight_eq_compensation_cellWeight line 23
5. theorem OAI.Ostmann.Construction.History.cellWeight_bounds line 32
6. def OAI.Ostmann.Construction.smoothHistoryScalar line 46
7. theorem OAI.Ostmann.Construction.history_weight_eq_compensation_smooth_spectator line 50