ParameterCost.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual projected weight cost in the three Bianchi parameters.

theorem OAI.PositiveEinsteinFour.HighestHessian.highestProjection_parameter_cost line 17

Source documentation

The scalar coefficients in equation (19) bound the actual highest projection of the unsymmetrized weight derivative tensor.

theorem highestProjection_parameter_cost (S : Shape) (v : ℝ) (hv : 0 ≤ v)
    (u : Fin 3 → ℝ) (hu : ∑ s, u s = 0) (x y : ℝ)
    (htx : ∀ s, -x ≤ v * S.s s) (huy : ∀ s, -y ≤ u s)
    (hy : 0 ≤ y) (hxy : x + y ≤ 2) (a p k l : Vec) :
    curvaturePairing (fun s => v * S.s s) u
        (highestProjection (weightTensor a (parameters S p k l)))
        (highestProjection (weightTensor a (parameters S p k l))) / 6 ≤
      ‖a‖ ^ 2 *
        (QuarticEnergy.projectionCoefficient v y S.sigma S.rho * ((5 / 3) * ‖p‖ ^ 2) +
          Energy.defectCoefficient v y * ((parameters S p k l).squaredNorm / 6 -
            (5 / 3) * ‖p‖ ^ 2)) := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing, OAI.PositiveEinsteinFour.HighestHessian.highestProjection, OAI.PositiveEinsteinFour.HighestHessian.weightTensor, OAI.PositiveEinsteinFour.QuarticEnergy.projectionCoefficient, OAI.PositiveEinsteinFour.Energy.defectCoefficient

theorem OAI.PositiveEinsteinFour.HighestHessian.squared_weight_parameter_cost line 48

Source documentation

For m=M² and dm=-(3/4)M(p-q), the exact weight factor is 9/64. The coefficient keeps its actual sign throughout the division.

theorem squared_weight_parameter_cost (S : Shape) (v : ℝ) (hv : 0 ≤ v)
    (u : Fin 3 → ℝ) (hu : ∑ s, u s = 0) (x y M : ℝ) (hM : M ≠ 0)
    (htx : ∀ s, -x ≤ v * S.s s) (huy : ∀ s, -y ≤ u s)
    (hy : 0 ≤ y) (hxy : x + y ≤ 2) (p q k l : Vec) :
    curvaturePairing (fun s => v * S.s s) u
        (highestProjection (weightTensor ((-(3 / 4 : ℝ) * M) • (p - q)) (parameters S p k l)))
        (highestProjection (weightTensor ((-(3 / 4 : ℝ) * M) • (p - q)) (parameters S p k l))) /
          (24 * M ^ 2) ≤
      (9 / 64 : ℝ) * ‖p - q‖ ^ 2 *
        (QuarticEnergy.projectionCoefficient v y S.sigma S.rho * ((5 / 3) * ‖p‖ ^ 2) +
          Energy.defectCoefficient v y * ((parameters S p k l).squaredNorm / 6 -
            (5 / 3) * ‖p‖ ^ 2)) := by
…