SineEstimates.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The analytic comparison underlying the rational radial integrals. The alternating seventh-degree sine bound is proved by successive derivatives, then compared with the exact rational polynomial used in VolumeConstants.

theorem OAI.PositiveEinsteinFour.VolumeConstants.nonneg_of_derivative line 16
theorem OAI.PositiveEinsteinFour.VolumeConstants.cos_fourth_upper line 31
theorem OAI.PositiveEinsteinFour.VolumeConstants.sin_fifth_upper line 43
theorem OAI.PositiveEinsteinFour.VolumeConstants.cos_sixth_lower line 54
theorem OAI.PositiveEinsteinFour.VolumeConstants.sin_seventh_lower line 68
theorem OAI.PositiveEinsteinFour.VolumeConstants.sineLower_le_sin line 83
Source documentation
The lower polynomial in the paper is below the sine of the true angle.
```
theorem sineLower_le_sin {z : ℝ} (hz : 0 ≤ z) : sineLower z ≤ Real.sin (Real.pi * z) := by
…
```
Mentions: OAI.PositiveEinsteinFour.VolumeConstants.sineLower
theorem OAI.PositiveEinsteinFour.VolumeConstants.sineLower_linear line 101
Source documentation
Positivity of the same lower polynomial on the half interval used in the reflection argument.
```
theorem sineLower_linear {z : ℝ} (hz : 0 ≤ z) (hz2 : z ≤ 1 / 2) :
    (9 / 5) * z ≤ sineLower z := by
…
```
Mentions: OAI.PositiveEinsteinFour.VolumeConstants.sineLower
theorem OAI.PositiveEinsteinFour.VolumeConstants.sineLower_nonneg line 115
theorem OAI.PositiveEinsteinFour.VolumeConstants.reflected_sineLower line 119
Source documentation
Reflection makes the positive polynomial bound available on all of [0,1].
```
theorem reflected_sineLower {u : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1) :
    0 ≤ sineLower (min u (1 - u)) ∧
      sineLower (min u (1 - u)) ≤ Real.sin (Real.pi * u) := by
…
```
Mentions: OAI.PositiveEinsteinFour.VolumeConstants.sineLower