HessianAssembly.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Assembly of the actual weighted Hessian square and its Green contributions.

def OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic line 19
Source documentation
Polarization is applied before any symmetry is imposed on the weight tensor.
```
def weightedQuadratic (q : Hessian → ℝ) (m : ℝ) (X L : Hessian) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.HighestHessian.plusDerivativeQuadratic line 22
def OAI.PositiveEinsteinFour.HighestHessian.matrixSlotQuadratic line 25
def OAI.PositiveEinsteinFour.HighestHessian.traceCorrection line 28
theorem OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic_identity line 32
theorem OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic_original line 47
Source documentation
The coefficients of the four Green calculations are those of the original curvature operator, on the whole inner-Bianchi tensor space.
```
theorem weightedQuadratic_original (t u : Fin 3 → ℝ) (m : ℝ) (X L : Hessian) :
    weightedQuadratic (originalCurvatureForm t u) m X L =
      4 * weightedQuadratic hessianNormSq m X L -
        (5 / 6 : ℝ) * weightedQuadratic (plusDerivativeQuadratic t) m X L -
        (5 / 3 : ℝ) * weightedQuadratic (matrixSlotQuadratic t) m X L -
        weightedQuadratic (minusDerivativeCurvatureForm u) m X L := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic, OAI.PositiveEinsteinFour.HighestHessian.originalCurvatureForm, OAI.PositiveEinsteinFour.HighestHessian.plusDerivativeQuadratic, OAI.PositiveEinsteinFour.HighestHessian.matrixSlotQuadratic, OAI.PositiveEinsteinFour.HighestHessian.minusDerivativeCurvatureForm

theorem OAI.PositiveEinsteinFour.HighestHessian.local_weighted_original_square line 59

Source documentation

The local square, rewritten in the original four curvature terms and with the entire prescribed trace subtracted.

theorem local_weighted_original_square (X : Hessian) (M : Mat)
    (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0) (hu : ∑ s, u s = 0)
    (hM : symmetric M) (hMt : traceFree M)
    (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0) (htrace : hessianTrace X = M)
    (hY : condition (X - traceComponent M))
    (a : Vec) (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi)
    (x y m : ℝ) (hm : 0 < m)
    (htx : ∀ s, -x ≤ t s) (huy : ∀ s, -y ≤ u s) (hxy : x + y ≤ 2) :
    0 ≤ 4 * weightedQuadratic hessianNormSq m X (weightTensor a Z) -
        (5 / 6 : ℝ) * weightedQuadratic (plusDerivativeQuadratic t) m X (weightTensor a Z) -
        (5 / 3 : ℝ) * weightedQuadratic (matrixSlotQuadratic t) m X (weightTensor a Z) -
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic, OAI.PositiveEinsteinFour.HighestHessian.weightTensor, OAI.PositiveEinsteinFour.HighestHessian.plusDerivativeQuadratic, OAI.PositiveEinsteinFour.HighestHessian.matrixSlotQuadratic

theorem OAI.PositiveEinsteinFour.HighestHessian.local_squared_weight_original line 102

Source documentation

Substitute the actual real-vector projection cost for the squared weight used in the coupling argument.

theorem local_squared_weight_original (S : Shape) (v : ℝ) (hv : 0 ≤ v)
    (X : Hessian) (M : Mat) (u : Fin 3 → ℝ) (hu : ∑ s, u s = 0)
    (hM : symmetric M) (hMt : traceFree M)
    (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0) (htrace : hessianTrace X = M)
    (hY : condition (X - traceComponent M))
    (x y w : ℝ) (hw : w ≠ 0) (hy : 0 ≤ y)
    (htx : ∀ s, -x ≤ v * S.s s) (huy : ∀ s, -y ≤ u s) (hxy : x + y ≤ 2)
    (p q k l : Vec) :
    0 ≤ weightedQuadratic (originalCurvatureForm (fun s => v * S.s s) u)
        (w ^ 2) X (weightTensor ((-(3 / 4 : ℝ) * w) • (p - q)) (parameters S p k l)) +
      traceCorrection (fun s => v * S.s s) u M (w ^ 2)
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.weightedQuadratic, OAI.PositiveEinsteinFour.HighestHessian.originalCurvatureForm, OAI.PositiveEinsteinFour.HighestHessian.weightTensor, OAI.PositiveEinsteinFour.HighestHessian.traceCorrection

def OAI.PositiveEinsteinFour.HighestHessian.collectedHessianForm line 129
Source documentation
The first-derivative form obtained after all four Green calculations.
```
def collectedHessianForm (v b e B C E p2 : ℝ) : ℝ :=
…
```

theorem OAI.PositiveEinsteinFour.HighestHessian.green_contributions_collect line 135

Source documentation

Collect the identity, plus, matrix-slot, minus, and trace contributions. The nonparallel cubic term retains its exact coefficient.

theorem green_contributions_collect (m v b e B C E p2 cubic : ℝ) :
    4 * (m * (-13 * e + 20 * B)) -
        (5 / 6 : ℝ) * (m * (7 * v ^ 2 * e - 4 * B - 4 * C)) -
        (5 / 3 : ℝ) * (m * (-10 * B - 3 * C + 20 * E) + cubic / 12) -
        m * (3 * b ^ 2 * e) +
        m * ((10 + (5 / 2) * v ^ 2) * e - 25 * B + 5 * v ^ 2 * p2) =
      m * collectedHessianForm v b e B C E p2 - (5 / 36 : ℝ) * cubic := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.collectedHessianForm

theorem OAI.PositiveEinsteinFour.HighestHessian.collectedHessianForm_eq_tensor line 145
def OAI.PositiveEinsteinFour.HighestHessian.assemblyIntegral line 162
theorem OAI.PositiveEinsteinFour.HighestHessian.assemblyIntegral_apply line 165
theorem OAI.PositiveEinsteinFour.HighestHessian.integral_green_combination line 171

theorem OAI.PositiveEinsteinFour.HighestHessian.weighted_hessian_inequality_of_green_identities line 183

Source documentation

Assemble the independently derived four Green identities and the full trace identity. This is an integration lemma, not an additional geometric or published-input assumption.

theorem weighted_hessian_inequality_of_green_identities
    (I T F U D cost m v b e B C E p2 cubic : C(Ω, ℝ))
    (hlocal : ∀ x, 0 ≤ 4 * I x - (5 / 6 : ℝ) * T x - (5 / 3 : ℝ) * F x -
      U x + D x + cost x)
    (hI : (∫ x, I x ∂μ) = ∫ x, m x * (-13 * e x + 20 * B x) ∂μ)
    (hT : (∫ x, T x ∂μ) = ∫ x, m x * (7 * v x ^ 2 * e x - 4 * B x - 4 * C x) ∂μ)
    (hF : (∫ x, F x ∂μ) = ∫ x, m x * (-10 * B x - 3 * C x + 20 * E x) + cubic x / 12 ∂μ)
    (hU : (∫ x, U x ∂μ) = ∫ x, m x * (3 * b x ^ 2 * e x) ∂μ)
    (hD : (∫ x, D x ∂μ) = ∫ x, m x * ((10 + (5 / 2 : ℝ) * v x ^ 2) * e x -
      25 * B x + 5 * v x ^ 2 * p2 x) ∂μ) :
    0 ≤ ∫ x, m x * collectedHessianForm (v x) (b x) (e x) (B x) (C x) (E x) (p2 x) -
      (5 / 36 : ℝ) * cubic x + cost x ∂μ := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.collectedHessianForm