QuarticEnergy.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The full scalar quartic estimate, with both energy and spectral defects.

def OAI.PositiveEinsteinFour.QuarticEnergy.projectionCoefficient line 15
Source documentation
The coefficient g in the weighted Hessian projection bound.
```
def projectionCoefficient (v y σ ρ : ℝ) : ℝ :=
…
```

theorem OAI.PositiveEinsteinFour.QuarticEnergy.projectionCoefficient_le line 19

Source documentation

The normalized spectral parameter controls the actual projection cost.

theorem projectionCoefficient_le
    {v b r σ ρ W : ℝ}
    (hv : 0 ≤ v) (hr : 1 ≤ r) (hr2 : r ≤ 2) (hvr : v * r ≤ 2)
    (hσ : σ = (3 * r - r ^ 3) / 2) (hρ : ρ ^ 2 = 1 - σ ^ 2) :
    projectionCoefficient v (b + W) σ ρ ≤ projectionBound v b (v * r - v) W := by
…

Mentions: OAI.PositiveEinsteinFour.QuarticEnergy.projectionCoefficient

theorem OAI.PositiveEinsteinFour.QuarticEnergy.energy_zero_defect_identity line 30

Source documentation

At zero energy defects the expression in (19) is exactly the scalar form bounded by the homogeneous inequality (20).

theorem energy_zero_defect_identity
    (v b V W H Hb P Q : ℝ) (hP : 0 ≤ P) (hQ : 0 ≤ Q) :
    quarticEnergy v b (P ^ 2) (Q ^ 2)
      (projectionBound v b V W) (projectionBound b v W V) H Hb (P ^ 2) (Q ^ 2) =
    (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) := by
…

theorem OAI.PositiveEinsteinFour.QuarticEnergy.energy_zero_defect_mono_coefficients line 48

Source documentation

Increasing the fixed radial coefficients increases the zero-defect energy expression. The remaining coefficients are irrelevant at zero defect.

theorem energy_zero_defect_mono_coefficients
    (v b H Hb P Q g gb g' gb' : ℝ) (hg : g ≤ g') (hgb : gb ≤ gb') :
    quarticEnergy v b (P ^ 2) (Q ^ 2) g gb H Hb (P ^ 2) (Q ^ 2) ≤
      quarticEnergy v b (P ^ 2) (Q ^ 2) g' gb' H Hb (P ^ 2) (Q ^ 2) := by
…

theorem OAI.PositiveEinsteinFour.QuarticEnergy.quartic_energy_bound line 64

Source documentation

The entire right side of equation (19) is bounded by the negative quartic term, retaining the actual spectral coefficients and arbitrary nonnegative energy defects. The normalized eigenvalue parameters supply the spectral restrictions rather than assuming axial curvature.

theorem quartic_energy_bound
    {v b r s σ τ ρ χ P Q e f : ℝ}
    (hv : 0 < v) (hb : 0 < b)
    (hr : 1 ≤ r) (hr2 : r ≤ 2) (hs : 1 ≤ s) (hs2 : s ≤ 2)
    (hspectral : v * r + b * s ≤ 2)
    (hσ : σ = (3 * r - r ^ 3) / 2) (hρ : ρ ^ 2 = 1 - σ ^ 2)
    (hτ : τ = (3 * s - s ^ 3) / 2) (hχ : χ ^ 2 = 1 - τ ^ 2)
    (hP : 0 ≤ P) (hQ : 0 ≤ Q) (he : P ^ 2 ≤ e) (hf : Q ^ 2 ≤ f) :
    quarticEnergy v b (P ^ 2) (Q ^ 2)
      (projectionCoefficient v (b * s) σ ρ) (projectionCoefficient b (v * r) τ χ)
      (defectCoefficient v (b * s)) (defectCoefficient b (v * r)) e f ≤
    -(2 / 5 - 3 * v * b / 10) * (9 / 25) *
…

Mentions: OAI.PositiveEinsteinFour.QuarticEnergy.projectionCoefficient

theorem OAI.PositiveEinsteinFour.QuarticEnergy.quartic_energy_bound_gradient line 104

Source documentation

The same estimate in the squared gradient variables of the combined integrand: a = |p|² and d = |q|².

theorem quartic_energy_bound_gradient
    {v b r s σ τ ρ χ a d e f : ℝ}
    (hv : 0 < v) (hb : 0 < b)
    (hr : 1 ≤ r) (hr2 : r ≤ 2) (hs : 1 ≤ s) (hs2 : s ≤ 2)
    (hspectral : v * r + b * s ≤ 2)
    (hσ : σ = (3 * r - r ^ 3) / 2) (hρ : ρ ^ 2 = 1 - σ ^ 2)
    (hτ : τ = (3 * s - s ^ 3) / 2) (hχ : χ ^ 2 = 1 - τ ^ 2)
    (ha : 0 ≤ a) (hd : 0 ≤ d) (he : (5 / 3) * a ≤ e) (hf : (5 / 3) * d ≤ f) :
    quarticEnergy v b ((5 / 3) * a) ((5 / 3) * d)
      (projectionCoefficient v (b * s) σ ρ) (projectionCoefficient b (v * r) τ χ)
      (defectCoefficient v (b * s)) (defectCoefficient b (v * r)) e f ≤
      -(2 / 5 - 3 * v * b / 10) * (a + d) * (a / v + d / b) := by
…

Mentions: OAI.PositiveEinsteinFour.QuarticEnergy.projectionCoefficient