OAI/NumberTheory/Jacobsthal/Analysis/DeficitIntegralValues.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.Erdos970Dependency.DeficitIntegralValues.shift_indicator line 15
2. theorem OAI.Erdos970.Erdos970Dependency.DeficitIntegralValues.integrableOn_shift_Ioi line 24
3. theorem OAI.Erdos970.Erdos970Dependency.DeficitIntegralValues.integral_shift_Ioi line 30
4. theorem OAI.Erdos970.Erdos970Dependency.DeficitIntegralValues.upper_integral_one line 36
5. theorem OAI.Erdos970.Erdos970Dependency.DeficitIntegralValues.lower_integral_zero line 44
6. theorem OAI.Erdos970.Erdos970Dependency.DeficitIntegralValues.lower_integral_two line 52
7. theorem OAI.Erdos970.Erdos970Dependency.DeficitIntegralValues.even_majorant_integral line 61
8. theorem OAI.Erdos970.Erdos970Dependency.DeficitIntegralValues.odd_majorant_integral line 74