Potential.lean`

43 declarations, 0 contain sorry, 0 declared as axioms

The potential polynomial certificate

The five quotient polynomials and their quarter-interval Bernstein certificates are those of Section 7, Lemma "The polynomial F" of the manuscript. The polynomial identities and inequalities hold over the real numbers.

def OAI.PositiveEinsteinFour.Potential.q0 line 17
def OAI.PositiveEinsteinFour.Potential.q1 line 20
def OAI.PositiveEinsteinFour.Potential.q2 line 23
def OAI.PositiveEinsteinFour.Potential.q3 line 26
def OAI.PositiveEinsteinFour.Potential.q4 line 29
theorem OAI.PositiveEinsteinFour.Potential.q0_quarter0 line 32
theorem OAI.PositiveEinsteinFour.Potential.q0_quarter1 line 49
theorem OAI.PositiveEinsteinFour.Potential.q0_quarter2 line 66
theorem OAI.PositiveEinsteinFour.Potential.q0_quarter3 line 83
theorem OAI.PositiveEinsteinFour.Potential.q0_nonneg line 100
theorem OAI.PositiveEinsteinFour.Potential.q1_quarter0 line 109
theorem OAI.PositiveEinsteinFour.Potential.q1_quarter1 line 128
theorem OAI.PositiveEinsteinFour.Potential.q1_quarter2 line 147
theorem OAI.PositiveEinsteinFour.Potential.q1_quarter3 line 166
theorem OAI.PositiveEinsteinFour.Potential.q1_nonneg line 185
theorem OAI.PositiveEinsteinFour.Potential.q2_quarter0 line 194
theorem OAI.PositiveEinsteinFour.Potential.q2_quarter1 line 214
theorem OAI.PositiveEinsteinFour.Potential.q2_quarter2 line 234
theorem OAI.PositiveEinsteinFour.Potential.q2_quarter3 line 254
theorem OAI.PositiveEinsteinFour.Potential.q2_nonneg line 274
theorem OAI.PositiveEinsteinFour.Potential.q3_quarter0 line 283
theorem OAI.PositiveEinsteinFour.Potential.q3_quarter1 line 303
theorem OAI.PositiveEinsteinFour.Potential.q3_quarter2 line 323
theorem OAI.PositiveEinsteinFour.Potential.q3_quarter3 line 343
theorem OAI.PositiveEinsteinFour.Potential.q3_nonneg line 363
theorem OAI.PositiveEinsteinFour.Potential.q4_quarter0 line 372
theorem OAI.PositiveEinsteinFour.Potential.q4_quarter1 line 392
theorem OAI.PositiveEinsteinFour.Potential.q4_quarter2 line 412
theorem OAI.PositiveEinsteinFour.Potential.q4_quarter3 line 432
theorem OAI.PositiveEinsteinFour.Potential.q4_nonneg line 452
def OAI.PositiveEinsteinFour.Potential.kappa line 462
Source documentation
The multiplier in equation (15), with its exact rational coefficients.
```
def kappa (v b : ℝ) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.Potential.theta line 471
def OAI.PositiveEinsteinFour.Potential.zeroOrder line 477
def OAI.PositiveEinsteinFour.Potential.potential line 484
Source documentation
The actual polynomial F = c E₀ - Θ² from equation (23).
```
def potential (v b : ℝ) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.Potential.f0 line 487
def OAI.PositiveEinsteinFour.Potential.f1 line 491
def OAI.PositiveEinsteinFour.Potential.f2 line 495
def OAI.PositiveEinsteinFour.Potential.f3 line 498
def OAI.PositiveEinsteinFour.Potential.normalForm line 500
theorem OAI.PositiveEinsteinFour.Potential.potential_normalForm line 503
theorem OAI.PositiveEinsteinFour.Potential.normalForm_certificate line 510
Source documentation
Homogeneous Bernstein identity; clearing the denominator avoids any division at the boundary n = 1.
```
theorem normalForm_certificate (n t : ℝ) :
    (1 - n) ^ 8 * normalForm n t =
      n ^ 3 * (1 - n) * q0 n * ((1 - n) ^ 2 - t ^ 2) ^ 4 +
      4 * n * (1 - n) * q1 n * t ^ 2 * ((1 - n) ^ 2 - t ^ 2) ^ 3 +
      6 * (1 - n) * q2 n * t ^ 4 * ((1 - n) ^ 2 - t ^ 2) ^ 2 +
      4 * (1 - n) * q3 n * t ^ 6 * ((1 - n) ^ 2 - t ^ 2) +
      (1 - n) * q4 n * t ^ 8 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Potential.normalForm, OAI.PositiveEinsteinFour.Potential.q0, OAI.PositiveEinsteinFour.Potential.q1, OAI.PositiveEinsteinFour.Potential.q2, OAI.PositiveEinsteinFour.Potential.q3, OAI.PositiveEinsteinFour.Potential.q4
theorem OAI.PositiveEinsteinFour.Potential.normalForm_nonneg line 520
theorem OAI.PositiveEinsteinFour.Potential.potential_nonneg line 540
Source documentation
Lemma 7.4 of the manuscript, including every boundary of its triangle.
```
theorem potential_nonneg {v b : ℝ} (hv : 0 ≤ v) (hb : 0 ≤ b)
    (hsum : v + b ≤ 2) : 0 ≤ potential v b := by
…
```
Mentions: OAI.PositiveEinsteinFour.Potential.potential