OAI/NumberTheory/Ostmann/Characters/TemplateSourcePivotLossBasic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourcePivotCountBound line 13
2. def OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourcePivotLoss line 15
3. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourcePivotCountBound_pos line 18
4. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourcePivotLoss_nonneg line 22
5. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.log_factorial_le_square line 28
6. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.pivot_factor_le_sourcePivotLoss line 38
7. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.eventually_pivot_leading_budget line 59
8. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.eventually_sourcePivotLoss_budget line 71