Quartic.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Scalar certificates for the quartic comparison

Exact rational signs for equation (20) and Lemma 7.2 of the manuscript. The Bernstein expansions give exact rational coefficients and their signs.

def OAI.PositiveEinsteinFour.Quartic.A line 17
def OAI.PositiveEinsteinFour.Quartic.G line 20
def OAI.PositiveEinsteinFour.Quartic.H line 23
def OAI.PositiveEinsteinFour.Quartic.L line 26
def OAI.PositiveEinsteinFour.Quartic.Z line 29
def OAI.PositiveEinsteinFour.Quartic.discriminant line 31
theorem OAI.PositiveEinsteinFour.Quartic.coefficients_as_in_manuscript line 34
theorem OAI.PositiveEinsteinFour.Quartic.G_lower line 46
theorem OAI.PositiveEinsteinFour.Quartic.H_lower line 63
theorem OAI.PositiveEinsteinFour.Quartic.Z_nonpos_small line 80
theorem OAI.PositiveEinsteinFour.Quartic.discriminant_nonneg line 101
theorem OAI.PositiveEinsteinFour.Quartic.sqrt_comparison line 130
theorem OAI.PositiveEinsteinFour.Quartic.root_bound line 148
Source documentation
The square-root comparison deduced from the two discriminant certificates.
```
theorem root_bound {u : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1) :
    L u ≤ 2 * Real.sqrt (A u) * (Real.sqrt (G u) + u * Real.sqrt (H u)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Quartic.L, OAI.PositiveEinsteinFour.Quartic.A, OAI.PositiveEinsteinFour.Quartic.G, OAI.PositiveEinsteinFour.Quartic.H
theorem OAI.PositiveEinsteinFour.Quartic.quotient_amgm line 171
theorem OAI.PositiveEinsteinFour.Quartic.relaxed_quartic_nonneg line 185
Source documentation
The relaxed quartic difference after division by v b P⁴ is nonnegative. This is the final arithmetic-geometric-mean step in equation (20).
```
theorem relaxed_quartic_nonneg {u v b : ℝ}
    (hu : 0 ≤ u) (hu1 : u ≤ 1) (hv : 0 < v) (hb : 0 < b) :
    0 ≤ A u / v + A u * u ^ 2 / b + G u * v + H u * b - L u := by
…
```
Mentions: OAI.PositiveEinsteinFour.Quartic.A, OAI.PositiveEinsteinFour.Quartic.G, OAI.PositiveEinsteinFour.Quartic.H, OAI.PositiveEinsteinFour.Quartic.L

theorem OAI.PositiveEinsteinFour.Quartic.enlarged_quartic_bound line 207

Source documentation

Equation (20) after normalizing the larger gradient parameter to one and enlarging the spectral defects to (δ, 0), exactly as in the paper.

theorem enlarged_quartic_bound {u v b : ℝ}
    (hu : 0 ≤ u) (hu1 : u ≤ 1) (hv : 0 < v) (hb : 0 < b) :
    (27 / 128) * v * b * (1 + u) ^ 2 *
        ((19 / 3 - 3 * v - 17 * b / 12) + (7 / 2 - 19 * b / 12) * u ^ 2) +
      (3 / 4) * v * b * (1 + u) *
        ((1 - 3 * (v - b) / 8) + (1 - 3 * (b - v) / 8) * u ^ 3) ≤
      (67 / 50 + 27 * v * b / 100) * (1 + u ^ 2) * (b + v * u ^ 2) := by
…

theorem OAI.PositiveEinsteinFour.Quartic.spectral_polynomial_nonneg line 228
theorem OAI.PositiveEinsteinFour.Quartic.spectral_defect_bound line 242
Source documentation
The spectral-shape term in the quartic projection cost is bounded by twice the minimum-eigenvalue defect. This keeps the cubic invariant of the normalized trace-free block, instead of assuming an axial eigenvalue shape.
```
theorem spectral_defect_bound {v r σ ρ : ℝ}
    (hv : 0 ≤ v) (hr : 1 ≤ r) (hr2 : r ≤ 2) (hvr : v * r ≤ 2)
    (hσ : σ = (3 * r - r ^ 3) / 2) (hρ : ρ ^ 2 = 1 - σ ^ 2) :
    -σ * v + ρ ^ 2 * v ^ 2 / 4 ≤ -v + 2 * (v * r - v) := by
…
```
def OAI.PositiveEinsteinFour.Quartic.projectionBound line 278
Source documentation
The upper bound for the projection coefficient after introducing the nonnegative spectral defects V = x-v and W = y-b.
```
def projectionBound (v b V W : ℝ) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.Quartic.quarticMargin line 282
Source documentation
The difference between the two sides of the paper's equation (20).
```
def quarticMargin (v b V W P Q : ℝ) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.Quartic.projection_enlargement line 289
theorem OAI.PositiveEinsteinFour.Quartic.normalized_margin_nonneg line 300
theorem OAI.PositiveEinsteinFour.Quartic.quarticMargin_swap line 312
theorem OAI.PositiveEinsteinFour.Quartic.ordered_margin_nonneg line 317

theorem OAI.PositiveEinsteinFour.Quartic.quartic_bound line 333

Source documentation

The complete homogeneous inequality (20), including both orderings of the two gradient norms and all allowable spectral defects.

theorem quartic_bound {v b V W P Q : ℝ}
    (hv : 0 < v) (hb : 0 < b) (hV : 0 ≤ V) (hW : 0 ≤ W)
    (hsum : V + W ≤ 2 - v - b) (hP : 0 ≤ P) (hQ : 0 ≤ Q) :
    (27 / 128) * v * b * (P + Q) ^ 2 *
        (projectionBound v b V W * P ^ 2 + projectionBound b v W V * Q ^ 2) +
      (3 / 4) * v * b * (P + Q) *
        ((1 - 3 * (v - b) / 8) * P ^ 3 + (1 - 3 * (b - v) / 8) * Q ^ 3) ≤
      (67 / 50 + 27 * v * b / 100) * (P ^ 2 + Q ^ 2) * (b * P ^ 2 + v * Q ^ 2) := by
…

Mentions: OAI.PositiveEinsteinFour.Quartic.projectionBound

theorem OAI.PositiveEinsteinFour.Quartic.zero_defect_quartic_bound line 365

Source documentation

The quartic estimate after the two nonradial energy defects have been removed. Here P² = 5 |p|² / 3 and Q² = 5 |q|² / 3; the factor 9/25 converts back to the gradient energies in the combined integrand.

theorem zero_defect_quartic_bound {v b V W P Q : ℝ}
    (hv : 0 < v) (hb : 0 < b) (hV : 0 ≤ V) (hW : 0 ≤ W)
    (hsum : V + W ≤ 2 - v - b) (hP : 0 ≤ P) (hQ : 0 ≤ Q) :
    (3 / 10) * (P + Q) *
        ((1 - 3 * (v - b) / 8) * P ^ 3 + (1 - 3 * (b - v) / 8) * Q ^ 3) +
      (27 / 320) * (P + Q) ^ 2 *
        (projectionBound v b V W * P ^ 2 + projectionBound b v W V * Q ^ 2) -
      (2 / 5) * (17 / 10) * (P ^ 2 + Q ^ 2) * (P ^ 2 / v + Q ^ 2 / b) ≤
      -(2 / 5 - 3 * v * b / 10) * (9 / 25) *
        (P ^ 2 + Q ^ 2) * (P ^ 2 / v + Q ^ 2 / b) := by
…

Mentions: OAI.PositiveEinsteinFour.Quartic.projectionBound