OAI/Combinatorics/PolynomialVacuum/Separator/Summability.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumCylinder.positiveSystemWeight line 10
2. theorem OAI.PolynomialVacuumCylinder.positiveSystemWeight_nonneg line 13
3. theorem OAI.PolynomialVacuumCylinder.systemWeight_two line 16
4. theorem OAI.PolynomialVacuumCylinder.finiteSeparatorSystems_tendsto line 20
5. theorem OAI.PolynomialVacuumCylinder.positiveSystemWeight_summable line 30
6. theorem OAI.PolynomialVacuumCylinder.systemWeight_norm_bound line 51
7. theorem OAI.PolynomialVacuumCylinder.separator_systems_summable line 66
8. theorem OAI.PolynomialVacuumCylinder.finite_separator_sums_tendsto line 70
9. theorem OAI.PolynomialVacuumCylinder.physical_limit_equals_separator line 75