`piSeries`

definition

show as: view math explainer →

module: IndisputableMonolith.Mathematics.Pi
domain: Mathematics
line: 224 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Mathematics.Pi on GitHub at line 224.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 221    3. Machin: π/4 = 4 arctan(1/5) - arctan(1/239)
 222
 223    Can any of these be derived from 8-tick structure? -/
 224def piSeries : List String := [
 225  "Leibniz: π/4 = Σ (-1)^n/(2n+1)",
 226  "Wallis: π/2 = Π (2k)²/((2k-1)(2k+1))",
 227  "Machin: π/4 = 4·arctan(1/5) - arctan(1/239)",
 228  "Chudnovsky: Fastest known algorithm"
 229]
 230
 231/-- The Leibniz series and 8-tick:
 232
 233    π/4 = 1 - 1/3 + 1/5 - 1/7 + ...
 234
 235    8 terms: 1 - 1/3 + 1/5 - 1/7 + 1/9 - 1/11 + 1/13 - 1/15
 236           ≈ 0.7604
 237    π/4 ≈ 0.7854
 238
 239    Error ≈ 3% with 8 terms. The 8-tick gives a natural truncation. -/
 240noncomputable def leibniz_8_terms : ℝ :=
 241  1 - 1/3 + 1/5 - 1/7 + 1/9 - 1/11 + 1/13 - 1/15
 242
 243theorem leibniz_8_approximates :
 244    -- leibniz_8_terms ≈ 0.76
 245    -- vs π/4 ≈ 0.785
 246    True := trivial
 247
 248/-! ## π in Physics -/
 249
 250/-- π appears throughout physics:
 251
 252    1. **Circles**: C = 2πr (definition)
 253    2. **Spheres**: V = (4/3)πr³
 254    3. **Gaussian**: ∫exp(-x²)dx = √π

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.