Showcase Summary🔗

Overview

Total entries45completed: 45; deps incomplete: 0; sorries: 0; no proof: 0

Ready now0Entries whose next formalization step is currently unblocked.

Fully closed45Local code and prerequisite closure are both complete.

Actionable priorities0Entries ready now and already unlocking downstream work.

Entry index (45)

Definitions14completed: 14; deps incomplete: 0; sorries: 0; no proof: 0

Lemmas18completed: 18; deps incomplete: 0; sorries: 0; no proof: 0

Theorems13completed: 13; deps incomplete: 0; sorries: 0; no proof: 0

Definition Index (14)

Definition bpSeries(Definition)
Associated lean decls (1)
- bpSeries
Definition bit(Definition)
Associated lean decls (1)
- A362583.bit
Definition χ(Definition)
Associated lean decls (1)
- A362583.χ
Definition fChi(Definition)
Associated lean decls (1)
- A362583.fChi
Definition raceSum(Definition)
Associated lean decls (1)
- A362583.raceSum
Definition contLog(Definition)
Associated lean decls (1)
- A362583.contLog
Definition tp(Definition)
Associated lean decls (1)
- A362583.tp
Definition layerBReal(Definition)
Associated lean decls (1)
- A362583.layerBReal
Definition layerT(Definition)
Associated lean decls (1)
- A362583.layerT
Definition raceKernel(Definition)
Associated lean decls (1)
- A362583.raceKernel
Definition layerA(Definition)
Associated lean decls (1)
- A362583.layerA
Definition ϱ(Definition)
Associated lean decls (1)
- A362583.ϱ
Definition layerB(Definition)
Associated lean decls (1)
- A362583.layerB
Definition oddPrime(Definition)
Associated lean decls (1)
- A362583.oddPrime

Theorem / Proposition / Lemma / Corollary Index (31)

Theorem tsum_mul_cpow_neg_eq_bpSeries(Theorem)
Associated lean decls (1)
- tsum_mul_cpow_neg_eq_bpSeries
Theorem raceSum_linear_of_eventuallyPeriodic(Theorem)
Associated lean decls (1)
- A362583.raceSum_linear_of_eventuallyPeriodic
Lemma norm_bpSeries_term_le(Lemma)
Associated lean decls (1)
- norm_bpSeries_term_le
Theorem bits_infinite_ones(Theorem)
Associated lean decls (1)
- A362583.bits_infinite_ones
Theorem eventuallyPeriodic_of_not_irrational(Theorem)
Associated lean decls (1)
- A362583.eventuallyPeriodic_of_not_irrational
Lemma sum_range_norm_bpSeries_le(Lemma)
Associated lean decls (1)
- sum_range_norm_bpSeries_le
Theorem irrational_ϱ(Theorem)
Associated lean decls (1)
- A362583.irrational_ϱ
Lemma norm_bpSeries_term_le_boxBound(Lemma)
Associated lean decls (1)
- norm_bpSeries_term_le_boxBound
Lemma norm_bpSeries_le(Lemma)
Associated lean decls (1)
- norm_bpSeries_le
Lemma differentiableOn_bpSeries_term(Lemma)
Associated lean decls (1)
- differentiableOn_bpSeries_term
Lemma Complex.norm_natCast_cpow_sub_add_one_cpow_le(Lemma)
Associated lean decls (1)
- Complex.norm_natCast_cpow_sub_add_one_cpow_le
Lemma neg_log_split(Lemma)
Associated lean decls (1)
- A362583.neg_log_split
Lemma exists_norm_LFunction_lt_near_half(Lemma)
Associated lean decls (1)
- A362583.exists_norm_LFunction_lt_near_half
Theorem exp_contLog_eqOn(Theorem)
Associated lean decls (1)
- A362583.exp_contLog_eqOn
Lemma norm_bpSeries_le_const(Lemma)
Associated lean decls (1)
- norm_bpSeries_le_const
Theorem c_eq_zero_of_raceSum_linear(Theorem)
Associated lean decls (1)
- A362583.c_eq_zero_of_raceSum_linear
Lemma exists_layerBReal_gt(Lemma)
Associated lean decls (1)
- A362583.exists_layerBReal_gt
Theorem raceSum_not_linear(Theorem)
Associated lean decls (1)
- A362583.raceSum_not_linear
Theorem differentiableOn_bpSeries(Theorem)
Associated lean decls (1)
- differentiableOn_bpSeries
Lemma hasSum_neg_log_one_sub(Lemma)
Associated lean decls (1)
- A362583.hasSum_neg_log_one_sub
Theorem differentiableOn_bpSeries_box(Theorem)
Associated lean decls (1)
- differentiableOn_bpSeries_box
Lemma summable_bpSeries_boxBound(Lemma)
Associated lean decls (1)
- summable_bpSeries_boxBound
Lemma layerBReal_sub_le_re_contLog(Lemma)
Associated lean decls (1)
- A362583.layerBReal_sub_le_re_contLog
Lemma tendsto_boundary_term(Lemma)
Associated lean decls (1)
- tendsto_boundary_term
Theorem exp_layers_eq_LFunction(Theorem)
Associated lean decls (1)
- A362583.exp_layers_eq_LFunction
Lemma sum_range_fChi(Lemma)
Associated lean decls (1)
- A362583.sum_range_fChi
Lemma exists_one_lt_tsum_primes_rpow_gt(Lemma)
Associated lean decls (1)
- A362583.exists_one_lt_tsum_primes_rpow_gt
Theorem bits_infinite_zeros(Theorem)
Associated lean decls (1)
- A362583.bits_infinite_zeros
Lemma layerA_eq_tsum_fChi(Lemma)
Associated lean decls (1)
- A362583.layerA_eq_tsum_fChi
Theorem tsum_neg_log_eq_layers(Theorem)
Associated lean decls (1)
- A362583.tsum_neg_log_eq_layers
Lemma norm_LFunction_eq_exp_re_contLog(Lemma)
Associated lean decls (1)
- A362583.norm_LFunction_eq_exp_re_contLog

By parent groups (5)

The mod-4 character, the k = 2 and k ≥ 3 layers of the Euler-product logarithm, the power series of the logarithm, and the divergence transfer. (4)

Lemma exists_one_lt_tsum_primes_rpow_gt(Lemma)
Associated lean decls (1)
- A362583.exists_one_lt_tsum_primes_rpow_gt
Lemma hasSum_neg_log_one_sub(Lemma)
Associated lean decls (1)
- A362583.hasSum_neg_log_one_sub
Lemma exists_layerBReal_gt(Lemma)
Associated lean decls (1)
- A362583.exists_layerBReal_gt
Lemma neg_log_split(Lemma)
Associated lean decls (1)
- A362583.neg_log_split

Dirichlet series with bounded partial sums: the by-parts series is the analytic continuation to the right half-plane. (12)

Lemma tendsto_boundary_term(Lemma)
Associated lean decls (1)
- tendsto_boundary_term
Lemma summable_bpSeries_boxBound(Lemma)
Associated lean decls (1)
- summable_bpSeries_boxBound
Theorem differentiableOn_bpSeries_box(Theorem)
Associated lean decls (1)
- differentiableOn_bpSeries_box
Theorem differentiableOn_bpSeries(Theorem)
Associated lean decls (1)
- differentiableOn_bpSeries
Lemma norm_bpSeries_le_const(Lemma)
Associated lean decls (1)
- norm_bpSeries_le_const
Lemma Complex.norm_natCast_cpow_sub_add_one_cpow_le(Lemma)
Associated lean decls (1)
- Complex.norm_natCast_cpow_sub_add_one_cpow_le
Lemma differentiableOn_bpSeries_term(Lemma)
Associated lean decls (1)
- differentiableOn_bpSeries_term
Lemma norm_bpSeries_le(Lemma)
Associated lean decls (1)
- norm_bpSeries_le
Lemma norm_bpSeries_term_le_boxBound(Lemma)
Associated lean decls (1)
- norm_bpSeries_term_le_boxBound
Lemma sum_range_norm_bpSeries_le(Lemma)
Associated lean decls (1)
- sum_range_norm_bpSeries_le
Lemma norm_bpSeries_term_le(Lemma)
Associated lean decls (1)
- norm_bpSeries_term_le
Theorem tsum_mul_cpow_neg_eq_bpSeries(Theorem)
Associated lean decls (1)
- tsum_mul_cpow_neg_eq_bpSeries

The k = 1 layer, the split of the Euler-product logarithm into layers, the identity exp(A + B + T) = L(s, χ), and the coefficient bridge to the race sum. (4)

Theorem tsum_neg_log_eq_layers(Theorem)
Associated lean decls (1)
- A362583.tsum_neg_log_eq_layers
Lemma layerA_eq_tsum_fChi(Lemma)
Associated lean decls (1)
- A362583.layerA_eq_tsum_fChi
Lemma sum_range_fChi(Lemma)
Associated lean decls (1)
- A362583.sum_range_fChi
Theorem exp_layers_eq_LFunction(Theorem)
Associated lean decls (1)
- A362583.exp_layers_eq_LFunction

The case c = 0: a bounded race would continue log L(s, χ₄) past Re s = 1/2 minus an explicitly divergent term — which the finite value L(1/2, χ₄) forbids. (5)

Lemma norm_LFunction_eq_exp_re_contLog(Lemma)
Associated lean decls (1)
- A362583.norm_LFunction_eq_exp_re_contLog
Lemma layerBReal_sub_le_re_contLog(Lemma)
Associated lean decls (1)
- A362583.layerBReal_sub_le_re_contLog
Theorem raceSum_not_linear(Theorem)
Associated lean decls (1)
- A362583.raceSum_not_linear
Theorem exp_contLog_eqOn(Theorem)
Associated lean decls (1)
- A362583.exp_contLog_eqOn
Lemma exists_norm_LFunction_lt_near_half(Lemma)
Associated lean decls (1)
- A362583.exists_norm_LFunction_lt_near_half

The digit sequence has infinitely many ones and infinitely many zeros; and a rational constant would have eventually periodic digits. (3)

Theorem bits_infinite_zeros(Theorem)
Associated lean decls (1)
- A362583.bits_infinite_zeros
Theorem eventuallyPeriodic_of_not_irrational(Theorem)
Associated lean decls (1)
- A362583.eventuallyPeriodic_of_not_irrational
Theorem bits_infinite_ones(Theorem)
Associated lean decls (1)
- A362583.bits_infinite_ones

Dependency insights

Statement-used entries44Entries reused in statement dependencies.

Tracked parent groups6Grouped health rollups for parents with more than one child entry.

Most used in statements (44)

Definition bpSeries(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 12proof uses: 0direct uses: 12downstream unlocks: 18
Associated lean decls (1)
- bpSeries
Definition χ(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 10proof uses: 0direct uses: 10downstream unlocks: 15
Associated lean decls (1)
- A362583.χ
Definition fChi(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 9
Associated lean decls (1)
- A362583.fChi
Definition layerB(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 12
Associated lean decls (1)
- A362583.layerB
Definition raceKernel(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 20
Associated lean decls (1)
- A362583.raceKernel
Definition bit(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 6
Associated lean decls (1)
- A362583.bit
Definition layerT(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 9
Associated lean decls (1)
- A362583.layerT
Definition contLog(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 5
Associated lean decls (1)
- A362583.contLog
Definition raceSum(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 5
Associated lean decls (1)
- A362583.raceSum
Definition tp(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 11
Associated lean decls (1)
- A362583.tp
Show all 34 more statement-used entries
- Definition layerA(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 8
  Associated lean decls (1)
  - A362583.layerA
- Definition oddPrime(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 7
  Associated lean decls (1)
  - A362583.oddPrime
- Definition layerBReal(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 4
  Associated lean decls (1)
  - A362583.layerBReal
- Theorem tsum_mul_cpow_neg_eq_bpSeries(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - tsum_mul_cpow_neg_eq_bpSeries
- Theorem exp_layers_eq_LFunction(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - A362583.exp_layers_eq_LFunction
- Lemma norm_bpSeries_le_const(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (1)
  - norm_bpSeries_le_const
- Definition ϱ(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - A362583.ϱ
- Lemma hasSum_neg_log_one_sub(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (1)
  - A362583.hasSum_neg_log_one_sub
- Lemma Complex.norm_natCast_cpow_sub_add_one_cpow_le(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
  Associated lean decls (1)
  - Complex.norm_natCast_cpow_sub_add_one_cpow_le
- Lemma neg_log_split(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
  Associated lean decls (1)
  - A362583.neg_log_split
- Lemma norm_bpSeries_term_le(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
  Associated lean decls (1)
  - norm_bpSeries_term_le
- Lemma tendsto_boundary_term(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - tendsto_boundary_term
- Lemma summable_bpSeries_boxBound(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - summable_bpSeries_boxBound
- Lemma sum_range_norm_bpSeries_le(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - sum_range_norm_bpSeries_le
- Lemma norm_bpSeries_term_le_boxBound(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - norm_bpSeries_term_le_boxBound
- Lemma differentiableOn_bpSeries_term(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - differentiableOn_bpSeries_term
- Theorem tsum_neg_log_eq_layers(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - A362583.tsum_neg_log_eq_layers
- Lemma norm_bpSeries_le(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (1)
  - norm_bpSeries_le
- Theorem differentiableOn_bpSeries_box(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (1)
  - differentiableOn_bpSeries_box
- Theorem differentiableOn_bpSeries(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - differentiableOn_bpSeries
- Lemma sum_range_fChi(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - A362583.sum_range_fChi
- Lemma layerA_eq_tsum_fChi(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - A362583.layerA_eq_tsum_fChi
- Lemma exists_one_lt_tsum_primes_rpow_gt(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - A362583.exists_one_lt_tsum_primes_rpow_gt
- Theorem exp_contLog_eqOn(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - A362583.exp_contLog_eqOn
- Lemma exists_norm_LFunction_lt_near_half(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - A362583.exists_norm_LFunction_lt_near_half
- Lemma exists_layerBReal_gt(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - A362583.exists_layerBReal_gt
- Lemma layerBReal_sub_le_re_contLog(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - A362583.layerBReal_sub_le_re_contLog
- Lemma norm_LFunction_eq_exp_re_contLog(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - A362583.norm_LFunction_eq_exp_re_contLog
- Theorem bits_infinite_ones(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - A362583.bits_infinite_ones
- Theorem bits_infinite_zeros(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - A362583.bits_infinite_zeros
- Theorem c_eq_zero_of_raceSum_linear(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - A362583.c_eq_zero_of_raceSum_linear
- Theorem eventuallyPeriodic_of_not_irrational(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - A362583.eventuallyPeriodic_of_not_irrational
- Theorem raceSum_linear_of_eventuallyPeriodic(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - A362583.raceSum_linear_of_eventuallyPeriodic
- Theorem raceSum_not_linear(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - A362583.raceSum_not_linear

Group health (6)

The mod-4 character, the k = 2 and k ≥ 3 layers of the Euler-product logarithm, the power series of the logarithm, and the divergence transfer.layers

Grouped view over entries sharing the same parent.

total: 10closed: 10local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 91

Next: no ready child currently unlocks downstream work.
Dirichlet series with bounded partial sums: the by-parts series is the analytic continuation to the right half-plane.n1

Grouped view over entries sharing the same parent.

total: 13closed: 13local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 85

Next: no ready child currently unlocks downstream work.
The k = 1 layer, the split of the Euler-product logarithm into layers, the identity exp(A + B + T) = L(s, χ), and the coefficient bridge to the race sum.euler

Grouped view over entries sharing the same parent.

total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 34

Next: no ready child currently unlocks downstream work.
The odd primes in order, the mod-4 digit each contributes, the constant they define, and the Chebyshev race sum.defs

Grouped view over entries sharing the same parent.

total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 20

Next: no ready child currently unlocks downstream work.
The case c = 0: a bounded race would continue log L(s, χ₄) past Re s = 1/2 minus an explicitly divergent term — which the finite value L(1/2, χ₄) forbids.czero

Grouped view over entries sharing the same parent.

total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 15

Next: no ready child currently unlocks downstream work.
The digit sequence has infinitely many ones and infinitely many zeros; and a rational constant would have eventually periodic digits.digit

Grouped view over entries sharing the same parent.

total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 5

Next: no ready child currently unlocks downstream work.

Metadata

Metadata audit

Missing owner45

Missing effort45

Untagged45

Missing owner (45)

Definition bit(Definition)

Missing owner metadata.
Associated lean decls (1)
- A362583.bit
Definition bpSeries(Definition)

Missing owner metadata.
Associated lean decls (1)
- bpSeries
Definition χ(Definition)

Missing owner metadata.
Associated lean decls (1)
- A362583.χ
Definition contLog(Definition)

Missing owner metadata.
Associated lean decls (1)
- A362583.contLog
Definition fChi(Definition)

Missing owner metadata.
Associated lean decls (1)
- A362583.fChi
Definition layerA(Definition)

Missing owner metadata.
Associated lean decls (1)
- A362583.layerA
Definition layerBReal(Definition)

Missing owner metadata.
Associated lean decls (1)
- A362583.layerBReal
Definition layerB(Definition)

Missing owner metadata.
Associated lean decls (1)
- A362583.layerB
Definition layerT(Definition)

Missing owner metadata.
Associated lean decls (1)
- A362583.layerT
Definition oddPrime(Definition)

Missing owner metadata.
Associated lean decls (1)
- A362583.oddPrime
Show all 35 more entries missing owner
- Definition raceKernel(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.raceKernel
- Definition raceSum(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.raceSum
- Definition ϱ(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.ϱ
- Definition tp(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.tp
- Lemma exists_norm_LFunction_lt_near_half(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.exists_norm_LFunction_lt_near_half
- Lemma tendsto_boundary_term(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - tendsto_boundary_term
- Lemma summable_bpSeries_boxBound(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - summable_bpSeries_boxBound
- Lemma norm_bpSeries_le_const(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - norm_bpSeries_le_const
- Lemma norm_bpSeries_le(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - norm_bpSeries_le
- Lemma exists_layerBReal_gt(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.exists_layerBReal_gt
- Lemma sum_range_fChi(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.sum_range_fChi
- Lemma Complex.norm_natCast_cpow_sub_add_one_cpow_le(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Complex.norm_natCast_cpow_sub_add_one_cpow_le
- Lemma layerA_eq_tsum_fChi(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.layerA_eq_tsum_fChi
- Lemma layerBReal_sub_le_re_contLog(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.layerBReal_sub_le_re_contLog
- Lemma hasSum_neg_log_one_sub(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.hasSum_neg_log_one_sub
- Lemma neg_log_split(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.neg_log_split
- Lemma norm_LFunction_eq_exp_re_contLog(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.norm_LFunction_eq_exp_re_contLog
- Lemma sum_range_norm_bpSeries_le(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - sum_range_norm_bpSeries_le
- Lemma exists_one_lt_tsum_primes_rpow_gt(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.exists_one_lt_tsum_primes_rpow_gt
- Lemma norm_bpSeries_term_le_boxBound(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - norm_bpSeries_term_le_boxBound
- Lemma differentiableOn_bpSeries_term(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - differentiableOn_bpSeries_term
- Lemma norm_bpSeries_term_le(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - norm_bpSeries_term_le
- Theorem bits_infinite_ones(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.bits_infinite_ones
- Theorem bits_infinite_zeros(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.bits_infinite_zeros
- Theorem tsum_mul_cpow_neg_eq_bpSeries(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - tsum_mul_cpow_neg_eq_bpSeries
- Theorem differentiableOn_bpSeries_box(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - differentiableOn_bpSeries_box
- Theorem differentiableOn_bpSeries(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - differentiableOn_bpSeries
- Theorem c_eq_zero_of_raceSum_linear(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.c_eq_zero_of_raceSum_linear
- Theorem exp_contLog_eqOn(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.exp_contLog_eqOn
- Theorem eventuallyPeriodic_of_not_irrational(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.eventuallyPeriodic_of_not_irrational
- Theorem exp_layers_eq_LFunction(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.exp_layers_eq_LFunction
- Theorem irrational_ϱ(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.irrational_ϱ
- Theorem raceSum_linear_of_eventuallyPeriodic(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.raceSum_linear_of_eventuallyPeriodic
- Theorem raceSum_not_linear(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.raceSum_not_linear
- Theorem tsum_neg_log_eq_layers(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - A362583.tsum_neg_log_eq_layers

Missing effort (45)

Definition bit(Definition)

Missing effort metadata.
Associated lean decls (1)
- A362583.bit
Definition bpSeries(Definition)

Missing effort metadata.
Associated lean decls (1)
- bpSeries
Definition χ(Definition)

Missing effort metadata.
Associated lean decls (1)
- A362583.χ
Definition contLog(Definition)

Missing effort metadata.
Associated lean decls (1)
- A362583.contLog
Definition fChi(Definition)

Missing effort metadata.
Associated lean decls (1)
- A362583.fChi
Definition layerA(Definition)

Missing effort metadata.
Associated lean decls (1)
- A362583.layerA
Definition layerBReal(Definition)

Missing effort metadata.
Associated lean decls (1)
- A362583.layerBReal
Definition layerB(Definition)

Missing effort metadata.
Associated lean decls (1)
- A362583.layerB
Definition layerT(Definition)

Missing effort metadata.
Associated lean decls (1)
- A362583.layerT
Definition oddPrime(Definition)

Missing effort metadata.
Associated lean decls (1)
- A362583.oddPrime
Show all 35 more entries missing effort
- Definition raceKernel(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.raceKernel
- Definition raceSum(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.raceSum
- Definition ϱ(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.ϱ
- Definition tp(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.tp
- Lemma exists_norm_LFunction_lt_near_half(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.exists_norm_LFunction_lt_near_half
- Lemma tendsto_boundary_term(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - tendsto_boundary_term
- Lemma summable_bpSeries_boxBound(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - summable_bpSeries_boxBound
- Lemma norm_bpSeries_le_const(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - norm_bpSeries_le_const
- Lemma norm_bpSeries_le(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - norm_bpSeries_le
- Lemma exists_layerBReal_gt(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.exists_layerBReal_gt
- Lemma sum_range_fChi(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.sum_range_fChi
- Lemma Complex.norm_natCast_cpow_sub_add_one_cpow_le(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Complex.norm_natCast_cpow_sub_add_one_cpow_le
- Lemma layerA_eq_tsum_fChi(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.layerA_eq_tsum_fChi
- Lemma layerBReal_sub_le_re_contLog(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.layerBReal_sub_le_re_contLog
- Lemma hasSum_neg_log_one_sub(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.hasSum_neg_log_one_sub
- Lemma neg_log_split(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.neg_log_split
- Lemma norm_LFunction_eq_exp_re_contLog(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.norm_LFunction_eq_exp_re_contLog
- Lemma sum_range_norm_bpSeries_le(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - sum_range_norm_bpSeries_le
- Lemma exists_one_lt_tsum_primes_rpow_gt(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.exists_one_lt_tsum_primes_rpow_gt
- Lemma norm_bpSeries_term_le_boxBound(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - norm_bpSeries_term_le_boxBound
- Lemma differentiableOn_bpSeries_term(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - differentiableOn_bpSeries_term
- Lemma norm_bpSeries_term_le(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - norm_bpSeries_term_le
- Theorem bits_infinite_ones(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.bits_infinite_ones
- Theorem bits_infinite_zeros(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.bits_infinite_zeros
- Theorem tsum_mul_cpow_neg_eq_bpSeries(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - tsum_mul_cpow_neg_eq_bpSeries
- Theorem differentiableOn_bpSeries_box(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - differentiableOn_bpSeries_box
- Theorem differentiableOn_bpSeries(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - differentiableOn_bpSeries
- Theorem c_eq_zero_of_raceSum_linear(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.c_eq_zero_of_raceSum_linear
- Theorem exp_contLog_eqOn(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.exp_contLog_eqOn
- Theorem eventuallyPeriodic_of_not_irrational(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.eventuallyPeriodic_of_not_irrational
- Theorem exp_layers_eq_LFunction(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.exp_layers_eq_LFunction
- Theorem irrational_ϱ(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.irrational_ϱ
- Theorem raceSum_linear_of_eventuallyPeriodic(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.raceSum_linear_of_eventuallyPeriodic
- Theorem raceSum_not_linear(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.raceSum_not_linear
- Theorem tsum_neg_log_eq_layers(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - A362583.tsum_neg_log_eq_layers

Untagged (45)

Definition bit(Definition)

Missing tag metadata.
Associated lean decls (1)
- A362583.bit
Definition bpSeries(Definition)

Missing tag metadata.
Associated lean decls (1)
- bpSeries
Definition χ(Definition)

Missing tag metadata.
Associated lean decls (1)
- A362583.χ
Definition contLog(Definition)

Missing tag metadata.
Associated lean decls (1)
- A362583.contLog
Definition fChi(Definition)

Missing tag metadata.
Associated lean decls (1)
- A362583.fChi
Definition layerA(Definition)

Missing tag metadata.
Associated lean decls (1)
- A362583.layerA
Definition layerBReal(Definition)

Missing tag metadata.
Associated lean decls (1)
- A362583.layerBReal
Definition layerB(Definition)

Missing tag metadata.
Associated lean decls (1)
- A362583.layerB
Definition layerT(Definition)

Missing tag metadata.
Associated lean decls (1)
- A362583.layerT
Definition oddPrime(Definition)

Missing tag metadata.
Associated lean decls (1)
- A362583.oddPrime
Show all 35 more untagged entries
- Definition raceKernel(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.raceKernel
- Definition raceSum(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.raceSum
- Definition ϱ(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.ϱ
- Definition tp(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.tp
- Lemma exists_norm_LFunction_lt_near_half(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.exists_norm_LFunction_lt_near_half
- Lemma tendsto_boundary_term(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - tendsto_boundary_term
- Lemma summable_bpSeries_boxBound(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - summable_bpSeries_boxBound
- Lemma norm_bpSeries_le_const(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - norm_bpSeries_le_const
- Lemma norm_bpSeries_le(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - norm_bpSeries_le
- Lemma exists_layerBReal_gt(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.exists_layerBReal_gt
- Lemma sum_range_fChi(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.sum_range_fChi
- Lemma Complex.norm_natCast_cpow_sub_add_one_cpow_le(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Complex.norm_natCast_cpow_sub_add_one_cpow_le
- Lemma layerA_eq_tsum_fChi(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.layerA_eq_tsum_fChi
- Lemma layerBReal_sub_le_re_contLog(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.layerBReal_sub_le_re_contLog
- Lemma hasSum_neg_log_one_sub(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.hasSum_neg_log_one_sub
- Lemma neg_log_split(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.neg_log_split
- Lemma norm_LFunction_eq_exp_re_contLog(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.norm_LFunction_eq_exp_re_contLog
- Lemma sum_range_norm_bpSeries_le(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - sum_range_norm_bpSeries_le
- Lemma exists_one_lt_tsum_primes_rpow_gt(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.exists_one_lt_tsum_primes_rpow_gt
- Lemma norm_bpSeries_term_le_boxBound(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - norm_bpSeries_term_le_boxBound
- Lemma differentiableOn_bpSeries_term(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - differentiableOn_bpSeries_term
- Lemma norm_bpSeries_term_le(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - norm_bpSeries_term_le
- Theorem bits_infinite_ones(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.bits_infinite_ones
- Theorem bits_infinite_zeros(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.bits_infinite_zeros
- Theorem tsum_mul_cpow_neg_eq_bpSeries(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - tsum_mul_cpow_neg_eq_bpSeries
- Theorem differentiableOn_bpSeries_box(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - differentiableOn_bpSeries_box
- Theorem differentiableOn_bpSeries(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - differentiableOn_bpSeries
- Theorem c_eq_zero_of_raceSum_linear(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.c_eq_zero_of_raceSum_linear
- Theorem exp_contLog_eqOn(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.exp_contLog_eqOn
- Theorem eventuallyPeriodic_of_not_irrational(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.eventuallyPeriodic_of_not_irrational
- Theorem exp_layers_eq_LFunction(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.exp_layers_eq_LFunction
- Theorem irrational_ϱ(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.irrational_ϱ
- Theorem raceSum_linear_of_eventuallyPeriodic(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.raceSum_linear_of_eventuallyPeriodic
- Theorem raceSum_not_linear(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.raceSum_not_linear
- Theorem tsum_neg_log_eq_layers(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - A362583.tsum_neg_log_eq_layers

Structure and coverage

Fully closed45Local code and ancestor closure are both complete.

Heaviest prerequisites (38)

Theorem raceSum_not_linear(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 10statement deps: 10proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
- A362583.raceSum_not_linear
Theorem c_eq_zero_of_raceSum_linear(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 8statement deps: 8proof deps: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
- A362583.c_eq_zero_of_raceSum_linear
Lemma layerBReal_sub_le_re_contLog(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 7statement deps: 7proof deps: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
- A362583.layerBReal_sub_le_re_contLog
Theorem exp_contLog_eqOn(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- A362583.exp_contLog_eqOn
Theorem tsum_neg_log_eq_layers(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 6
Associated lean decls (1)
- A362583.tsum_neg_log_eq_layers
Theorem exp_layers_eq_LFunction(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 5statement deps: 5proof deps: 0direct uses: 2downstream unlocks: 5
Associated lean decls (1)
- A362583.exp_layers_eq_LFunction
Definition contLog(Definition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 4downstream unlocks: 5
Associated lean decls (1)
- A362583.contLog
Lemma layerA_eq_tsum_fChi(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- A362583.layerA_eq_tsum_fChi
Lemma neg_log_split(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 7
Associated lean decls (1)
- A362583.neg_log_split
Lemma norm_LFunction_eq_exp_re_contLog(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
- A362583.norm_LFunction_eq_exp_re_contLog
Show all 28 more heaviest-prerequisite entries
- Theorem differentiableOn_bpSeries_box(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (1)
  - differentiableOn_bpSeries_box
- Theorem eventuallyPeriodic_of_not_irrational(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - A362583.eventuallyPeriodic_of_not_irrational
- Theorem irrational_ϱ(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - A362583.irrational_ϱ
- Lemma sum_range_fChi(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - A362583.sum_range_fChi
- Lemma norm_bpSeries_le_const(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (1)
  - norm_bpSeries_le_const
- Lemma norm_bpSeries_le(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (1)
  - norm_bpSeries_le
- Lemma norm_bpSeries_term_le_boxBound(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - norm_bpSeries_term_le_boxBound
- Theorem bits_infinite_ones(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - A362583.bits_infinite_ones
- Theorem bits_infinite_zeros(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - A362583.bits_infinite_zeros
- Theorem tsum_mul_cpow_neg_eq_bpSeries(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - tsum_mul_cpow_neg_eq_bpSeries
- Theorem differentiableOn_bpSeries(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - differentiableOn_bpSeries
- Theorem raceSum_linear_of_eventuallyPeriodic(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - A362583.raceSum_linear_of_eventuallyPeriodic
- Definition bit(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 6
  Associated lean decls (1)
  - A362583.bit
- Definition χ(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 10downstream unlocks: 15
  Associated lean decls (1)
  - A362583.χ
- Definition fChi(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 8downstream unlocks: 9
  Associated lean decls (1)
  - A362583.fChi
- Definition layerA(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 8
  Associated lean decls (1)
  - A362583.layerA
- Definition layerBReal(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 4
  Associated lean decls (1)
  - A362583.layerBReal
- Definition layerT(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 9
  Associated lean decls (1)
  - A362583.layerT
- Definition raceSum(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 5
  Associated lean decls (1)
  - A362583.raceSum
- Definition ϱ(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - A362583.ϱ
- Definition tp(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 11
  Associated lean decls (1)
  - A362583.tp
- Lemma exists_norm_LFunction_lt_near_half(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - A362583.exists_norm_LFunction_lt_near_half
- Lemma tendsto_boundary_term(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - tendsto_boundary_term
- Lemma summable_bpSeries_boxBound(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - summable_bpSeries_boxBound
- Lemma exists_layerBReal_gt(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - A362583.exists_layerBReal_gt
- Lemma sum_range_norm_bpSeries_le(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - sum_range_norm_bpSeries_le
- Lemma differentiableOn_bpSeries_term(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - differentiableOn_bpSeries_term
- Lemma norm_bpSeries_term_le(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 7
  Associated lean decls (1)
  - norm_bpSeries_term_le

No prerequisites (7)

Lemma Complex.norm_natCast_cpow_sub_add_one_cpow_le(Lemma)
Associated lean decls (1)
- Complex.norm_natCast_cpow_sub_add_one_cpow_le
Definition raceKernel(Definition)
Associated lean decls (1)
- A362583.raceKernel
Lemma hasSum_neg_log_one_sub(Lemma)
Associated lean decls (1)
- A362583.hasSum_neg_log_one_sub
Definition layerB(Definition)
Associated lean decls (1)
- A362583.layerB
Lemma exists_one_lt_tsum_primes_rpow_gt(Lemma)
Associated lean decls (1)
- A362583.exists_one_lt_tsum_primes_rpow_gt
Definition oddPrime(Definition)
Associated lean decls (1)
- A362583.oddPrime
Definition bpSeries(Definition)
Associated lean decls (1)
- bpSeries

No dependents (1)

Theorem irrational_ϱ(Theorem)
Associated lean decls (1)
- A362583.irrational_ϱ