ActualGlobalCoercive.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.affineMaximal_global_coercive_identity line 23
theorem OAI.AffineBernstein.tube_paired_determinant line 106

theorem OAI.AffineBernstein.paired_cauchy_coercive line 112

Source comment

A two-dimensional positive-semidefinite quadratic form, stated in terms of the actual squared lengths and cross inner product.

theorem paired_cauchy_coercive {P D I a b c : ℝ}
    (hP : 0 ≤ P) (hD : 0 ≤ D) (hI : I ^ 2 ≤ P * D)
    (ha : 0 ≤ a) (hb : 0 < b) (hdet : c ^ 2 ≤ 4 * a * b) :
    0 ≤ a * P + c * I + b * D := by
…

theorem OAI.AffineBernstein.tube_pointwise_coercivity line 129

Source comment

A fixed explicit lower coercivity constant for the exact source range. In particular it is independent of the number of directions k >= 2.

theorem tube_pointwise_coercivity {n k P D I E : ℝ}
    (hn : 3 ≤ n) (hn9 : n ≤ 9) (hk : 2 ≤ k)
    (hP : 0 ≤ P) (hD : 0 ≤ D) (hE : 0 ≤ E) (hI : I ^ 2 ≤ P * D) :
    (1 / 512) * (1 + P + D + E) ≤
      k - 15 / 8 + (n - 7 / 8) * P + ((n + 2) / 2) * I + (15 / 16) * (D + E) := by
…

theorem OAI.AffineBernstein.cauchy_young line 143

Source comment

Cauchy--Schwarz followed by Young, with no choice of orthonormal frame.

theorem cauchy_young {P Q J a ε : ℝ} (hP : 0 ≤ P) (hQ : 0 ≤ Q)
    (hJ : J ^ 2 ≤ P * Q) (hε : 0 < ε) :
    a * J ≤ ε * P + (a ^ 2 / (4 * ε)) * Q := by
…

theorem OAI.AffineBernstein.tube_cutoff_coefficients line 154
Source comment
The exact coefficients on the right of the source coercive identity.
```
theorem tube_cutoff_coefficients {n : ℝ} (hn : 3 ≤ n) :
    (2 - 15 / (2 * n)) ^ 2 + (-15 / (4 * n)) ^ 2 ≤ 8 := by
…
```

theorem OAI.AffineBernstein.tube_cutoff_absorption line 173

Source comment

Quantitative absorption in the exact coercive identity, with constants uniform for every n in [3,9] and every tube direction count.

theorem tube_cutoff_absorption {n v P D E Q Jp Jd : ℝ}
    (hn : 3 ≤ n) (hP : 0 ≤ P) (hD : 0 ≤ D) (hE : 0 ≤ E) (hQ : 0 ≤ Q)
    (hJp : Jp ^ 2 ≤ P * Q) (hJd : Jd ^ 2 ≤ D * Q) :
    v * ((2 - 15 / (2 * n)) * Jp - (15 / (4 * n)) * Jd) ≤
      (1 / 1024) * v ^ 2 * (1 + P + D + E) + 4096 * Q := by
…

theorem OAI.AffineBernstein.tube_coercive_identity_algebra line 195

Source comment

Exact cancellation of the two stationarity identities in tubes.tex. The symbols are their actual integrals; this is just their linear combination.

theorem tube_coercive_identity_algebra {n k V P D E I Rp Rd : ℝ}
    (hn : n ≠ 0)
    (hp : k * V + (n + 1) * P + ((n + 2) / 2) * I = 2 * Rp)
    (hd : (n / 2) * (D + E) + (n + 2) * (P + I) - (n - 2 * k) * V = -2 * Rd) :
    (k - 15 / 8) * V + (n - 7 / 8) * P + ((n + 2) / 2) * I +
      (15 / 16) * (D + E) = (2 - 15 / (2 * n)) * Rp - (15 / (4 * n)) * Rd := by
…