OAI/NumberTheory/Jacobsthal/Partitions/CompletedParentInterval.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.ContinuousRatioBins.weightedRatioLaw line 19
2. theorem OAI.Erdos970.NumberTheoryLean.ContinuousRatioBins.weightedRatioLaw_eq_density line 22
3. theorem OAI.Erdos970.NumberTheoryLean.ContinuousRatioBins.weightedRatioLaw_probability line 33
4. theorem OAI.Erdos970.NumberTheoryLean.ContinuousRatioBins.weightedRatioLaw_even line 38
5. theorem OAI.Erdos970.NumberTheoryLean.ContinuousRatioBins.weightedRatioLaw_odd line 44
6. instance OAI.Erdos970.NumberTheoryLean.ContinuousRatioBins.ratioMeasure_noAtoms line 50
7. theorem OAI.Erdos970.NumberTheoryLean.ContinuousRatioBins.ratio_restrict_bin line 54
8. theorem OAI.Erdos970.NumberTheoryLean.ContinuousRatioBins.ratio_bin_mass line 60
9. def OAI.Erdos970.NumberTheoryLean.ContinuousRatioBins.continuousBin line 70
10. theorem OAI.Erdos970.NumberTheoryLean.ContinuousRatioBins.continuousBin_sandwich line 73
11. def OAI.Erdos970.NumberTheoryLean.ContinuousKilledBins.continuousChain line 131
12. instance OAI.Erdos970.NumberTheoryLean.ContinuousKilledBins.continuousChain_isMarkov line 134
13. def OAI.Erdos970.NumberTheoryLean.ContinuousKilledBins.ratioBinSet line 142
14. theorem OAI.Erdos970.NumberTheoryLean.ContinuousKilledBins.ratioBinSet_measurable line 144
15. theorem OAI.Erdos970.NumberTheoryLean.ContinuousKilledBins.costKernel_ratioLaw line 148
16. theorem OAI.Erdos970.NumberTheoryLean.ContinuousKilledBins.costKernel_bin line 164
17. theorem OAI.Erdos970.NumberTheoryLean.ContinuousKilledBins.lowKernel_full_bin line 170
18. theorem OAI.Erdos970.NumberTheoryLean.ContinuousKilledBins.continuousChain_full_bin line 198
19. theorem OAI.Erdos970.NumberTheoryLean.ContinuousKilledBins.continuousChain_full_bin_real line 205
20. theorem OAI.Erdos970.NumberTheoryLean.ContinuousIntervalUpper.transition_density_upper line 226
21. theorem OAI.Erdos970.NumberTheoryLean.ContinuousIntervalUpper.weighted_interval_upper line 245
22. def OAI.Erdos970.NumberTheoryLean.ContinuousIntervalUpper.closedCostBin line 256
23. theorem OAI.Erdos970.NumberTheoryLean.ContinuousIntervalUpper.closedCostBin_measurable line 259
24. theorem OAI.Erdos970.NumberTheoryLean.ContinuousIntervalUpper.costKernel_closedBin line 262
25. theorem OAI.Erdos970.NumberTheoryLean.ContinuousIntervalUpper.completed_interval_upper line 268
26. theorem OAI.Erdos970.NumberTheoryLean.CompletedParentInterval.completed_parent_interval_upper line 294