Repository navigation
Expand file tree
/
Copy pathFixedCostGenerators.lean
More file actions
28 lines (26 loc) · 1.88 KB
/
Copy pathFixedCostGenerators.lean
File metadata and controls
28 lines (26 loc) · 1.88 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
import CollatzTargetDensity.FixedCostGenerators
#print CollatzTargetDensity.FixedCostGenerators.generator
#print CollatzTargetDensity.FixedCostGenerators.geometricProduct
#print CollatzTargetDensity.FixedCostGenerators.count
#check CollatzTargetDensity.FixedCostGenerators.pmf_eq_generator_value
#check CollatzTargetDensity.FixedCostGenerators.uniform_generator_value_lower
#check CollatzTargetDensity.FixedCostGenerators.central_zero_with_positive_value
#print axioms CollatzTargetDensity.FixedCostGenerators.two_pow_period
#print axioms CollatzTargetDensity.FixedCostGenerators.polynomialBoundary_explicit
#print axioms CollatzTargetDensity.FixedCostGenerators.value_succ
#print axioms CollatzTargetDensity.FixedCostGenerators.pmf_unroll
#print axioms CollatzTargetDensity.FixedCostGenerators.pmf_period_equation
#print axioms CollatzTargetDensity.FixedCostGenerators.geometricProduct_pos
#print axioms CollatzTargetDensity.FixedCostGenerators.geometricProduct_le_one
#print axioms CollatzTargetDensity.FixedCostGenerators.geometricProduct_ge_two_thirds
#print axioms CollatzTargetDensity.FixedCostGenerators.normalizer_mul_pmf_eq_value
#print axioms CollatzTargetDensity.FixedCostGenerators.pmf_eq_generator_value
#print axioms CollatzTargetDensity.FixedCostGenerators.sum_value_eq_normalizer
#print axioms CollatzTargetDensity.FixedCostGenerators.uniform_generator_value_lower
#print axioms CollatzTargetDensity.FixedCostGenerators.count_succ
#print axioms CollatzTargetDensity.FixedCostGenerators.count_succ_explicit
#print axioms CollatzTargetDensity.FixedCostGenerators.recursiveCount_eq_count
#print axioms CollatzTargetDensity.FixedCostGenerators.count_two_two_four
#print axioms CollatzTargetDensity.FixedCostGenerators.count_twelve_twelve_seven
#print axioms CollatzTargetDensity.FixedCostGenerators.count_twelve_twelve_one_pos
#print axioms CollatzTargetDensity.FixedCostGenerators.central_zero_with_positive_value