Commit 2021-06-24 09:57 5bd649fb

View on Github →

feat(analysis/liouville/liouville_constant): transcendental Liouville numbers exist! (#8020) The final (hopefully!) PR in the Liouville series: there are a couple of results and the proof that Liouville numbers are transcendental.

Estimated changes

Modified src/analysis/liouville/liouville_constant.lean

modified theorem liouville.aux_calc

added theorem liouville.is_liouville

added theorem liouville.is_transcendental

modified theorem liouville.liouville_number_eq_initial_terms_add_tail

added theorem liouville.liouville_number_rat_initial_terms

modified theorem liouville.liouville_number_tail_pos

modified theorem liouville.tsum_one_div_pow_factorial_lt