VolumeAssembly.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Integration of the radial determinant deficit using the radial comparison and polar volume formula.

theorem OAI.PositiveEinsteinFour.VolumeConstants.integral_sine_cube line 15

theorem OAI.PositiveEinsteinFour.VolumeConstants.radial_deficit_from_average line 37

Source documentation

Averaging the pointwise determinant loss uses only its nonnegative coefficient and the lower bound for the averaged squared curvature.

theorem radial_deficit_from_average {D Q F s u : ℝ}
    (hu : 0 ≤ u) (hu1 : u ≤ 1) (hF : 0 ≤ F)
    (hloss : D ≤ Real.sin (Real.pi * u) ^ 3 * (1 - F * Q / 6))
    (hQ : (3 / 2) * s * (1 - u ^ 2 / 2) ≤ Q) :
    D ≤ Real.sin (Real.pi * u) ^ 3 *
      (1 - F * s * (1 - u ^ 2 / 2) / 4) := by
…

theorem OAI.PositiveEinsteinFour.VolumeConstants.volume_ratio_upper_of_radial_comparison line 51

Source documentation

Integration of the radial comparison and polar volume bound gives equation (7), with coefficient 3/40 from exact rational integration.

theorem volume_ratio_upper_of_radial_comparison {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))
    (hfirst : ∀ u ∈ Set.Icc (0 : ℝ) (5 / 8),
      D u ≤ Real.sin (Real.pi * u) ^ 3 - (4 / (3 * Real.pi)) * s * upperKernel u)
    (hlast : ∀ u ∈ Set.Icc (5 / 8 : ℝ) 1,
      D u ≤ Real.sin (Real.pi * u) ^ 3 - (4 / (3 * Real.pi)) * s * upperKernelEnd u) :
    V ≤ 1 - (3 / 40) * s := by
…

Mentions: OAI.PositiveEinsteinFour.VolumeConstants.upperKernel, OAI.PositiveEinsteinFour.VolumeConstants.upperKernelEnd

theorem OAI.PositiveEinsteinFour.VolumeConstants.volume_ratio_upper_of_radial_comparison_open line 99

Source documentation

Endpoint values have no effect on the volume integral. This form only requires the radial estimate on the open comparison intervals.

theorem volume_ratio_upper_of_radial_comparison_open {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))
    (hfirst : ∀ u ∈ Set.Ioo (0 : ℝ) (5 / 8),
      D u ≤ Real.sin (Real.pi * u) ^ 3 - (4 / (3 * Real.pi)) * s * upperKernel u)
    (hlast : ∀ u ∈ Set.Ioo (5 / 8 : ℝ) 1,
      D u ≤ Real.sin (Real.pi * u) ^ 3 - (4 / (3 * Real.pi)) * s * upperKernelEnd u) :
    V ≤ 1 - (3 / 40) * s := by
…

Mentions: OAI.PositiveEinsteinFour.VolumeConstants.upperKernel, OAI.PositiveEinsteinFour.VolumeConstants.upperKernelEnd