OAI/Combinatorics/Progressions/Probability/AllocatedRecoveredChartMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.jointIntegerFullChart_normalized_spatial_top line 17
2. theorem OAI.Erdos3.VectorPolynomial.layerSamplerBox_sum_le_zero_root_budget line 41
3. theorem OAI.Erdos3.VectorPolynomial.allocatedRecoveredIntegerFullChart_spatial_top_mass line 49
4. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenIntegerFullChart_spatial_top_mass line 84
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_normalized_top_tag_mass line 154
6. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_normalized_top_mass line 176
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_frozen_normalized_top_mass line 213