OAI/NumberTheory/Jacobsthal/Analysis/DensityConservation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.IncomingDensityIdentities.incomingOdd line 15
2. def OAI.Erdos970.Erdos970Dependency.IncomingDensityIdentities.incomingEven line 17
3. theorem OAI.Erdos970.Erdos970Dependency.IncomingDensityIdentities.incomingOdd_formula line 20
4. theorem OAI.Erdos970.Erdos970Dependency.IncomingDensityIdentities.incomingEven_formula line 45
5. theorem OAI.Erdos970.Erdos970Dependency.IncomingDensityIdentities.incomingOdd_zero line 64
6. theorem OAI.Erdos970.Erdos970Dependency.IncomingDensityIdentities.incomingEven_zero line 70
7. theorem OAI.Erdos970.Erdos970Dependency.IncomingDensityIdentities.incomingOdd_integral line 77
8. theorem OAI.Erdos970.Erdos970Dependency.IncomingDensityIdentities.incomingEven_integral line 90
9. theorem OAI.Erdos970.Erdos970Dependency.IncomingDensityIdentities.incomingOdd_integrable line 103
10. theorem OAI.Erdos970.Erdos970Dependency.IncomingDensityIdentities.incomingEven_integrable line 117
11. theorem OAI.Erdos970.Erdos970Dependency.DensityConservation.kernel_density_conservation line 132