CubicWeight.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Normalize the actual cubic trace and its squared-weight contribution.

def OAI.PositiveEinsteinFour.Bianchi.derivativeMatrix line 16
Source documentation
The matrix of derivatives in a fixed tangent direction.
```
def derivativeMatrix (T : Tensor) (d : Fin 4) : Mat :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.derivativeMatrix_symmetric line 19
def OAI.PositiveEinsteinFour.Bianchi.weightedCubicTrace line 25
Source documentation
The trace appearing in the varying matrix-slot coefficient.
```
def weightedCubicTrace (a : Vec) (T : Tensor) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor
theorem OAI.PositiveEinsteinFour.Bianchi.derivative_trace line 29
theorem OAI.PositiveEinsteinFour.Bianchi.weightedCubicTrace_eq line 49
Source documentation
The coordinate contraction and the actual matrix trace have exactly the normalization used in the weighted Green formula.
```
theorem weightedCubicTrace_eq (a : Vec) (T : Tensor) :
    weightedCubicTrace a T = 6 * cubicContraction a T := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.weightedCubicTrace, OAI.PositiveEinsteinFour.Bianchi.cubicContraction
theorem OAI.PositiveEinsteinFour.Bianchi.cubicContraction_smul line 85
theorem OAI.PositiveEinsteinFour.Bianchi.cubicContraction_zero line 91
theorem OAI.PositiveEinsteinFour.Bianchi.cubicContraction_sharp_tensor_diagonal line 96
Source documentation
The sharp diagonal-frame estimate applies to every actual Bianchi tensor, by the proved reconstruction of its three vector coordinates.
```
theorem cubicContraction_sharp_tensor_diagonal (S : Shape) (a : Vec) (T : Tensor)
    (ht : T.traceFree) (hb : T.bianchi) {ν : ℝ}
    (ha : ‖a‖ = 1) (hν : 0 ≤ ν)
    (hdiag : ∀ i j, inner ℝ a (T.matrix i j) = if i = j then ν * S.s i else 0) :
    |cubicContraction a T| ≤
      (4 / 5) * Real.sqrt (3 / 5) * (T.squaredNorm / 6) *
        Real.sqrt (T.squaredNorm / 6) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.cubicContraction

theorem OAI.PositiveEinsteinFour.Bianchi.cubicContraction_sharp_scaled_diagonal line 109

Source documentation

Homogeneity gives the sharp contraction for a non-unit distinguished direction once its normalized diagonal frame has been supplied.

theorem cubicContraction_sharp_scaled_diagonal (S : Shape) (a : Vec) (T : Tensor)
    (ht : T.traceFree) (hb : T.bianchi) (r : ℝ) {ν : ℝ}
    (ha : ‖a‖ = 1) (hν : 0 ≤ ν)
    (hdiag : ∀ i j, inner ℝ a (T.matrix i j) = if i = j then ν * S.s i else 0) :
    |cubicContraction (r • a) T| ≤
      ‖r • a‖ * ((4 / 5) * Real.sqrt (3 / 5) * (T.squaredNorm / 6) *
        Real.sqrt (T.squaredNorm / 6)) := by
…

Mentions: OAI.PositiveEinsteinFour.Bianchi.Shape, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.cubicContraction

theorem OAI.PositiveEinsteinFour.Bianchi.squared_weight_cubic_bound line 123

Source documentation

The coefficient −5/36 in the collected Hessian formula multiplies the full trace, giving exactly the positive cubic term in equation (19). The sharp directional estimate remains an explicit local obligation.

theorem squared_weight_cubic_bound (T : Tensor) (M : ℝ) (hM : 0 ≤ M)
    (p q : Vec)
    (hsharp : |cubicContraction ((-(3 / 4 : ℝ) * M) • (p - q)) T| ≤
      ‖(-(3 / 4 : ℝ) * M) • (p - q)‖ *
        ((4 / 5) * Real.sqrt (3 / 5) * (T.squaredNorm / 6) *
          Real.sqrt (T.squaredNorm / 6))) :
    -(5 / 36 : ℝ) * weightedCubicTrace ((-(3 / 4 : ℝ) * M) • (p - q)) T ≤
      (1 / 2 : ℝ) * Real.sqrt (3 / 5) * (‖p‖ + ‖q‖) * M *
        ((T.squaredNorm / 6) * Real.sqrt (T.squaredNorm / 6)) := by
…

Mentions: OAI.PositiveEinsteinFour.Bianchi.Tensor, OAI.PositiveEinsteinFour.Bianchi.Vec, OAI.PositiveEinsteinFour.Bianchi.cubicContraction, OAI.PositiveEinsteinFour.Bianchi.weightedCubicTrace