OAI/NumberTheory/Jacobsthal/Probability/FullPatternVariance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosLargePatternLaw.four_coordinate_count line 16
2. theorem OAI.Erdos970.ErdosLargePatternLaw.joint_condition_card line 50
3. theorem OAI.Erdos970.ErdosLargePatternLaw.joint_density_split line 65
4. theorem OAI.Erdos970.ErdosLargePatternLaw.joint_expectation line 71
5. theorem OAI.Erdos970.ErdosLargePatternLaw.single_expectation line 110
6. theorem OAI.Erdos970.ErdosLargePatternLaw.pair_expectation line 122
7. theorem OAI.Erdos970.ErdosLargePatternLaw.count_variance line 135
8. theorem OAI.Erdos970.ErdosLargePatternLaw.uniform_pattern_chebyshev line 152