ProjectionCost.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Domination of the actual highest projection by the real-vector cost.

theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_sub line 16
Distinct definitions of this name: OAI/Geometry/EinsteinFour/WeylEstimates01.lean:9053 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.HighestHessian.totalPlus_sub@path.
theorem OAI.PositiveEinsteinFour.HighestHessian.projected_plus_pairing line 22
Distinct definitions of this name: OAI/Geometry/EinsteinFour/WeylEstimates01.lean:9059 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.HighestHessian.projected_plus_pairing@path.
theorem OAI.PositiveEinsteinFour.HighestHessian.projection_difference_plus_energy line 35
Distinct definitions of this name: OAI/Geometry/EinsteinFour/WeylEstimates01.lean:9072 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.HighestHessian.projection_difference_plus_energy@path.
theorem OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing_sub_self line 47
theorem OAI.PositiveEinsteinFour.HighestHessian.highestProjection_curvature_le line 60
Source documentation
Positivity of the orthogonal complement is proved from its actual energy, so the highest projected cost is dominated without a type-decomposition premise.
```
theorem highestProjection_curvature_le (t u : Fin 3 → ℝ) (x y : ℝ)
    (ht : ∀ s, -x ≤ t s) (hu : ∀ s, -y ≤ u s)
    (hy : 0 ≤ y) (hxy : x + y ≤ 2) (W : Hessian)
    (hW : (∑ s : Fin 3, hessianNormSq (totalPlus s W)) = 48 * hessianNormSq W) :
    curvaturePairing t u (highestProjection W) (highestProjection W) ≤
      curvaturePairing t u W W := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalPlus, OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing, OAI.PositiveEinsteinFour.HighestHessian.highestProjection

theorem OAI.PositiveEinsteinFour.HighestHessian.highestProjection_weight_cost line 76

Source documentation

The complete real-vector upper bound for the constructed highest projection.

theorem highestProjection_weight_cost (t u : Fin 3 → ℝ)
    (ht : ∑ s, t s = 0) (hu : ∑ s, u s = 0)
    (x y : ℝ) (htx : ∀ s, -x ≤ t s) (huy : ∀ s, -y ≤ u s)
    (hy : 0 ≤ y) (hxy : x + y ≤ 2) (a : Vec) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) :
    curvaturePairing t u (highestProjection (weightTensor a Z))
      (highestProjection (weightTensor a Z)) ≤
        ‖a‖ ^ 2 * ((7 / 12) * (4 + y) * Z.squaredNorm -
          (5 / 4) * ∑ s, t s * (∑ b, ‖Z.matrix s b‖ ^ 2)) := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing, OAI.PositiveEinsteinFour.HighestHessian.highestProjection, OAI.PositiveEinsteinFour.HighestHessian.weightTensor