Energy.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Removal of the energy defects

The right side of equation (19) is kept as an actual function of its two energies. Its derivative estimate uses the scalar discriminant; continuity supplies the zero-energy endpoints.

def OAI.PositiveEinsteinFour.Energy.scalarWeight line 21
def OAI.PositiveEinsteinFour.Energy.gradientSum line 23
def OAI.PositiveEinsteinFour.Energy.quarticEnergy line 28
Source documentation
The actual right side of equation (19), with the two fixed radial energies e0, f0 and variable total energies e, f.
```
def quarticEnergy (v b e0 f0 g gb H Hb e f : ℝ) : ℝ :=
…
```

theorem OAI.PositiveEinsteinFour.Energy.homogeneous_derivative_nonpos line 36

Source documentation

The homogeneous form of the strict scalar discriminant estimate.

theorem homogeneous_derivative_nonpos
    {v : ℝ} (hv : 0 < v) (hv2 : v < 2) (r s : ℝ) :
    A0 v * (r + s) ^ 2 + L0 v * r * (r + s) -
      (17 / 10) * ((7 / 5) * r ^ 2 + (1 + 2 * v / (5 * (2 - v))) * s ^ 2) ≤ 0 := by
…

theorem OAI.PositiveEinsteinFour.Energy.hasDerivAt_mul_sqrt line 63

theorem OAI.PositiveEinsteinFour.Energy.quarticEnergy_hasDerivAt_left line 75

Source documentation

The derivative with respect to the first energy, for positive first energy.

theorem quarticEnergy_hasDerivAt_left
    (v b e0 f0 g gb H Hb f : ℝ) {e : ℝ} (he : 0 < e) :
    HasDerivAt (fun x => quarticEnergy v b e0 f0 g gb H Hb x f)
      ((3 / 4) * Real.sqrt (3 / 5) * gradientSum e0 f0 * scalarWeight v b * Real.sqrt e +
        (9 / 64) * (gradientSum e0 f0) ^ 2 * H -
        (17 / 10) * ((e - (3 / 5) * e0) / v + (f - (3 / 5) * f0) / b + (e + f) / v)) e := by
…

Mentions: OAI.PositiveEinsteinFour.Energy.quarticEnergy, OAI.PositiveEinsteinFour.Energy.gradientSum, OAI.PositiveEinsteinFour.Energy.scalarWeight

theorem OAI.PositiveEinsteinFour.Energy.quarticEnergy_left_derivative_nonpos line 100

Source documentation

The actual first-energy derivative in (19) is nonpositive. The elementary bounds on H are exactly the displayed bounds for the defect coefficient.

theorem quarticEnergy_left_derivative_nonpos
    {v b e0 f0 H e f : ℝ}
    (hv : 0 < v) (hb : 0 < b) (hsum : v + b ≤ 2)
    (he0 : 0 ≤ e0) (hf0 : 0 ≤ f0) (he : e0 ≤ e) (hf : f0 ≤ f)
    (hH0 : 0 ≤ H) (hH : H ≤ 15 / 2 + 2 * v / 3) :
    (3 / 4) * Real.sqrt (3 / 5) * gradientSum e0 f0 * scalarWeight v b * Real.sqrt e +
      (9 / 64) * (gradientSum e0 f0) ^ 2 * H -
      (17 / 10) * ((e - (3 / 5) * e0) / v + (f - (3 / 5) * f0) / b + (e + f) / v) ≤ 0 := by
…

Mentions: OAI.PositiveEinsteinFour.Energy.gradientSum, OAI.PositiveEinsteinFour.Energy.scalarWeight

theorem OAI.PositiveEinsteinFour.Energy.quarticEnergy_left_antitone line 172

Source documentation

Monotonicity in the first defect, including a zero radial-energy endpoint.

theorem quarticEnergy_left_antitone
    {v b e0 f0 H e f : ℝ} (g gb Hb : ℝ)
    (hv : 0 < v) (hb : 0 < b) (hsum : v + b ≤ 2)
    (he0 : 0 ≤ e0) (hf0 : 0 ≤ f0) (he : e0 ≤ e) (hf : f0 ≤ f)
    (hH0 : 0 ≤ H) (hH : H ≤ 15 / 2 + 2 * v / 3) :
    quarticEnergy v b e0 f0 g gb H Hb e f ≤
      quarticEnergy v b e0 f0 g gb H Hb e0 f := by
…

Mentions: OAI.PositiveEinsteinFour.Energy.quarticEnergy

theorem OAI.PositiveEinsteinFour.Energy.quarticEnergy_swap line 197
Source documentation
Exchanging the two Weyl blocks preserves the energy expression.
```
theorem quarticEnergy_swap (v b e0 f0 g gb H Hb e f : ℝ) :
    quarticEnergy v b e0 f0 g gb H Hb e f =
      quarticEnergy b v f0 e0 gb g Hb H f e := by
…
```
Mentions: OAI.PositiveEinsteinFour.Energy.quarticEnergy

theorem OAI.PositiveEinsteinFour.Energy.remove_energy_defects line 207

Source documentation

The full removal of both nonnegative energy defects in equation (19). The coefficient bounds are the elementary pointwise bounds displayed before the manuscript's scalar discriminant calculation; all zero-energy cases are included by continuity.

theorem remove_energy_defects
    {v b e0 f0 H Hb e f : ℝ} (g gb : ℝ)
    (hv : 0 < v) (hb : 0 < b) (hsum : v + b ≤ 2)
    (he0 : 0 ≤ e0) (hf0 : 0 ≤ f0) (he : e0 ≤ e) (hf : f0 ≤ f)
    (hH0 : 0 ≤ H) (hH : H ≤ 15 / 2 + 2 * v / 3)
    (hHb0 : 0 ≤ Hb) (hHb : Hb ≤ 15 / 2 + 2 * b / 3) :
    quarticEnergy v b e0 f0 g gb H Hb e f ≤
      quarticEnergy v b e0 f0 g gb H Hb e0 f0 := by
…

Mentions: OAI.PositiveEinsteinFour.Energy.quarticEnergy

def OAI.PositiveEinsteinFour.Energy.defectCoefficient line 224
Source documentation
The defect coefficient H_d in equation (19).
```
def defectCoefficient (v y : ℝ) : ℝ := (7 / 12) * (4 + y) + (5 / 4) * v + 4
```
theorem OAI.PositiveEinsteinFour.Energy.defectCoefficient_bounds line 227
Source documentation
The elementary sectional-domain bounds for the coefficient H_d.
```
theorem defectCoefficient_bounds {v y : ℝ}
    (hv : 0 ≤ v) (hy : 0 ≤ y) (hsum : v + y ≤ 2) :
    0 ≤ defectCoefficient v y ∧ defectCoefficient v y ≤ 15 / 2 + 2 * v / 3 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Energy.defectCoefficient

theorem OAI.PositiveEinsteinFour.Energy.remove_energy_defects_from_spectral_bounds line 235

Source documentation

Removal of defects with the actual curvature coefficient H_d on the sectional-positivity domain.

theorem remove_energy_defects_from_spectral_bounds
    {v b x y e0 f0 e f : ℝ} (g gb : ℝ)
    (hv : 0 < v) (hb : 0 < b) (hvx : v ≤ x) (hby : b ≤ y) (hxy : x + y ≤ 2)
    (he0 : 0 ≤ e0) (hf0 : 0 ≤ f0) (he : e0 ≤ e) (hf : f0 ≤ f) :
    quarticEnergy v b e0 f0 g gb (defectCoefficient v y) (defectCoefficient b x) e f ≤
      quarticEnergy v b e0 f0 g gb (defectCoefficient v y) (defectCoefficient b x) e0 f0 := by
…

Mentions: OAI.PositiveEinsteinFour.Energy.quarticEnergy, OAI.PositiveEinsteinFour.Energy.defectCoefficient