HessianAlgebra.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Finite algebra in the weighted Hessian inequality

These are the energy metric, compressed curvature action, matrix (12), and sharp scalar optimization in (13). The manifold Hessian and its integration by parts are separate from these finite-dimensional identities.

def OAI.PositiveEinsteinFour.HessianAlgebra.energy line 20
Source documentation
The energy metric of the three Bianchi parameters.
```
def energy (p k l : ℝ) : ℝ := (5 / 3) * p ^ 2 + 5 * k ^ 2 + l ^ 2
```
def OAI.PositiveEinsteinFour.HessianAlgebra.curvatureForm line 24
Source documentation
The quadratic form of the compressed matrix-slot action, normalized by |Z|² / 6.
```
def curvatureForm (v σ ρ p k l : ℝ) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.HessianAlgebra.squareCurvatureForm line 29
Source documentation
The analogous form of the trace-free square of the Weyl block.
```
def squareCurvatureForm (v σ ρ p k l : ℝ) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.HessianAlgebra.actionP line 34
Source documentation
First component of H⁻¹ B, for H = diag(5/3,5,1).
```
def actionP (v σ ρ p k : ℝ) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.HessianAlgebra.actionK line 38
Source documentation
Second component of H⁻¹ B.
```
def actionK (v σ ρ p k l : ℝ) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.HessianAlgebra.actionL line 42
Source documentation
Last component of H⁻¹ B.
```
def actionL (v k : ℝ) : ℝ := -v * k
```
theorem OAI.PositiveEinsteinFour.HessianAlgebra.energy_pair_action line 46
Source documentation
The compressed operator is represented by the curvature bilinear form in the energy metric.
```
theorem energy_pair_action (v σ ρ p k l p' k' l' : ℝ) :
    (5 / 3) * actionP v σ ρ p k * p' +
        5 * actionK v σ ρ p k l * k' + actionL v k * l' =
      v * ((4 / 3) * σ * p * p' - 4 * ρ / Real.sqrt 3 * (p * k' + k * p') -
        4 * σ * k * k' - k * l' - l * k') := by
…
```
Mentions: OAI.PositiveEinsteinFour.HessianAlgebra.actionP, OAI.PositiveEinsteinFour.HessianAlgebra.actionK, OAI.PositiveEinsteinFour.HessianAlgebra.actionL
theorem OAI.PositiveEinsteinFour.HessianAlgebra.squared_action_energy line 56
Source documentation
The matrix of the squared operator is B H⁻¹ B, not the ordinary matrix square. This is the displayed formula for E_B before (12).
```
theorem squared_action_energy (v σ ρ p k l : ℝ)
    (hcircle : ρ ^ 2 = 1 - σ ^ 2) :
    energy (actionP v σ ρ p k) (actionK v σ ρ p k l) (actionL v k) =
      v ^ 2 * ((16 / 15) * p ^ 2 + (21 / 5) * k ^ 2 + l ^ 2 / 5 +
        8 * ρ / (5 * Real.sqrt 3) * p * l + (8 / 5) * σ * k * l) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HessianAlgebra.energy, OAI.PositiveEinsteinFour.HessianAlgebra.actionP, OAI.PositiveEinsteinFour.HessianAlgebra.actionK, OAI.PositiveEinsteinFour.HessianAlgebra.actionL
def OAI.PositiveEinsteinFour.HessianAlgebra.hessianForm line 72
Source documentation
The invariant scalar expression obtained after the Hessian integration by parts.
```
def hessianForm (v b σ ρ p k l : ℝ) : ℝ :=
…
```

theorem OAI.PositiveEinsteinFour.HessianAlgebra.hessian_matrix line 79

Source documentation

Exact matrix (12), with all off-diagonal entries counted twice.

theorem hessian_matrix (v b σ ρ p k l : ℝ) (hcircle : ρ ^ 2 = 1 - σ ^ 2) :
    hessianForm v b σ ρ p k l =
      (-70 - 5 * b ^ 2 + 100 * σ * v - 25 * v ^ 2) * p ^ 2 +
      (-210 - 15 * b ^ 2 - 300 * σ * v - 190 * v ^ 2) * k ^ 2 +
      (-42 - 3 * b ^ 2 - 10 * v ^ 2) * l ^ 2 -
      200 * Real.sqrt 3 * ρ * v * p * k -
      70 * ρ * v ^ 2 / Real.sqrt 3 * p * l -
      2 * (75 * v + 35 * σ * v ^ 2) * k * l := by
…

Mentions: OAI.PositiveEinsteinFour.HessianAlgebra.hessianForm

theorem OAI.PositiveEinsteinFour.HessianAlgebra.cubic_energy_optimization line 100
Source documentation
The last scalar maximization in the sharp cubic contraction estimate. Its hypotheses are precisely the energy spent by the distinguished tangent component, e₁ = 5ν²/3 ≤ e.
```
theorem cubic_energy_optimization {ν e : ℝ}
    (_hν : 0 ≤ ν) (he : (5 / 3) * ν ^ 2 ≤ e) :
    ν * (e - ν ^ 2 / 3) ≤
      (4 / 5) * Real.sqrt (3 / 5) * e * Real.sqrt e := by
…
```

theorem OAI.PositiveEinsteinFour.HessianAlgebra.weighted_operator_square line 120

Source documentation

Positive operator square underlying (11), before integration.

theorem weighted_operator_square
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (P : E →ₗ[ℝ] E)
    (hsymm : ∀ x y, inner ℝ (P x) y = inner ℝ (P y) x)
    (hpos : ∀ x, 0 ≤ inner ℝ (P x) x)
    {m : ℝ} (hm : 0 < m) (Y L : E) :
    0 ≤ m / 6 * inner ℝ (P Y) Y + inner ℝ (P Y) L / 6 +
      inner ℝ (P L) L / (24 * m) := by
…

theorem OAI.PositiveEinsteinFour.HessianAlgebra.projection_bracket_bound line 139

Source documentation

The mixed radial/defect cost is controlled by an explicit square. The statement retains the actual tangent inner products.

theorem projection_bracket_bound
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    {v y σ ρ : ℝ} (hv : 0 ≤ v) (hσ : σ ≤ 1) (p k l : E) :
    (7 / 12) * (4 + y) * ((5 / 3) * ‖p‖ ^ 2 + 5 * ‖k‖ ^ 2 + ‖l‖ ^ 2) -
      (5 / 4) * v * ((4 / 3) * σ * ‖p‖ ^ 2 -
        8 * ρ / Real.sqrt 3 * inner ℝ p k - 4 * σ * ‖k‖ ^ 2 - 2 * inner ℝ k l) ≤
    QuarticEnergy.projectionCoefficient v y σ ρ * ((5 / 3) * ‖p‖ ^ 2) +
      Energy.defectCoefficient v y * (5 * ‖k‖ ^ 2 + ‖l‖ ^ 2) := by
…

Mentions: OAI.PositiveEinsteinFour.QuarticEnergy.projectionCoefficient, OAI.PositiveEinsteinFour.Energy.defectCoefficient