Boundary.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Exact triangle certificates and the full zeroth-order coupling bound.

def OAI.PositiveEinsteinFour.Boundary.spectralCoefficient line 14
def OAI.PositiveEinsteinFour.Boundary.correctedPotential line 17
theorem OAI.PositiveEinsteinFour.Boundary.spectral_coefficient_triangle line 20
theorem OAI.PositiveEinsteinFour.Boundary.corrected_potential_left line 59
theorem OAI.PositiveEinsteinFour.Boundary.corrected_potential_right line 120
theorem OAI.PositiveEinsteinFour.Boundary.spectralCoefficient_nonneg line 182
Source documentation
The first boundary certificate in equation (23), including the vertex where its value is zero.
```
theorem spectralCoefficient_nonneg {v b : ℝ}
    (hb : 0 ≤ b) (horder : b ≤ v) (hsum : v + b ≤ 2) :
    0 ≤ spectralCoefficient v b := by
…
```
Mentions: OAI.PositiveEinsteinFour.Boundary.spectralCoefficient
theorem OAI.PositiveEinsteinFour.Boundary.correctedPotential_nonneg line 191
Source documentation
The last boundary certificate in equation (23). The two triangle proofs meet along v = 1, so no strict-domain hypothesis is required.
```
theorem correctedPotential_nonneg {v b : ℝ}
    (hb : 0 ≤ b) (horder : b ≤ v) (hsum : v + b ≤ 2) :
    0 ≤ correctedPotential v b := by
…
```
Mentions: OAI.PositiveEinsteinFour.Boundary.correctedPotential

theorem OAI.PositiveEinsteinFour.Boundary.spectral_potential_defect_bound line 204

Source documentation

The cubic eigenvalue parametrization controls the potential defect using only the minimum-eigenvalue defect and the closed spectral domain.

theorem spectral_potential_defect_bound {v r σ δ : ℝ}
    (hv : 0 ≤ v) (hr : 1 ≤ r) (hr2 : r ≤ 2)
    (hδ : 0 ≤ δ) (hdefect : v * (r - 1) ≤ δ)
    (hσ : σ = (3 * r - r ^ 3) / 2) :
    v ^ 2 * (1 - σ) ≤ 2 * δ ^ 2 := by
…

def OAI.PositiveEinsteinFour.Boundary.zeroOrderIntegrand line 218
Source documentation
The derivative-free part of the manuscript's combined integrand.
```
def zeroOrderIntegrand (v b σ τ : ℝ) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.Boundary.ordered_zeroOrder_bound line 222
theorem OAI.PositiveEinsteinFour.Boundary.zeroOrderIntegrand_swap line 258
theorem OAI.PositiveEinsteinFour.Boundary.theta_swap line 263
theorem OAI.PositiveEinsteinFour.Boundary.zeroOrder_bound line 270
Source documentation
The full potential estimate I₀ ≤ -Θ²/c, on the closed spectral triangle and for either ordering of the blocks. All polynomial certificates required by equation (23) are proved in this development.
```
theorem zeroOrder_bound {v b σ τ : ℝ}
    (hv : 0 ≤ v) (hb : 0 ≤ b) (hsum : v + b ≤ 2)
    (hσ : σ ≤ 1) (hτ : τ ≤ 1)
    (hvdefect : v ^ 2 * (1 - σ) ≤ 2 * (2 - v - b) ^ 2)
    (hbdefect : b ^ 2 * (1 - τ) ≤ 2 * (2 - v - b) ^ 2) :
    zeroOrderIntegrand v b σ τ ≤ -theta v b ^ 2 / couplingCoefficient v b := by
…
```
Mentions: OAI.PositiveEinsteinFour.Boundary.zeroOrderIntegrand, OAI.PositiveEinsteinFour.couplingCoefficient