module module

`IndisputableMonolith.Numerics.Interval.PiBounds`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Numerics.Interval.Trig module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Numerics.Interval.Basic module_import

declarations in this module (25)

def piInterval L32
theorem pi_in_piInterval L38
def piIntervalWide L55
theorem pi_in_piIntervalWide L61
theorem four_pi_gt L78
theorem four_pi_lt L83
def fourPiInterval L88
theorem four_pi_in_interval L94
theorem pi_sq_gt L107
theorem pi_sq_lt L115
def piSqInterval L123
theorem pi_sq_in_interval L129
theorem pi_pow5_eq L142
theorem pi_pow5_gt L145
theorem pi_pow5_lt L158
def piPow5Interval L170
theorem pi_pow5_in_interval L176
theorem four_pi_gt_d6 L189
theorem four_pi_lt_d6 L194
def fourPiIntervalTight L199
theorem four_pi_in_interval_tight L205
theorem pi_pow5_gt_d6 L216
theorem pi_pow5_lt_d6 L228
def piPow5IntervalTight L239
theorem pi_pow5_in_interval_tight L245