RadialIntegrals.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The two analytic integral margins in the volume comparison. All numerical bounds here follow from exact polynomial integrals and the proved sine bound; no numerical integration or decimal error premise is used.

def OAI.PositiveEinsteinFour.VolumeConstants.upperKernel line 15
def OAI.PositiveEinsteinFour.VolumeConstants.upperKernelEnd line 18
def OAI.PositiveEinsteinFour.VolumeConstants.lowerKernel line 21
theorem OAI.PositiveEinsteinFour.VolumeConstants.upper_comparison line 24
theorem OAI.PositiveEinsteinFour.VolumeConstants.lower_comparison line 33
theorem OAI.PositiveEinsteinFour.VolumeConstants.sine_reflected_bound line 41
theorem OAI.PositiveEinsteinFour.VolumeConstants.upper_integral_first line 46
theorem OAI.PositiveEinsteinFour.VolumeConstants.upper_integral_middle line 58
theorem OAI.PositiveEinsteinFour.VolumeConstants.upper_integral_end line 69
theorem OAI.PositiveEinsteinFour.VolumeConstants.analytic_upper_margin line 82
Source documentation
The actual upper-volume deficit coefficient exceeds the constant required by the classification argument. The two pieces are precisely the integral of the manuscript's piecewise weight.
```
theorem analytic_upper_margin : (3 / 40 : ℝ) <
    (∫ u in (0 : ℝ)..(5 / 8), upperKernel u) +
      ∫ u in (5 / 8 : ℝ)..1, upperKernelEnd u := by
…
```
Mentions: OAI.PositiveEinsteinFour.VolumeConstants.upperKernel, OAI.PositiveEinsteinFour.VolumeConstants.upperKernelEnd
theorem OAI.PositiveEinsteinFour.VolumeConstants.lower_integral_first line 92
theorem OAI.PositiveEinsteinFour.VolumeConstants.lower_integral_end line 101
theorem OAI.PositiveEinsteinFour.VolumeConstants.analytic_lower_margin line 113
Source documentation
The lower radial integral exceeds 4/3, with its strict margin supplied by the exact rational certificates.
```
theorem analytic_lower_margin : (4 / 3 : ℝ) <
    2 * (Real.pi ^ 2 - 4) / 9 + ∫ u in (0 : ℝ)..1, lowerKernel u := by
…
```
Mentions: OAI.PositiveEinsteinFour.VolumeConstants.lowerKernel