mo271

  "Mathlib.Control.Basic" -> "Mathlib.Tactic.Rewrites";
  "Mathlib.Control.EquivFunctor" -> "Mathlib.Logic.Equiv.Option";
  "Mathlib.Control.ULift" -> "Mathlib.Data.ULift";
  "Mathlib.Data.Bool.Set" -> "Mathlib.Order.CompleteLattice";
  "Mathlib.Data.MLList.Dedup" -> "Mathlib.Tactic.Rewrites";
  "Mathlib.Data.Nat.Set" -> "Mathlib.Order.CompleteLattice";
  "Mathlib.Data.Option.Basic" -> "Mathlib.Logic.Embedding.Basic";
  "Mathlib.Data.Option.Basic" -> "Mathlib.Logic.Equiv.Option";
  "Mathlib.Data.Prod.PProd" -> "Mathlib.Logic.Embedding.Basic";
  "Mathlib.Data.Set.Basic" -> "Mathlib.Data.Set.Intervals.Basic";

mo271

mo271

* {
  margin: 0;
  padding: 0;
  font-family: Calibri, "Trebuchet MS", Helvetica, sans-serif;
  text-decoration: none; }

html {
  min-height: 100%;
  height: 100%; }

mo271

from codetiming import Timer
from decimal import Decimal, getcontext

@Timer()
def BBPzeta2(n: int) -> Decimal:
    s = Decimal(0)
    f = Decimal(1)
    # TODO: figure out exactly how fast this converges, 
    # but I think math.log(10, 64) should be the right factor here
    for k in range(int(n*0.5536546824812272) + 1):

mo271

Images for comment in libjxl/libjxl#1470

mo271

The Basel Problem:

$$\sum_{n=1}^\infty \frac{1}{n^2} = \frac{\pi^2}{6}.$$

Some commutative diagram:

$$\require{AMScd} \begin{CD} K(X) @>{ch}>> H(X;\mathbb Q);\ @VVV @VVV \

mo271

We couldn’t find that file to show.

mo271

mo271

import tactic
import tactic.gptf
import data.nat.prime
import data.nat.parity
import algebra.divisibility
import algebra.big_operators
import data.set.finite
import number_theory.bernoulli
import data.finset
import data.finset.basic

mo271