AveragedVolume.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The volume deficit follows from the averaged Jacobi bound and the polar volume formula. All numerical constants and integration weights are proved.

theorem OAI.PositiveEinsteinFour.Jacobi.averaged_radial_piecewise_bound line 17

Source documentation

Replace the exact determinant coefficient by the explicit integrable piecewise lower bound used in the volume estimate.

theorem averaged_radial_piecewise_bound {D s u : ℝ}
    (hu : 0 ≤ u) (hu1 : u < 1) (hs : 0 ≤ s)
    (hD : D ≤ Real.sin (Real.pi * u) ^ 3 *
      (1 - lossFactor ((Real.pi * u) ^ 2 /
        (Real.pi ^ 2 - (Real.pi * u) ^ 2)) / 6 *
        ((3 / 2) * s) * (1 - ((Real.pi * u) / Real.pi) ^ 2 / 2))) :
    D ≤ Real.sin (Real.pi * u) ^ 3 *
      (1 - radialLower u * s * (1 - u ^ 2 / 2) / 4) := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.lossFactor, OAI.PositiveEinsteinFour.Jacobi.radialLower

theorem OAI.PositiveEinsteinFour.Jacobi.volume_ratio_upper_of_averaged_radial line 46

Source documentation

The upper-volume estimate with the averaged radial determinant bound. The only volume premise is the classical polar integration upper bound; the sharp deficit coefficient is derived here.

theorem volume_ratio_upper_of_averaged_radial {D : ℝ → ℝ} {V s : ℝ}
    (hs : 0 ≤ s)
    (hD0 : IntervalIntegrable D volume 0 (5 / 8))
    (hD1 : IntervalIntegrable D volume (5 / 8) 1)
    (hpolar : V ≤ (3 * Real.pi / 4) *
      ((∫ u in (0 : ℝ)..(5 / 8), D u) + ∫ u in (5 / 8 : ℝ)..1, D u))
    (hD : ∀ u, 0 < u → u < 1 → D u ≤ Real.sin (Real.pi * u) ^ 3 *
      (1 - lossFactor ((Real.pi * u) ^ 2 /
        (Real.pi ^ 2 - (Real.pi * u) ^ 2)) / 6 *
        ((3 / 2) * s) * (1 - ((Real.pi * u) / Real.pi) ^ 2 / 2))) :
    V ≤ 1 - (3 / 40) * s := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.lossFactor