CurvatureTensors02.lean`

757 declarations, 0 contain sorry, 0 declared as axioms

The actual smooth metric supplies the algebraic curvature identities. No curvature decomposition or sectional criterion is a premise here.

theorem OAI.PositiveEinsteinFour.Geometry.frameCurvature_last_skew line 53
theorem OAI.PositiveEinsteinFour.Geometry.frame_algebraic_lastSkew line 58
theorem OAI.PositiveEinsteinFour.Geometry.actual_einstein_decomposition line 62
theorem OAI.PositiveEinsteinFour.Geometry.actual_weyl_symmetric line 67
theorem OAI.PositiveEinsteinFour.Geometry.actual_weyl_traceFree line 72
theorem OAI.PositiveEinsteinFour.Geometry.actual_sectionalInput line 77
theorem OAI.PositiveEinsteinFour.Geometry.actual_norm_pinching line 82
Source documentation
Strict pointwise pinching of the normalized Weyl norms follows from positive sectional curvature and the actual algebraic curvature identities.
```
theorem actual_norm_pinching (hRic : RicciThree g)
    (hsec : HasPositiveSectionalCurvature g) (e : FrameBundle g) :
    normalizedBlockNorm (plusWeyl g e.base e.frame) +
      normalizedBlockNorm (minusWeyl g e.base e.frame) < 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.minusWeyl
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.relations_of_ricci_zero line 110
theorem OAI.PositiveEinsteinFour.AlgebraicCurvature.ricci_zero_decomposition line 167
theorem OAI.PositiveEinsteinFour.Geometry.curvature_trace_connection line 208
def OAI.PositiveEinsteinFour.Geometry.ricciTensorCoordinates line 240
Source documentation
The Ricci field in one fixed chart, retaining both covariant slots.
```
def ricciTensorCoordinates (g : SmoothMetric M) (c : M) (z : FourSpace) :
    CovariantCoordinates 2 := fun a => ricciInChart g c z (a 0) (a 1)
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_two_apply line 243
theorem OAI.PositiveEinsteinFour.Geometry.ricciInChart_eq_curvatureMatrix_trace line 262
theorem OAI.PositiveEinsteinFour.Geometry.partialDeriv_ricciInChart line 267
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_ricci_eq_curvature_trace line 286
Source documentation
The contracted connection terms cancel in the same fixed chart.
```
theorem covariantDerivative_ricci_eq_curvature_trace (g : SmoothMetric M)
    (c : M) (z : FourSpace) (hz : z ∈ (chartAt FourSpace c).target)
    (hdet : (metricInChart g c z).det ≠ 0) (i j k : Fin 4) :
    covariantDerivative g c (ricciTensorCoordinates g c) z ![i, j, k] =
      ∑ r, coordinateCovariantCurvatureDerivative g c z i r j r k := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.covariantDerivative, OAI.PositiveEinsteinFour.Geometry.ricciTensorCoordinates, OAI.PositiveEinsteinFour.Geometry.coordinateCovariantCurvatureDerivative
theorem OAI.PositiveEinsteinFour.Geometry.lowered_curvature_derivative_contraction line 304
Source documentation
Lowering and contracting the actual curvature derivative gives the actual derivative of Ricci. Invertibility is used only at the evaluation point; no derivative of the inverse metric is required.
```
theorem lowered_curvature_derivative_contraction (g : SmoothMetric M)
    (c : M) (z : FourSpace) (hz : z ∈ (chartAt FourSpace c).target)
    (hdet : (metricInChart g c z).det ≠ 0) (i j k : Fin 4) :
    (∑ r, ∑ s, (metricInChart g c z)⁻¹ r s *
      covariantDerivative g c (curvatureCoordinates g c) z ![i, r, j, k, s]) =
      covariantDerivative g c (ricciTensorCoordinates g c) z ![i, j, k] := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.covariantDerivative, OAI.PositiveEinsteinFour.Geometry.curvatureCoordinates, OAI.PositiveEinsteinFour.Geometry.ricciTensorCoordinates
theorem OAI.PositiveEinsteinFour.Geometry.continuous_tangent_fiber_smul line 338
theorem OAI.PositiveEinsteinFour.Geometry.continuous_frameReflection line 360
def OAI.PositiveEinsteinFour.Geometry.frameReflectionEquiv line 376
theorem OAI.PositiveEinsteinFour.Geometry.tendsto_regularizedHessianWeight_zero line 405
theorem OAI.PositiveEinsteinFour.Geometry.integrable_regularizedHessianWeight_zero line 441
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.hessianIntegrand_integrable line 504
theorem OAI.PositiveEinsteinFour.Geometry.regularized_norm_laplacian_split line 540
theorem OAI.PositiveEinsteinFour.Geometry.weylGradientEnergy_nonneg line 547
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.laplacianNormField line 559
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.regularizedEnergyQuotient_bound line 563
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.integrableEnergyQuotient line 618
theorem OAI.PositiveEinsteinFour.Geometry.smooth_weighted_variance line 678
theorem OAI.PositiveEinsteinFour.Geometry.partial_product line 751
theorem OAI.PositiveEinsteinFour.Geometry.partial_difference line 759
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_unitCurvature line 764
theorem OAI.PositiveEinsteinFour.Geometry.frameJacobiMatrix_apply line 827
theorem OAI.PositiveEinsteinFour.Geometry.frameJacobiMatrix_symmetric line 833
def OAI.PositiveEinsteinFour.Geometry.normalCoordinates line 842
theorem OAI.PositiveEinsteinFour.Geometry.normalCoordinates_ne_zero line 845
theorem OAI.PositiveEinsteinFour.Geometry.normalCoordinates_orthogonal line 852
theorem OAI.PositiveEinsteinFour.Geometry.frameJacobiMatrix_quadratic line 856
theorem OAI.PositiveEinsteinFour.Geometry.actual_jacobi_posSemidef line 877
Source documentation
Positivity of sectional curvatures implies the actual radial matrix is positive semidefinite, including its zero-vector quadratic value.
```
theorem actual_jacobi_posSemidef (hsec : HasPositiveSectionalCurvature g)
    (e : FrameBundle g) : (1 + frameCurvatureField g e).PosSemidef := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameCurvatureField
def OAI.PositiveEinsteinFour.Geometry.tensorConsEquiv line 927
theorem OAI.PositiveEinsteinFour.Geometry.sum_tensor_cons line 936
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_cons line 945
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_zero line 962
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_three line 968
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_four line 983
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_trace_gram line 1000
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.matrix_mul_transpose line 1044
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_trace_inverse line 1059
Source documentation
Contracting in an orthonormal frame equals contraction by the inverse chart metric before framing the uncontracted indices.
```
theorem frameTensor_trace_inverse (e : OrthonormalFrame g c)
    (T : CovariantCoordinates 4) (j k : Fin 4) :
    (∑ i, frameTensor e.matrix T ![i, j, k, i]) =
      ∑ b, ∑ d, e.matrix b j * e.matrix d k *
        (∑ a, ∑ f, (chartMetric g c)⁻¹ a f * T ![a, b, d, f]) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.frameTensor, OAI.PositiveEinsteinFour.Geometry.chartMetric
theorem OAI.PositiveEinsteinFour.Geometry.frame_curvature_derivative_trace line 1067
Source documentation
All three derivative/Ricci slots transform by the same frame.
```
theorem frame_curvature_derivative_trace (e : OrthonormalFrame g c)
    (a j k : Fin 4) :
    (∑ i, frameTensor e.matrix
      (covariantDerivative g c (curvatureCoordinates g c) (chartAt FourSpace c c))
      ![a, i, j, k, i]) =
      frameTensor e.matrix
        (covariantDerivative g c (ricciTensorCoordinates g c) (chartAt FourSpace c c))
        ![a, j, k] := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.frameTensor, OAI.PositiveEinsteinFour.Geometry.covariantDerivative, OAI.PositiveEinsteinFour.Geometry.curvatureCoordinates, OAI.PositiveEinsteinFour.Geometry.ricciTensorCoordinates
theorem OAI.PositiveEinsteinFour.Geometry.frame_curvature_derivative_trace_zero line 1104
def OAI.PositiveEinsteinFour.Geometry.scalarNormExpression line 1130
theorem OAI.PositiveEinsteinFour.Geometry.abs_scalarNormExpression_le line 1134
theorem OAI.PositiveEinsteinFour.Geometry.tendsto_scalarNormExpression line 1164
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.integral_scalarNormExpression_tendsto line 1192
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.scalarNormEquation line 1229
def OAI.PositiveEinsteinFour.Geometry.scalarVarianceWeight line 1274
theorem OAI.PositiveEinsteinFour.Geometry.PetersenOrientedNormInput.plus_regularized_vector line 1278
theorem OAI.PositiveEinsteinFour.Geometry.PetersenOrientedNormInput.minus_regularized_vector line 1293
theorem OAI.PositiveEinsteinFour.Geometry.smooth_weighted_variance_ae line 1311
theorem OAI.PositiveEinsteinFour.Geometry.regularized_difference_variance line 1335
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_const_smul line 1400
theorem OAI.PositiveEinsteinFour.Geometry.ricci_parallel_of_chart_equation line 1418
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_normalizedWeyl line 1453
theorem OAI.PositiveEinsteinFour.Geometry.normalizedWeylCoordinates_second_bianchi line 1466
theorem OAI.PositiveEinsteinFour.Geometry.frame_normalizedWeyl_second_bianchi line 1475
def OAI.PositiveEinsteinFour.Geometry.normalizedDeterminantShape line 1504
theorem OAI.PositiveEinsteinFour.Geometry.shape_product line 1507
theorem OAI.PositiveEinsteinFour.Geometry.orthogonal_conjugate_det line 1512
theorem OAI.PositiveEinsteinFour.Geometry.determinant_shape line 1518
theorem OAI.PositiveEinsteinFour.Geometry.normalizedDeterminantShape_mul line 1529
theorem OAI.PositiveEinsteinFour.Geometry.normalizedDeterminantShape_le_one line 1537
def OAI.PositiveEinsteinFour.Geometry.plusDeterminantShape line 1555
def OAI.PositiveEinsteinFour.Geometry.minusDeterminantShape line 1558
theorem OAI.PositiveEinsteinFour.Geometry.plusDeterminantShape_mul line 1561
theorem OAI.PositiveEinsteinFour.Geometry.minusDeterminantShape_mul line 1566
theorem OAI.PositiveEinsteinFour.Geometry.plusDeterminantShape_le_one line 1571
theorem OAI.PositiveEinsteinFour.Geometry.minusDeterminantShape_le_one line 1576
theorem OAI.PositiveEinsteinFour.Geometry.ricciInChart_transition line 1601
theorem OAI.PositiveEinsteinFour.Geometry.ricciThree_in_chart line 1619
theorem OAI.PositiveEinsteinFour.Geometry.actual_ricci_parallel line 1640
theorem OAI.PositiveEinsteinFour.Geometry.actual_ricci_parallel_at_center line 1647
theorem OAI.PositiveEinsteinFour.Geometry.actual_ricci_hessian line 1653
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_permute line 1685
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_neg line 1700
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_permute_eq line 1716
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_permute_neg line 1726
theorem OAI.PositiveEinsteinFour.Geometry.sum_tensor_permute line 1737
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_permute line 1744
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_neg line 1756
theorem OAI.PositiveEinsteinFour.Geometry.regularized_plus_variance line 1781
theorem OAI.PositiveEinsteinFour.Geometry.regularized_H_plus_variance line 1806
theorem OAI.PositiveEinsteinFour.Geometry.regularized_minus_variance line 1851
theorem OAI.PositiveEinsteinFour.Geometry.regularized_H_minus_variance line 1876
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.scalarNormField line 1946
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.testedNormEquation_of_limits line 1957
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.testedNormEquation line 2047
theorem OAI.PositiveEinsteinFour.Geometry.traceCube_eq_three_det line 2091
theorem OAI.PositiveEinsteinFour.Geometry.weylLaplacian_pairing line 2099
def OAI.PositiveEinsteinFour.Geometry.covariantSlotAction line 2132
Source documentation
Apply a matrix in one covariant slot.
```
def covariantSlotAction {n : ℕ} (s : Fin n) (A : Mat4)
    (T : CovariantCoordinates n) : CovariantCoordinates n := fun a =>
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates
def OAI.PositiveEinsteinFour.Geometry.tensorSlotAction line 2137
Source documentation
The induced action on all covariant slots.
```
def tensorSlotAction {n : ℕ} (A : Mat4) (T : CovariantCoordinates n) :
    CovariantCoordinates n := fun a => ∑ s, covariantSlotAction s A T a
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.covariantSlotAction
theorem OAI.PositiveEinsteinFour.Geometry.covariantSlotAction_add_matrix line 2140
theorem OAI.PositiveEinsteinFour.Geometry.covariantSlotAction_sub_matrix line 2148
theorem OAI.PositiveEinsteinFour.Geometry.covariantSlotAction_add_tensor line 2156
theorem OAI.PositiveEinsteinFour.Geometry.covariantSlotAction_sub_tensor line 2163
theorem OAI.PositiveEinsteinFour.Geometry.covariantSlotAction_same line 2170
theorem OAI.PositiveEinsteinFour.Geometry.covariantSlotAction_distinct line 2184
theorem OAI.PositiveEinsteinFour.Geometry.covariantSlotAction_commutator line 2199
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_add_matrix line 2210
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_sub_matrix line 2217
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_add_tensor line 2224
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_sub_tensor line 2231
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_compose line 2238
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_commutator line 2250
Source documentation
Covariant tensors form the anti-representation of the matrix slot operation; the opposite sign is the covector curvature sign.
```
theorem tensorSlotAction_commutator {n : ℕ} (A B : Mat4)
    (T : CovariantCoordinates n) :
    tensorSlotAction A (tensorSlotAction B T) -
      tensorSlotAction B (tensorSlotAction A T) =
        tensorSlotAction (B * A - A * B) T := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.tensorSlotAction
def OAI.PositiveEinsteinFour.Geometry.pairSwap line 2288
def OAI.PositiveEinsteinFour.Geometry.curvatureArray line 2294
theorem OAI.PositiveEinsteinFour.Geometry.firstSkew_permute line 2297
theorem OAI.PositiveEinsteinFour.Geometry.lastSkew_permute line 2309
theorem OAI.PositiveEinsteinFour.Geometry.pairSymmetric_permute line 2321
theorem OAI.PositiveEinsteinFour.Geometry.coordinate_curvature_firstSkew line 2333
theorem OAI.PositiveEinsteinFour.Geometry.coordinate_curvature_lastSkew line 2342
theorem OAI.PositiveEinsteinFour.Geometry.coordinate_curvature_firstBianchi line 2349
theorem OAI.PositiveEinsteinFour.Geometry.coordinate_curvature_pairSymmetric line 2361
theorem OAI.PositiveEinsteinFour.Geometry.curvatureDerivative_firstSkew line 2370
theorem OAI.PositiveEinsteinFour.Geometry.curvatureDerivative_lastSkew line 2387
theorem OAI.PositiveEinsteinFour.Geometry.curvatureDerivative_pairSymmetric line 2406
def OAI.PositiveEinsteinFour.Geometry.derivativePairSwap line 2426
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_firstSkew line 2432
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_lastSkew line 2454
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_pairSymmetric line 2476
theorem OAI.PositiveEinsteinFour.Geometry.frame_normalizedWeyl_derivative_symmetries line 2500
Source documentation
Every derivative slice of the actual Weyl tensor retains all three algebraic curvature symmetries in any actual orthonormal frame.
```
theorem frame_normalizedWeyl_derivative_symmetries (g : SmoothMetric M) (c : M)
    (e : OrthonormalFrame g c) (d : Fin 4) :
    let D := curvatureDerivativeArray (frameTensor e.matrix
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeArray, OAI.PositiveEinsteinFour.Geometry.frameTensor
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.energyDerivativeField line 2541
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.energyDerivative line 2545
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.energyLaplacianField line 2559
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.testedEnergyEquation line 2569
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.kappaNormEquation line 2630
def OAI.PositiveEinsteinFour.Geometry.regularizedWeylRoot line 2701
def OAI.PositiveEinsteinFour.Geometry.regularizedWeylRootFirst line 2704
def OAI.PositiveEinsteinFour.Geometry.regularizedWeylRootSecond line 2708
theorem OAI.PositiveEinsteinFour.Geometry.regularizedWeylRoot_eq line 2714
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_regularizedWeylRoot line 2721
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_regularizedWeylRootFirst line 2734
theorem OAI.PositiveEinsteinFour.Geometry.regularized_radial_refined_kato line 2751
theorem OAI.PositiveEinsteinFour.Geometry.regularizedWeylRootSecond_sum line 2761
theorem OAI.PositiveEinsteinFour.Geometry.regularizedWeylRootSecond_trace_lower line 2779
theorem OAI.PositiveEinsteinFour.Geometry.weylLaplacian_trace_lower line 2806

theorem OAI.PositiveEinsteinFour.Geometry.regularizedWeylRootSecond_lower line 2822

Source documentation

The pointwise differential inequality for (normalizedBlockNorm A ^ 2 + ε ^ 2) ^ (1/6).

theorem regularizedWeylRootSecond_lower (ε : ℝ) (hε : 0 < ε)
    (A : Mat) (Z : Fin 4 → Mat) (X : Hessian)
    (hA : symmetric A) (htA : traceFree A)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0)
    (hX : hessianTrace X = weylLaplacian A) :
    2 * normalizedBlockNorm A ^ 2 * (1 - normalizedBlockNorm A) /
        regularizedBlockNorm ε A ^ (5 / 3 : ℝ) ≤
      ∑ i, regularizedWeylRootSecond ε A (Z i) (X i i) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.gradientDivergence, OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm, OAI.PositiveEinsteinFour.Geometry.regularizedBlockNorm, OAI.PositiveEinsteinFour.Geometry.regularizedWeylRootSecond

theorem OAI.PositiveEinsteinFour.Geometry.continuous_regularizedWeylRoot line 2839
theorem OAI.PositiveEinsteinFour.Geometry.continuous_regularizedWeylRootFirst line 2844
theorem OAI.PositiveEinsteinFour.Geometry.continuous_regularizedWeylRootSecond line 2853
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.regularizedWeylRoot_derivative line 2873
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.regularizedWeylRootFirst_derivative line 2883
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.regularizedWeylRoot_lower line 2897
Source documentation
The actual metric flow has the regularized lower Laplacian bound; all algebraic gradient and Weyl-equation hypotheses come from its proved data.
```
theorem regularizedWeylRoot_lower (d : MetricGreenData g μ)
    (ε : ℝ) (hε : 0 < ε) (e : FrameBundle g) :
    2 * normalizedBlockNorm (plusWeyl g e.base e.frame) ^ 2 *
        (1 - normalizedBlockNorm (plusWeyl g e.base e.frame)) /
        regularizedBlockNorm ε (plusWeyl g e.base e.frame) ^ (5 / 3 : ℝ) ≤
      ∑ i, regularizedWeylRootSecond ε (plusWeyl g e.base e.frame)
        (plusWeylGradient g e.base e.frame i) (plusWeylHessian g e.base e.frame i i) :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.regularizedBlockNorm, OAI.PositiveEinsteinFour.Geometry.regularizedWeylRootSecond, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.plusWeylHessian
def OAI.PositiveEinsteinFour.Geometry.tensorPartial line 2927
def OAI.PositiveEinsteinFour.Geometry.tensorCovariantDirection line 2931
theorem OAI.PositiveEinsteinFour.Geometry.tensor_partial_sum line 2935
theorem OAI.PositiveEinsteinFour.Geometry.tensor_partial_mul line 2942
theorem OAI.PositiveEinsteinFour.Geometry.tensorPartial_sub line 2950
theorem OAI.PositiveEinsteinFour.Geometry.tensorPartial_slotAction line 2958
theorem OAI.PositiveEinsteinFour.Geometry.tensorPartial_comm line 2985
theorem OAI.PositiveEinsteinFour.Geometry.slotAction_contDiffAt line 3002
theorem OAI.PositiveEinsteinFour.Geometry.tensorCovariantDirection_commutator line 3013
theorem OAI.PositiveEinsteinFour.Geometry.tensorCovariantDirection_cons line 3048
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_direction line 3062
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_iterated_direction line 3068

theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_commutator line 3087

Source documentation

The actual Ricci commutator. Torsion freedom removes the extra connection term from the derivative slot.

theorem covariantDerivative_commutator {n : ℕ} (g : SmoothMetric M) (c : M)
    (T : FourSpace → CovariantCoordinates n) (z : FourSpace)
    (hz : z ∈ (chartAt FourSpace c).target)
    (hdet : (metricInChart g c z).det ≠ 0)
    (hT : ∀ a, ContDiffAt ℝ ∞ (fun w => T w a) z)
    (i j : Fin 4) (a : Fin n → Fin 4) :
    covariantDerivative g c (covariantDerivative g c T) z (Fin.cons i (Fin.cons j a)) -
      covariantDerivative g c (covariantDerivative g c T) z (Fin.cons j (Fin.cons i a)) =
        -tensorSlotAction (coordinateCurvatureMatrix g c i j z) (T z) a := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.covariantDerivative, OAI.PositiveEinsteinFour.Geometry.tensorSlotAction, OAI.PositiveEinsteinFour.Geometry.coordinateCurvatureMatrix

theorem OAI.PositiveEinsteinFour.Geometry.normalizedWeyl_commutator line 3116

Source documentation

The rank-four instance used by the Weyl Hessian.

theorem normalizedWeyl_commutator (g : SmoothMetric M) (c : M)
    (z : FourSpace) (hz : z ∈ (chartAt FourSpace c).target)
    (hdet : (metricInChart g c z).det ≠ 0) (i j : Fin 4)
    (a : Fin 4 → Fin 4) :
    covariantDerivative g c (covariantDerivative g c (normalizedWeylCoordinates g c)) z
      (Fin.cons i (Fin.cons j a)) -
      covariantDerivative g c (covariantDerivative g c (normalizedWeylCoordinates g c)) z
        (Fin.cons j (Fin.cons i a)) =
      -tensorSlotAction (coordinateCurvatureMatrix g c i j z)
        (normalizedWeylCoordinates g c z) a :=
…

Mentions: OAI.PositiveEinsteinFour.Geometry.covariantDerivative, OAI.PositiveEinsteinFour.Geometry.normalizedWeylCoordinates, OAI.PositiveEinsteinFour.Geometry.tensorSlotAction, OAI.PositiveEinsteinFour.Geometry.coordinateCurvatureMatrix

theorem OAI.PositiveEinsteinFour.Geometry.normalizedWeyl_gradient_commutator line 3130

Source documentation

The rank-five instance used by the outer commutator of the Weyl gradient.

theorem normalizedWeyl_gradient_commutator (g : SmoothMetric M) (c : M)
    (z : FourSpace) (hz : z ∈ (chartAt FourSpace c).target)
    (hdet : (metricInChart g c z).det ≠ 0) (i j : Fin 4)
    (a : Fin 5 → Fin 4) :
    covariantDerivative g c
      (covariantDerivative g c (covariantDerivative g c (normalizedWeylCoordinates g c))) z
        (Fin.cons i (Fin.cons j a)) -
      covariantDerivative g c
        (covariantDerivative g c (covariantDerivative g c (normalizedWeylCoordinates g c))) z
          (Fin.cons j (Fin.cons i a)) =
      -tensorSlotAction (coordinateCurvatureMatrix g c i j z)
        (covariantDerivative g c (normalizedWeylCoordinates g c) z) a :=
…

theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_add line 3167
def OAI.PositiveEinsteinFour.Geometry.curvatureCycle line 3183
def OAI.PositiveEinsteinFour.Geometry.frameCurvatureCycle line 3189
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_firstBianchi line 3195
theorem OAI.PositiveEinsteinFour.Geometry.curvatureDerivative_firstBianchi line 3249
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_firstBianchi line 3260
theorem OAI.PositiveEinsteinFour.Geometry.frame_normalizedWeyl_derivative_firstBianchi line 3298
def OAI.PositiveEinsteinFour.Geometry.curvatureHessianArray line 3329
def OAI.PositiveEinsteinFour.Geometry.hessianPairSwap line 3332
theorem OAI.PositiveEinsteinFour.Geometry.curvatureHessian_firstSkew line 3338
theorem OAI.PositiveEinsteinFour.Geometry.curvatureHessian_lastSkew line 3363
theorem OAI.PositiveEinsteinFour.Geometry.curvatureHessian_pairSymmetric line 3388
theorem OAI.PositiveEinsteinFour.Geometry.covariantHessian_normalizedWeyl line 3412
theorem OAI.PositiveEinsteinFour.Geometry.frameHessian_firstSkew line 3421
theorem OAI.PositiveEinsteinFour.Geometry.frameHessian_lastSkew line 3436
theorem OAI.PositiveEinsteinFour.Geometry.frameHessian_pairSymmetric line 3451
theorem OAI.PositiveEinsteinFour.Geometry.frame_normalizedWeyl_hessian_symmetries line 3466
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_add line 3501
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_const_mul line 3506
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_sum line 3514
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_const_mul line 3520
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_sum line 3530
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_cons line 3541
theorem OAI.PositiveEinsteinFour.Geometry.intertwining_pairing line 3549
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_slotAction_intertwine line 3574
Source documentation
An intertwining frame acts simultaneously on every covariant slot. The proof uses one fresh slot at a time, so no large coordinate sum is expanded.
```
theorem frameTensor_slotAction_intertwine (E A B : Mat4) (h : A * E = E * B)
    {n : ℕ} (T : CovariantCoordinates n) :
    frameTensor E (tensorSlotAction A T) = tensorSlotAction B (frameTensor E T) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.frameTensor, OAI.PositiveEinsteinFour.Geometry.tensorSlotAction
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_slotAction line 3613
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.deficitEnergyEquation line 3640
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.refinedKato line 3741
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.energyQuotient_integrable line 3749
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.weakNormEquation line 3755
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.kappaTest line 3761
theorem OAI.PositiveEinsteinFour.Geometry.prescribed_trace_norm_subtraction line 3792
def OAI.PositiveEinsteinFour.Geometry.traceEnergy line 3804
theorem OAI.PositiveEinsteinFour.Geometry.continuous_traceEnergy line 3806
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.traceEnergy_remainder line 3822
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.traceEnergy_le_hessian line 3834
theorem OAI.PositiveEinsteinFour.Geometry.cubeRoot_regularization_error_le line 3863
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.weylRootField line 3914
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.weylRootFirstField line 3918
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.weylRootSecondField line 3924
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.weylRoot_error_le line 3931
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.weylRoot_energy_eq line 3957
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.weylRoot_energy_le line 3982
Source documentation
The regularized gap energy estimate has a uniform vanishing error, and needs no limiting statement about the singular norm gradient.
```
theorem weylRoot_energy_le (d : MetricGreenData g μ) (ε : ℝ) (hε : 0 < ε) :
    (∫ e, (∑ i, d.weylRootFirstField ε hε i e ^ 2) +
        2 * d.weylRootField ε e ^ 2 ∂μ) ≤
      2 * (∫ e, normalizedBlockNorm (plusWeyl g e.base e.frame) *
        d.weylRootField ε e ^ 2 ∂μ) + 2 * ε ^ (2 / 3 : ℝ) * μ.real univ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm, OAI.PositiveEinsteinFour.Geometry.plusWeyl
def OAI.PositiveEinsteinFour.Geometry.twoFormPairing line 4055
Source documentation
The bilinear two-form contraction defining each Weyl block entry.
```
def twoFormPairing (T : CovariantCoordinates 4) (P Q : Mat4) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.Mat4
theorem OAI.PositiveEinsteinFour.Geometry.sumFive_swap0 line 4058
theorem OAI.PositiveEinsteinFour.Geometry.sumFive_swap1 line 4071
theorem OAI.PositiveEinsteinFour.Geometry.sumFive_swap2 line 4084
theorem OAI.PositiveEinsteinFour.Geometry.sumFive_swap3 line 4097
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_add_tensor line 4110
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_add_left line 4114
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_add_right line 4118
theorem OAI.PositiveEinsteinFour.Geometry.updateFour_0 line 4122
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_slot0 line 4127
theorem OAI.PositiveEinsteinFour.Geometry.updateFour_1 line 4140
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_slot1 line 4145
theorem OAI.PositiveEinsteinFour.Geometry.updateFour_2 line 4158
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_slot2 line 4163
theorem OAI.PositiveEinsteinFour.Geometry.updateFour_3 line 4176
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_slot3 line 4181
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_slotAction line 4195
Source documentation
Contracting all four covariant slots acts on each two-form factor.
```
theorem twoFormPairing_slotAction (A : Mat4) (T : CovariantCoordinates 4)
    (P Q : Mat4) :
    twoFormPairing (tensorSlotAction A T) P Q =
      twoFormPairing T (A * P + P * Aᵀ) Q +
        twoFormPairing T P (Q * Aᵀ + A * Q) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.twoFormPairing, OAI.PositiveEinsteinFour.Geometry.tensorSlotAction
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_skew_slotAction line 4210
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_smul_left line 4222
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_smul_right line 4228
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_zero_left line 4234
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_zero_right line 4237
theorem OAI.PositiveEinsteinFour.Geometry.blockCoordinates_pairing line 4240
theorem OAI.PositiveEinsteinFour.Geometry.plusWeylGradient_bianchi_of_ricci_parallel line 4266
Source documentation
The Ricci-parallel hypothesis concerns the fixed-chart Ricci field throughout the chart.
```
theorem plusWeylGradient_bianchi_of_ricci_parallel (e : OrthonormalFrame g c)
    (hRic : covariantDerivative g c (ricciTensorCoordinates g c)
      (chartAt FourSpace c c) = 0) (r : Fin 3) (i : Fin 4) :
    gradientDivergence (plusWeylGradient g c e) r i = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.covariantDerivative, OAI.PositiveEinsteinFour.Geometry.ricciTensorCoordinates, OAI.PositiveEinsteinFour.Geometry.gradientDivergence, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient
theorem OAI.PositiveEinsteinFour.Geometry.minusWeylGradient_bianchi_of_ricci_parallel line 4284
Source documentation
The Ricci-parallel hypothesis concerns the fixed-chart Ricci field throughout the chart.
```
theorem minusWeylGradient_bianchi_of_ricci_parallel (e : OrthonormalFrame g c)
    (hRic : covariantDerivative g c (ricciTensorCoordinates g c)
      (chartAt FourSpace c c) = 0) (r : Fin 3) (i : Fin 4) :
    (∑ s, ∑ j, Angular.oppositeMatrix s i j * minusWeylGradient g c e j s r) = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.covariantDerivative, OAI.PositiveEinsteinFour.Geometry.ricciTensorCoordinates, OAI.PositiveEinsteinFour.Angular.oppositeMatrix, OAI.PositiveEinsteinFour.Geometry.minusWeylGradient
theorem OAI.PositiveEinsteinFour.Geometry.weylGradient_constraints_of_ricci_parallel line 4302
Source documentation
Both block derivatives are symmetric and trace-free, obtained directly from the five-tensor identities rather than a moving eigenframe.
```
theorem weylGradient_constraints_of_ricci_parallel (e : OrthonormalFrame g c)
    (hRic : covariantDerivative g c (ricciTensorCoordinates g c)
      (chartAt FourSpace c c) = 0) :
    (∀ i, TraceHessian.symmetric (plusWeylGradient g c e i) ∧
      TraceHessian.traceFree (plusWeylGradient g c e i)) ∧
    (∀ i, TraceHessian.symmetric (minusWeylGradient g c e i) ∧
      TraceHessian.traceFree (minusWeylGradient g c e i)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.covariantDerivative, OAI.PositiveEinsteinFour.Geometry.ricciTensorCoordinates, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.Geometry.minusWeylGradient
theorem OAI.PositiveEinsteinFour.Geometry.actual_weylHessian_symmetric line 4350
theorem OAI.PositiveEinsteinFour.Geometry.sum_five line 4382
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_five_apply line 4390
def OAI.PositiveEinsteinFour.Geometry.fiveTensorMatrix line 4422
Source documentation
Put the two contracted curvature slots into the row/column positions.
```
def fiveTensorMatrix (T : FourSpace → CovariantCoordinates 5)
    (a j k : Fin 4) (z : FourSpace) : Mat4 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.Mat4
theorem OAI.PositiveEinsteinFour.Geometry.fiveTensorMatrix_covariantDerivative line 4426
def OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeMatrix line 4450
theorem OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeMatrix_trace_zero line 4454
theorem OAI.PositiveEinsteinFour.Geometry.curvatureHessian_contraction_zero line 4463
theorem OAI.PositiveEinsteinFour.Geometry.regularizedRadialDerivative_smul line 4518
theorem OAI.PositiveEinsteinFour.Geometry.reflectedGradient_radial_sum line 4523
theorem OAI.PositiveEinsteinFour.Geometry.scalarNormExpression_reflected line 4530
structure OAI.PositiveEinsteinFour.Geometry.FrameReflectionData line 4540
Source documentation
The two elementary reflection compatibilities of uniform parallel frame flow. These are classical input, not a curvature estimate.
```
structure FrameReflectionData (d : MetricGreenData g μ) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.integral_reflection line 4550
def OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.reflectTest line 4555
def OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.reflectTestDerivative line 4558
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.reflectTest_derivative line 4564
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.opposite_testedNormEquation line 4581
theorem OAI.PositiveEinsteinFour.Geometry.quaternion_generator_commutator line 4642
theorem OAI.PositiveEinsteinFour.Geometry.blockCoordinates_quaternion_action line 4649
Source documentation
The negative of the actual covector action is the spin-two matrix action.
```
theorem blockCoordinates_quaternion_action (T : CovariantCoordinates 4) (s : Fin 3) :
    blockCoordinates (tensorSlotAction (quaternionMatrix s) T) quaternionMatrix =
      -matrixAction s (blockCoordinates T quaternionMatrix) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.blockCoordinates, OAI.PositiveEinsteinFour.Geometry.tensorSlotAction
theorem OAI.PositiveEinsteinFour.Geometry.blockCoordinates_opposite_action line 4664
Source documentation
The commuting quaternion triple has no action on the positive Weyl block.
```
theorem blockCoordinates_opposite_action (T : CovariantCoordinates 4) (s : Fin 3) :
    blockCoordinates (tensorSlotAction (Angular.oppositeMatrix s) T) quaternionMatrix = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.blockCoordinates, OAI.PositiveEinsteinFour.Geometry.tensorSlotAction, OAI.PositiveEinsteinFour.Angular.oppositeMatrix
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.scalarNorm_integrable line 4697
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.radial_integrable line 4728
theorem OAI.PositiveEinsteinFour.Geometry.integrable_continuous_weight line 4756
theorem OAI.PositiveEinsteinFour.Geometry.shape_fourth_moment line 4779
theorem OAI.PositiveEinsteinFour.Geometry.weylLaplacian_shape line 4790
theorem OAI.PositiveEinsteinFour.Geometry.matrixNormSq_diagonal line 4802
theorem OAI.PositiveEinsteinFour.Geometry.traceEnergy_shape line 4806
theorem OAI.PositiveEinsteinFour.Geometry.weylLaplacian_conjugate line 4823
theorem OAI.PositiveEinsteinFour.Geometry.traceEnergy_conjugate line 4828
theorem OAI.PositiveEinsteinFour.Geometry.traceEnergy_spectral line 4837
theorem OAI.PositiveEinsteinFour.Geometry.trace_mul_weylLaplacian_shape line 4842
theorem OAI.PositiveEinsteinFour.Geometry.radialLaplacian_spectral line 4854
theorem OAI.PositiveEinsteinFour.Geometry.scalarNormExpression_spectral line 4873
theorem OAI.PositiveEinsteinFour.Geometry.actual_weylGradient_constraints line 4904
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylGradient_symmetric line 4911
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylGradient_trace line 4917
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylGradient_bianchi line 4922
theorem OAI.PositiveEinsteinFour.Geometry.actual_minusWeylGradient_bianchi line 4927
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_smul_tensor line 4949
def OAI.PositiveEinsteinFour.Geometry.blockCoordinatesLinear line 4957
Source documentation
The fixed two-form contraction is linear in the four-tensor.
```
def blockCoordinatesLinear (Q : Fin 3 → Mat4) : CovariantCoordinates 4 →ₗ[ℝ] Mat3 where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.Mat3
def OAI.PositiveEinsteinFour.Geometry.curvatureEndomorphism line 4969
Source documentation
Slots are arranged as the endomorphism R(e_i,e_j) on vectors.
```
def curvatureEndomorphism (R : Angular.CurvatureArray) (i j : Fin 4) : Mat4 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.CurvatureArray, OAI.PositiveEinsteinFour.Geometry.Mat4
theorem OAI.PositiveEinsteinFour.Geometry.curvatureEndomorphism_blockTensor line 4972
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_smul_matrix line 4986
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_sum_matrix line 4998
theorem OAI.PositiveEinsteinFour.Geometry.blockCoordinates_blockTensor_plus_action line 5011
theorem OAI.PositiveEinsteinFour.Geometry.blockCoordinates_blockTensor_opposite_action line 5027
theorem OAI.PositiveEinsteinFour.Geometry.blockCoordinates_einstein_curvature_action line 5040
theorem OAI.PositiveEinsteinFour.Geometry.frame_curvature_hessian_trace_zero line 5092
theorem OAI.PositiveEinsteinFour.Geometry.frame_normalizedWeyl_hessian_trace_zero line 5119
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.oppositeEnergyField line 5150
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.oppositeEnergyDerivativeField line 5153
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.oppositeEnergyLaplacianField line 5158
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.totalEnergyField line 5161
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.totalEnergyDerivativeField line 5164
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.oppositeEnergyField_apply line 5167
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.oppositeEnergy_derivative line 5185
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.totalEnergy_derivative line 5190
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.opposite_testedEnergyEquation line 5195
theorem OAI.PositiveEinsteinFour.Geometry.scalarNormExpression_zero line 5242
theorem OAI.PositiveEinsteinFour.Geometry.radialLaplacian_lower line 5250
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.radialEnergyQuotient_integrable line 5272
Source documentation
The singular radial energy is integrable by the proved refined Kato inequality and the actual full-gradient quotient estimate.
```
theorem radialEnergyQuotient_integrable (d : MetricGreenData g μ) :
    Integrable (fun e =>
      ‖blockRadialGradient (plusWeyl g e.base e.frame)
        (plusWeylGradient g e.base e.frame)‖ ^ 2 /
          normalizedBlockNorm (plusWeyl g e.base e.frame)) μ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.blockRadialGradient, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.sqrtNormEnergyGap line 5301
Source documentation
The square-root norm gap on the given frame measure. In particular no reflection invariance of an oriented frame measure is assumed.
```
theorem sqrtNormEnergyGap (d : MetricGreenData g μ) :
    (4 / 9 : ℝ) * (∫ e,
      (‖blockRadialGradient (plusWeyl g e.base e.frame)
        (plusWeylGradient g e.base e.frame)‖ ^ 2 /
          normalizedBlockNorm (plusWeyl g e.base e.frame)) / 4 ∂μ) ≤
      (∫ e, normalizedBlockNorm (plusWeyl g e.base e.frame) ^ 2 ∂μ) -
        ∫ e, normalizedBlockNorm (plusWeyl g e.base e.frame) ∂μ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.blockRadialGradient, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm
def OAI.PositiveEinsteinFour.QuaternionFrame.projectionBracket line 5382
theorem OAI.PositiveEinsteinFour.QuaternionFrame.projectionBracket_nonneg line 5386
theorem OAI.PositiveEinsteinFour.QuaternionFrame.norm_of_weight_square line 5401

theorem OAI.PositiveEinsteinFour.QuaternionFrame.cubic_bound_of_weight_square line 5412

Source documentation

Only the norm of the weight covector matters, so this also applies to the reflected opposite block.

theorem cubic_bound_of_weight_square (M : ℝ) (hM : 0 ≤ M) (a p q : Vec)
    (ha : ‖a‖ ^ 2 = (9 / 16 : ℝ) * M ^ 2 * ‖p - q‖ ^ 2)
    (Z : Angular.Gradient) (hs : ∀ i, symmetric (Z i))
    (ht : ∀ i, traceFree (Z i)) (hb : ∀ r i, gradientDivergence Z r i = 0) :
    -(5 / 36 : ℝ) * weightedCubicField a Z ≤
      (1 / 2 : ℝ) * Real.sqrt (3 / 5) * (‖p‖ + ‖q‖) * M *
        (weylGradientEnergy Z * Real.sqrt (weylGradientEnergy Z)) := by
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.QuaternionFrame.weightedCubicField

theorem OAI.PositiveEinsteinFour.QuaternionFrame.projection_bound_of_weight_square line 5435

Source documentation

The true projected cost, with a norm-specified weight derivative.

theorem projection_bound_of_weight_square (A U : Mat)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (x y : ℝ) (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2)
    (M : ℝ) (hM : M ≠ 0) (a p q : Vec)
    (ha : ‖a‖ ^ 2 = (9 / 16 : ℝ) * M ^ 2 * ‖p - q‖ ^ 2)
    (Z : Angular.Gradient) (hs : ∀ i, symmetric (Z i))
    (ht : ∀ i, traceFree (Z i)) (hb : ∀ r i, gradientDivergence Z r i = 0)
    (S : Shape) (p' k l : Vec)
    (he : (parameters S p' k l).squaredNorm / 6 = weylGradientEnergy Z)
    (hp : ‖p'‖ ^ 2 = ‖p‖ ^ 2)
    (hB : weylMatrixEnergy A Z =
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient

theorem OAI.PositiveEinsteinFour.QuaternionFrame.projection_bound_norm_sum line 5462
theorem OAI.PositiveEinsteinFour.QuaternionFrame.gradientSum_radial line 5474
def OAI.PositiveEinsteinFour.QuaternionFrame.arrayHessianTerm line 5489
Source documentation
The part of one actual normalized Hessian Green integrand containing its invariant quadratic form, distinguished cubic trace and projected cost.
```
def arrayHessianTerm (A U : Mat) (Z : Angular.Gradient) (a : Vec) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.Gradient
def OAI.PositiveEinsteinFour.QuaternionFrame.scalarCouplingTerm line 5499
Source documentation
The tested scalar norm equations, trace subtraction and variance term that are added to the two actual Hessian Green integrands.
```
def scalarCouplingTerm (v b e f B C NA NB TA TB : ℝ) (p q : Vec) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.QuaternionFrame.arrayCoupledIntegrand line 5508
def OAI.PositiveEinsteinFour.Geometry.symmetricFrameMeasure line 5538
theorem OAI.PositiveEinsteinFour.Geometry.reflection_preserves_symmetricFrameMeasure line 5541
instance OAI.PositiveEinsteinFour.Geometry.symmetricFrameMeasure_finite line 5554
def OAI.PositiveEinsteinFour.Geometry.ParallelReflection line 5561
Source documentation
The only reflection input on the oriented measure is the ordinary parallel-transport relation, valid independently of the measure.
```
def ParallelReflection (d : MetricGreenData g μ) : Prop :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.flow_preserves_reflected line 5565
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.symmetricFlow line 5577
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.onSymmetricMeasure line 5584
theorem OAI.PositiveEinsteinFour.Geometry.OppositeWeylData.onSymmetricMeasure line 5600
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.symmetricReflection line 5610
theorem OAI.PositiveEinsteinFour.Geometry.integral_symmetricFrameMeasure line 5616
Source documentation
Transfer a symmetric integral back to the oriented frame measure.
```
theorem integral_symmetricFrameMeasure (f : FrameBundle g → ℝ)
    (hi : Integrable f (symmetricFrameMeasure g μ))
    (hs : ∀ e, f (frameReflection e) = f e) :
    (∫ e, f e ∂symmetricFrameMeasure g μ) = 2 * ∫ e, f e ∂μ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.symmetricFrameMeasure, OAI.PositiveEinsteinFour.Geometry.frameReflection
def OAI.PositiveEinsteinFour.Geometry.secondCurvatureCycle line 5646
theorem OAI.PositiveEinsteinFour.Geometry.covariantHessian_firstBianchi line 5655
theorem OAI.PositiveEinsteinFour.Geometry.curvatureHessian_firstBianchi line 5712
theorem OAI.PositiveEinsteinFour.Geometry.frameHessian_firstBianchi line 5726
theorem OAI.PositiveEinsteinFour.Geometry.frame_normalizedWeyl_hessian_firstBianchi line 5743
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_sub line 5771
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_two_prefix line 5776
def OAI.PositiveEinsteinFour.Geometry.pulledCurvatureEndomorphism line 5790
Source documentation
Pull back the two tangent arguments of the curvature endomorphism.
```
def pulledCurvatureEndomorphism (E : Mat4) (C : Fin 4 → Fin 4 → Mat4)
    (i j : Fin 4) : Mat4 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4

theorem OAI.PositiveEinsteinFour.Geometry.framed_tensor_commutator line 5796

Source documentation

This is purely finite tensor algebra; the actual coordinate curvature commutator supplies hX in the geometric specialization.

theorem framed_tensor_commutator {n : ℕ} (E : Mat4) (hE : IsUnit E.det)
    (C : Fin 4 → Fin 4 → Mat4) (T : CovariantCoordinates n)
    (X : CovariantCoordinates (n + 1 + 1))
    (hX : ∀ p q a, X (Fin.cons p (Fin.cons q a)) -
      X (Fin.cons q (Fin.cons p a)) = -tensorSlotAction (C p q) T a)
    (i j : Fin 4) (a : Fin n → Fin 4) :
    frameTensor E X (Fin.cons i (Fin.cons j a)) -
      frameTensor E X (Fin.cons j (Fin.cons i a)) =
        -tensorSlotAction
          (E⁻¹ * pulledCurvatureEndomorphism E C i j * E) (frameTensor E T) a := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.tensorSlotAction, OAI.PositiveEinsteinFour.Geometry.frameTensor, OAI.PositiveEinsteinFour.Geometry.pulledCurvatureEndomorphism

theorem OAI.PositiveEinsteinFour.Geometry.scalarNormExpression_frameReflection line 5867
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.opposite_scalarNorm_integrable line 5885
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.opposite_radial_integrable line 5891
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.jointNormEnergyEquation line 5903
def OAI.PositiveEinsteinFour.QuaternionFrame.scalarHessianCorrection line 5961
def OAI.PositiveEinsteinFour.QuaternionFrame.quarticNormLoss line 5967
def OAI.PositiveEinsteinFour.QuaternionFrame.radialQuadraticTerm line 5970
theorem OAI.PositiveEinsteinFour.QuaternionFrame.scalar_potential_identity line 5975
theorem OAI.PositiveEinsteinFour.QuaternionFrame.scalarCouplingTerm_spectral_split line 5986
theorem OAI.PositiveEinsteinFour.QuaternionFrame.axial_plus_radial_identity line 6000

theorem OAI.PositiveEinsteinFour.QuaternionFrame.invariant_axial_bound line 6015

Source documentation

The actual invariant Hessian expression and the scalar correction are bounded together, so the axial reduction uses the same spectral data.

theorem invariant_axial_bound (A U : Mat) (Z : Angular.Gradient)
    (S : Shape) (τ : ℝ) (p' k l p : Vec)
    (hv : 0 < normalizedBlockNorm A)
    (hsum : normalizedBlockNorm A + normalizedBlockNorm U ≤ 2) (hτ : τ ≤ 1)
    (he : (parameters S p' k l).squaredNorm / 6 = weylGradientEnergy Z)
    (hp : ‖p'‖ ^ 2 = ‖p‖ ^ 2)
    (hB : weylMatrixEnergy A Z =
      curvatureContraction S (normalizedBlockNorm A) (parameters S p' k l))
    (hH : invariantHessianForm A U Z ≤
      hessianTensorForm S (normalizedBlockNorm A) (normalizedBlockNorm U) p' k l) :
    weight (normalizedBlockNorm A) (normalizedBlockNorm U) * invariantHessianForm A U Z +
      scalarHessianCorrection (normalizedBlockNorm A) (normalizedBlockNorm U)
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.QuaternionFrame.scalarHessianCorrection

theorem OAI.PositiveEinsteinFour.QuaternionFrame.scalarWeight_positive line 6039

theorem OAI.PositiveEinsteinFour.QuaternionFrame.quartic_bounds_identity line 6046

Source documentation

The two cubic and projection upper bounds have exactly the quartic energy form used by the scalar relaxation.

theorem quartic_bounds_identity (v b r s σ τ ρ χ e f : ℝ) (p q : Vec) :
    (1 / 2 : ℝ) * Real.sqrt (3 / 5) * (‖p‖ + ‖q‖) * scalarWeight v b *
        (e * Real.sqrt e) +
      (1 / 2 : ℝ) * Real.sqrt (3 / 5) * (‖p‖ + ‖q‖) * scalarWeight b v *
        (f * Real.sqrt f) +
      (9 / 64 : ℝ) * (‖p‖ + ‖q‖) ^ 2 * projectionBracket v (b * s) σ ρ e (‖p‖ ^ 2) +
      (9 / 64 : ℝ) * (‖p‖ + ‖q‖) ^ 2 * projectionBracket b (v * r) τ χ f (‖q‖ ^ 2) +
      quarticNormLoss v b e f p q =
    quarticEnergy v b ((5 / 3) * ‖p‖ ^ 2) ((5 / 3) * ‖q‖ ^ 2)
      (projectionCoefficient v (b * s) σ ρ) (projectionCoefficient b (v * r) τ χ)
      (defectCoefficient v (b * s)) (defectCoefficient b (v * r)) e f := by
…

Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.projectionBracket, OAI.PositiveEinsteinFour.QuaternionFrame.quarticNormLoss

theorem OAI.PositiveEinsteinFour.Geometry.actual_weylHessian_traceFree line 6082
theorem OAI.PositiveEinsteinFour.Geometry.actual_weylHessian_constraints line 6096
theorem OAI.PositiveEinsteinFour.Geometry.sumThree_cycle line 6121
theorem OAI.PositiveEinsteinFour.Geometry.sumFour_pairSwap line 6130
theorem OAI.PositiveEinsteinFour.Geometry.sumFour_BCAD line 6136
theorem OAI.PositiveEinsteinFour.Geometry.sumFour_BDAC line 6143
theorem OAI.PositiveEinsteinFour.Geometry.metric_pairing_apply line 6150
theorem OAI.PositiveEinsteinFour.Geometry.unit_product_first line 6155
theorem OAI.PositiveEinsteinFour.Geometry.unit_product_second line 6164
def OAI.PositiveEinsteinFour.Geometry.unitFrameTensor line 6174
Source documentation
The constant-curvature tensor in an orthonormal frame.
```
def unitFrameTensor : CovariantCoordinates 4 := fun a =>
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_unitCurvature line 6181
theorem OAI.PositiveEinsteinFour.Geometry.sumFive_moveLast line 6200
theorem OAI.PositiveEinsteinFour.Geometry.sumFour_moveLast line 6216
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_curvatureCoordinates line 6225
theorem OAI.PositiveEinsteinFour.Geometry.unitFrameTensor_pairing line 6247
theorem OAI.PositiveEinsteinFour.Geometry.blockCoordinates_unitFrameTensor line 6270
theorem OAI.PositiveEinsteinFour.Geometry.frameWeyl_blockCoordinates line 6279
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.inverse_eq_transpose_metric line 6304
theorem OAI.PositiveEinsteinFour.Geometry.sumFive_moveFirst line 6311
theorem OAI.PositiveEinsteinFour.Geometry.frame_curvatureEndomorphism line 6318
Source documentation
The matrix in the framed covector action is exactly the metric's curvature endomorphism evaluated on that orthonormal frame.
```
theorem frame_curvatureEndomorphism (e : OrthonormalFrame g c) (i j : Fin 4) :
    e.matrix⁻¹ * pulledCurvatureEndomorphism e.matrix
      (fun p q => coordinateCurvatureMatrix g c p q (chartAt FourSpace c c)) i j * e.matrix =
        curvatureEndomorphism (frameCurvature g c e) i j := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.pulledCurvatureEndomorphism, OAI.PositiveEinsteinFour.Geometry.coordinateCurvatureMatrix, OAI.PositiveEinsteinFour.Geometry.curvatureEndomorphism, OAI.PositiveEinsteinFour.Geometry.frameCurvature
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylHessian_commutator line 6336
Source documentation
The last pointwise commutator input of the Weyl equation is a consequence of the actual Levi-Civita commutator and Einstein curvature decomposition.
```
theorem actual_plusWeylHessian_commutator (e : OrthonormalFrame g c)
    (hRic : RicciThree g) (i j : Fin 4) (a b : Fin 3) :
    plusWeylHessian g c e i j a b - plusWeylHessian g c e j i a b =
      bundleCurvatureAction (plusWeyl g c e) i j (plusWeyl g c e) a b := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.plusWeylHessian, OAI.PositiveEinsteinFour.Geometry.plusWeyl
def OAI.PositiveEinsteinFour.Geometry.differentiatedBianchiCycle line 6395
theorem OAI.PositiveEinsteinFour.Geometry.covariantHessian_differentialBianchi line 6404
theorem OAI.PositiveEinsteinFour.Geometry.curvatureHessian_differentialBianchi line 6462
theorem OAI.PositiveEinsteinFour.Geometry.frameHessian_differentialBianchi line 6476
theorem OAI.PositiveEinsteinFour.Geometry.frame_normalizedWeyl_hessian_differentialBianchi line 6495
theorem OAI.PositiveEinsteinFour.Geometry.minusWeylGradient_reflect line 6528
theorem OAI.PositiveEinsteinFour.Geometry.regularizedDeficit_swap line 6537
theorem OAI.PositiveEinsteinFour.Geometry.deficit_frameReflection line 6542
theorem OAI.PositiveEinsteinFour.Geometry.deficitDerivative_frameReflection line 6550
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.deficitEnergy_integrable line 6572
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.opposite_deficitEnergyEquation line 6593
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.jointDeficitEnergyEquation line 6633
theorem OAI.PositiveEinsteinFour.Geometry.integral_reflectedMeasure line 6689
theorem OAI.PositiveEinsteinFour.Geometry.blockNorm_frameReflection line 6693
theorem OAI.PositiveEinsteinFour.Geometry.blockRadialEnergy_frameReflection line 6699
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.reflectedFlow line 6715
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.onReflectedMeasure line 6721
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.oppositeWeakNormEquation line 6739
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.oppositeScalarNorm_integrable line 6746
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.oppositeRadialEnergyQuotient_integrable line 6756
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.oppositeSqrtNormEnergyGap line 6770
structure OAI.PositiveEinsteinFour.QuaternionFrame.PointwiseSpectrum line 6803

theorem OAI.PositiveEinsteinFour.QuaternionFrame.pointwiseSpectrum_nonempty line 6828

Source documentation

All fields, including the Hessian upper bound, come from the proved finite-dimensional identities.

theorem pointwiseSpectrum_nonempty (A U : Mat) (Z : Angular.Gradient) (p : Vec)
    (hA : symmetric A) (htA : traceFree A) (hv : 0 < normalizedBlockNorm A)
    (hs : ∀ i, symmetric (Z i)) (ht : ∀ i, traceFree (Z i))
    (hb : ∀ r i, gradientDivergence Z r i = 0)
    (hp : ‖p‖ ^ 2 = ‖blockRadialGradient A Z‖ ^ 2) :
    Nonempty (PointwiseSpectrum A U Z p) := by
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.QuaternionFrame.PointwiseSpectrum

theorem OAI.PositiveEinsteinFour.QuaternionFrame.PointwiseSpectrum.energy_lower line 6862
theorem OAI.PositiveEinsteinFour.QuaternionFrame.PointwiseSpectrum.shape_sigma_upper line 6868
theorem OAI.PositiveEinsteinFour.QuaternionFrame.PointwiseSpectrum.shape_circle line 6871
theorem OAI.PositiveEinsteinFour.QuaternionFrame.PointwiseSpectrum.minimum_shift line 6875
theorem OAI.PositiveEinsteinFour.QuaternionFrame.PointwiseSpectrum.minimum_le_shift line 6880
theorem OAI.PositiveEinsteinFour.QuaternionFrame.PointwiseSpectrum.scalar_norm line 6886
theorem OAI.PositiveEinsteinFour.QuaternionFrame.PointwiseSpectrum.trace_energy line 6893

def OAI.PositiveEinsteinFour.Geometry.frameVariation line 6919

Source documentation

First variation in the frame matrix, adding one covariant slot at a time.

def frameVariation : {n : ℕ} → Mat4 → Mat4 → CovariantCoordinates n →
    CovariantCoordinates n
  | 0, _, _, _ => 0
  | _n + 1, E, P, T => fun a =>
      (∑ b, P b (a 0) * frameTensor E (fun v => T (Fin.cons b v)) (fun k => a k.succ)) +
      ∑ b, E b (a 0) * frameVariation E P (fun v => T (Fin.cons b v)) (fun k => a k.succ)

Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.frameTensor

theorem OAI.PositiveEinsteinFour.Geometry.frameVariation_cons line 6926
theorem OAI.PositiveEinsteinFour.Geometry.connection_pairing line 6932
theorem OAI.PositiveEinsteinFour.Geometry.frameVariation_connection line 6953
Source documentation
The derivative of the frame precisely cancels the difference between the source and target connection coefficients.
```
theorem frameVariation_connection {n : ℕ} (E P U C : Mat4)
    (h : E * C = P + U * E) (T : CovariantCoordinates n) :
    frameVariation E P T + frameTensor E (tensorSlotAction U T) =
      tensorSlotAction C (frameTensor E T) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.frameVariation, OAI.PositiveEinsteinFour.Geometry.frameTensor, OAI.PositiveEinsteinFour.Geometry.tensorSlotAction
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_differentiableAt line 7002
theorem OAI.PositiveEinsteinFour.Geometry.pullback_partial_sum line 7014
theorem OAI.PositiveEinsteinFour.Geometry.pullback_partial_mul line 7021
theorem OAI.PositiveEinsteinFour.Geometry.tensorPartial_frameTensor line 7029
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylHessian_bianchi_components line 7088
theorem OAI.PositiveEinsteinFour.Geometry.actual_minusWeylHessian_bianchi_components line 7102
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylHessian_bianchi line 7116
theorem OAI.PositiveEinsteinFour.Geometry.gradientBlock_negative_slotAction line 7144
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylThird_outerCommutator line 7166
Source documentation
The outer Ricci commutation formula is derived from the actual Levi-Civita action on all five slots, including the gradient covector.
```
theorem actual_plusWeylThird_outerCommutator (e : OrthonormalFrame g c)
    (hRic : RicciThree g) (i k j : Fin 4) :
    plusWeylThirdDerivative g c e i k j - plusWeylThirdDerivative g c e k i j =
      bundleCurvatureAction (plusWeyl g c e) i k (plusWeylGradient g c e j) +
        ∑ a, frameCurvature g c e i k a j • plusWeylGradient g c e a := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.plusWeylThirdDerivative, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.frameCurvature
def OAI.PositiveEinsteinFour.Geometry.normalRestriction line 7236
Source documentation
The normal restriction of a bilinear form written in coordinate components.
```
def normalRestriction (E K : Mat4) : Mat3 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.Mat3
def OAI.PositiveEinsteinFour.Geometry.normalChange line 7240
Source documentation
Restrict a full frame change to the three normal vectors.
```
def normalChange (P : Mat4) : Mat3 := P.submatrix Fin.succ Fin.succ
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.Mat3
theorem OAI.PositiveEinsteinFour.Geometry.normalChange_orthogonal line 7242
theorem OAI.PositiveEinsteinFour.Geometry.normalRestriction_conjugate line 7257
theorem OAI.PositiveEinsteinFour.Geometry.conjugate_frobenius_norm_sq line 7271
def OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.changeMatrix line 7282
Source documentation
Coordinates of the second frame in the first.
```
def OrthonormalFrame.changeMatrix (e f : OrthonormalFrame g c) : Mat4 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.Mat4
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.mul_changeMatrix line 7285
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.changeMatrix_orthogonal line 7290
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.changeMatrix_first line 7300
theorem OAI.PositiveEinsteinFour.Geometry.normalRestriction_same_direction line 7310
theorem OAI.PositiveEinsteinFour.Geometry.normalRestriction_norm_sq_same_direction line 7325
theorem OAI.PositiveEinsteinFour.Geometry.normalRestriction_sub_one_norm_sq_same_direction line 7333
theorem OAI.PositiveEinsteinFour.Geometry.regularizedKappaDerivative_smul line 7365
def OAI.PositiveEinsteinFour.Geometry.kappaNormIntegrand line 7372
theorem OAI.PositiveEinsteinFour.Geometry.kappaNormIntegrand_reflected line 7376
theorem OAI.PositiveEinsteinFour.Geometry.kappaNormIntegrand_frameReflection line 7393
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.opposite_kappaTest line 7413
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.deficitField line 7451
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.jointScalarNorm line 7456
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.jointEnergyLaplacian line 7460
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.jointScalarNorm_integrable line 7472
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.jointEnergyCancellation line 7475
def OAI.PositiveEinsteinFour.Geometry.matrixActionLinear line 7539
def OAI.PositiveEinsteinFour.Geometry.matrixActionCLM line 7555
def OAI.PositiveEinsteinFour.Geometry.matrixEntryLinear line 7558
def OAI.PositiveEinsteinFour.Geometry.matrixEntryCLM line 7563
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_matrixAction line 7566
theorem OAI.PositiveEinsteinFour.Geometry.parallel_hasDerivAt_entry line 7571

theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_bundleCurvatureSelf line 7577

Source documentation

Product differentiation in the matrix bundle, without an eigenframe.

theorem hasDerivAt_bundleCurvatureSelf {T : ℝ → Mat} {Z : Mat} {t : ℝ}
    (hT : HasDerivAt T Z t) (i j : Fin 4) :
    HasDerivAt (fun r => bundleCurvatureAction (T r) i j (T r))
      (bundleCurvatureDerivative Z i j (T t) + bundleCurvatureAction (T t) i j Z) t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.bundleCurvatureDerivative

theorem OAI.PositiveEinsteinFour.Geometry.inner_commutator_of_derivatives line 7600

Source documentation

A pointwise Hessian commutator can be differentiated using only its parallel derivative fields.

theorem inner_commutator_of_derivatives
    (T : ℝ → Mat) (X : ℝ → Hessian) (Z : Mat) (V : Fin 4 → Fin 4 → Mat)
    (t : ℝ) (k j : Fin 4)
    (hcomm : ∀ r, X r k j - X r j k = bundleCurvatureAction (T r) k j (T r))
    (hT : HasDerivAt T Z t)
    (hXkj : HasDerivAt (fun r => X r k j) (V k j) t)
    (hXjk : HasDerivAt (fun r => X r j k) (V j k) t) :
    V k j - V j k =
      bundleCurvatureDerivative Z k j (T t) + bundleCurvatureAction (T t) k j Z := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.bundleCurvatureDerivative

theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylThird_innerCommutator line 7621

Source documentation

The inner commutator in the Green formula is forced by the actual Hessian identity and the existing ordinary parallel-frame derivatives.

theorem actual_plusWeylThird_innerCommutator
    (g : SmoothMetric M) (hRic : RicciThree g) {μ : Measure (FrameBundle g)}
    (φ : Fin 4 → FrameFlow g μ)
    (hT : ∀ i t e, HasDerivAt
      (fun r => plusWeyl g ((φ i).map r e).base ((φ i).map r e).frame)
      (plusWeylGradient g ((φ i).map t e).base ((φ i).map t e).frame i) t)
    (hX : ∀ i k j t e, HasDerivAt
      (fun r => plusWeylHessian g ((φ i).map r e).base ((φ i).map r e).frame k j)
      (plusWeylThirdDerivative g ((φ i).map t e).base ((φ i).map t e).frame i k j) t)
    (e : FrameBundle g) (i k j : Fin 4) :
    plusWeylThirdDerivative g e.base e.frame i k j -
        plusWeylThirdDerivative g e.base e.frame i j k =
…

Mentions: OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.plusWeylHessian, OAI.PositiveEinsteinFour.Geometry.plusWeylThirdDerivative

theorem OAI.PositiveEinsteinFour.QuaternionFrame.zero_gradient_energy line 7674
theorem OAI.PositiveEinsteinFour.QuaternionFrame.zero_gradient_matrix_energy line 7677
theorem OAI.PositiveEinsteinFour.QuaternionFrame.zero_gradient_radial line 7681
theorem OAI.PositiveEinsteinFour.QuaternionFrame.zero_gradient_hessian_nonpos line 7686
theorem OAI.PositiveEinsteinFour.QuaternionFrame.pointwiseSpectrum_zero line 7697
theorem OAI.PositiveEinsteinFour.QuaternionFrame.pointwiseSpectrum_nonempty_closed line 7726
theorem OAI.PositiveEinsteinFour.QuaternionFrame.PointwiseSpectrum.scalar_norm_closed line 7750
theorem OAI.PositiveEinsteinFour.QuaternionFrame.PointwiseSpectrum.axial_closed line 7766
theorem OAI.PositiveEinsteinFour.Geometry.actual_weylCovariantIdentities line 7818
theorem OAI.PositiveEinsteinFour.Geometry.actual_metric_weyl_trace line 7826
theorem OAI.PositiveEinsteinFour.Geometry.directionalCurvature_sumFour_moveLast line 7852
def OAI.PositiveEinsteinFour.Geometry.directionalCurvatureMatrix line 7868
Source documentation
Contract the two Jacobi directions before choosing the normal basis.
```
def directionalCurvatureMatrix (T : CovariantCoordinates 4) (w : Fin 4 → ℝ) : Mat4 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.Mat4
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_normal_matrix line 7871
def OAI.PositiveEinsteinFour.Geometry.directionalDerivativeTensor line 7881
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_directionalDerivative line 7884
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureField_normalRestriction line 7900
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureField_norm_same_direction line 7910
theorem OAI.PositiveEinsteinFour.Geometry.actual_weyl_derivative_decomposition line 7921
Source documentation
Each actual first derivative of the normalized Weyl tensor has only its positive and negative Weyl blocks; its Ricci contraction is zero.
```
theorem actual_weyl_derivative_decomposition (e : OrthonormalFrame g c)
    (hRic : RicciThree g) (d : Fin 4) :
    curvatureDerivativeArray (frameTensor e.matrix
      (covariantDerivative g c (normalizedWeylCoordinates g c) (chartAt FourSpace c c))) d =
      blockTensor (plusWeylGradient g c e d) quaternionMatrix +
        blockTensor (minusWeylGradient g c e d) oppositeMatrix := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeArray, OAI.PositiveEinsteinFour.Geometry.frameTensor, OAI.PositiveEinsteinFour.Geometry.covariantDerivative, OAI.PositiveEinsteinFour.Geometry.normalizedWeylCoordinates, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.minusWeylGradient
theorem OAI.PositiveEinsteinFour.Geometry.blockTensor_add line 7939
theorem OAI.PositiveEinsteinFour.Geometry.normalEvaluation_pureBlocks line 7943
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureDerivative_actual line 7958
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureDerivative_normalRestriction line 7972
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureDerivative_norm_same_direction line 7991
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureField_directionInvariant line 8002
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureDerivative_directionInvariant line 8009
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.jointMatrixEnergy line 8040
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.jointTraceEnergy line 8043
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.jointHessianEnergy line 8049
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.jointTraceEnergy_le_hessian line 8055
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.traceDeficitIntegrand line 8075
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.traceDeficit_integral_nonneg line 8090
theorem OAI.PositiveEinsteinFour.QuaternionFrame.arrayCoupledIntegrand_le_reduced line 8144

theorem OAI.PositiveEinsteinFour.QuaternionFrame.pointwise_coupling_bound line 8258

Source documentation

Positive-norm finite-array coupling estimate. Spectral frames and all three-parameter decompositions are constructed and eliminated internally.

theorem pointwise_coupling_bound
    (A U : Mat) (Z V : Angular.Gradient) (a ab p q : Vec)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (hZs : ∀ i, symmetric (Z i)) (hZt : ∀ i, traceFree (Z i))
    (hZb : ∀ r i, gradientDivergence Z r i = 0)
    (hVs : ∀ i, symmetric (V i)) (hVt : ∀ i, traceFree (V i))
    (hVb : ∀ r i, gradientDivergence V r i = 0)
    (hv : 0 < normalizedBlockNorm A) (hb : 0 < normalizedBlockNorm U)
    (x y : ℝ) (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2)
    (hp : ‖p‖ ^ 2 = ‖blockRadialGradient A Z‖ ^ 2)
    (hq : ‖q‖ ^ 2 = ‖blockRadialGradient U V‖ ^ 2)
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient

theorem OAI.PositiveEinsteinFour.QuaternionFrame.pointwise_coupling_bound_closed line 8300

Source documentation

The same bound includes both zero axes under precisely the gradient-vanishing hypotheses supplied almost everywhere by the flow.

theorem pointwise_coupling_bound_closed
    (A U : Mat) (Z V : Angular.Gradient) (a ab p q : Vec)
    (hA : symmetric A) (hU : symmetric U) (htA : traceFree A) (htU : traceFree U)
    (hZs : ∀ i, symmetric (Z i)) (hZt : ∀ i, traceFree (Z i))
    (hZb : ∀ r i, gradientDivergence Z r i = 0)
    (hVs : ∀ i, symmetric (V i)) (hVt : ∀ i, traceFree (V i))
    (hVb : ∀ r i, gradientDivergence V r i = 0)
    (hzero : normalizedBlockNorm A = 0 → Z = 0)
    (hzerob : normalizedBlockNorm U = 0 → V = 0)
    (x y : ℝ) (hAx : (A + x • (1 : Mat)).PosSemidef)
    (hUy : (U + y • (1 : Mat)).PosSemidef) (hxy : x + y ≤ 2)
    (hp : ‖p‖ ^ 2 = ‖blockRadialGradient A Z‖ ^ 2)
…

Mentions: OAI.PositiveEinsteinFour.Angular.Gradient

theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_mul line 8358
Source documentation
Successive pullbacks act by the product of their frame matrices.
```
theorem frameTensor_mul {n : ℕ} (E P : Mat4) (T : CovariantCoordinates n) :
    frameTensor (E * P) T = frameTensor P (frameTensor E T) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.frameTensor
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_directionFrame_normal line 8385
theorem OAI.PositiveEinsteinFour.Geometry.turn_blockTensor_add line 8412
theorem OAI.PositiveEinsteinFour.Geometry.turn_normalEvaluation_pureBlocks line 8416
theorem OAI.PositiveEinsteinFour.Geometry.normalDeviation_sum_smul line 8431
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureDerivative_turn line 8446
Source documentation
The quaternionic completion rotates the derivative direction and all four curvature slots of the actual tensor at once.
```
theorem frameCurvatureDerivative_turn (e : OrthonormalFrame g c)
    (hRic : RicciThree g) (q : Directions) :
    frameCurvatureDerivative g (frameTurn e q) = normalCurvatureDerivative g c e q := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.frameCurvatureDerivative, OAI.PositiveEinsteinFour.Geometry.frameTurn, OAI.PositiveEinsteinFour.Geometry.normalCurvatureDerivative
theorem OAI.PositiveEinsteinFour.Geometry.continuous_kappaV_fields line 8492
theorem OAI.PositiveEinsteinFour.Geometry.continuous_kappaB_fields line 8498
theorem OAI.PositiveEinsteinFour.Geometry.abs_radialDerivative_zero_le line 8504
theorem OAI.PositiveEinsteinFour.Geometry.integrable_radialDerivative_product line 8524
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.kappaTest_integrable line 8555
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.opposite_kappaTest_integrable line 8592
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.traceDeficit_integrable line 8599
theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotAction_smul_right line 8633
theorem OAI.PositiveEinsteinFour.Geometry.matrixPairing_same_smul line 8637
theorem OAI.PositiveEinsteinFour.Geometry.weylMatrixEnergy_reflected line 8646
theorem OAI.PositiveEinsteinFour.Geometry.hessianNormSq_reflected line 8655
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.jointMatrixEnergy_apply line 8666
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.jointTraceEnergy_apply line 8679
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.jointHessianEnergy_apply line 8685
def OAI.PositiveEinsteinFour.Geometry.frameTensorPairing line 8724
Source documentation
Pairing of all components of a covariant tensor in an orthonormal frame.
```
def frameTensorPairing {n : ℕ} (T U : CovariantCoordinates n) : ℝ := ∑ a, T a * U a
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates
def OAI.PositiveEinsteinFour.Geometry.frameTensorSquareNorm line 8726
def OAI.PositiveEinsteinFour.Geometry.pairingConsEquiv line 8728
theorem OAI.PositiveEinsteinFour.Geometry.sum_tensor_indices_cons line 8737
theorem OAI.PositiveEinsteinFour.Geometry.orthogonal_covector_pairing line 8746
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_pairing_orthogonal line 8767
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_norm_orthogonal line 8796
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_norm_same_base line 8804
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.preVarianceIntegrand line 8834
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.jointHessianGreen line 8852
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.preVarianceIntegrand_integrable line 8867
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.preVarianceGreen line 8876
def OAI.PositiveEinsteinFour.Geometry.weylWeightGradient line 8920
def OAI.PositiveEinsteinFour.Geometry.reflectedVector line 8923
theorem OAI.PositiveEinsteinFour.Geometry.reflectedVector_norm line 8926
theorem OAI.PositiveEinsteinFour.Geometry.blockRadialGradient_reflected line 8932
theorem OAI.PositiveEinsteinFour.Geometry.weylWeightGradient_eq line 8937
theorem OAI.PositiveEinsteinFour.Geometry.weylWeightGradient_reflected line 8946
theorem OAI.PositiveEinsteinFour.Geometry.kappaNormIntegrand_pair line 8958
theorem OAI.PositiveEinsteinFour.Geometry.regularizedHessianIntegrand_eq_arrayHessianTerm line 8976
theorem OAI.PositiveEinsteinFour.Geometry.reflectedHessianIntegrand_eq_arrayHessianTerm line 8987
def OAI.PositiveEinsteinFour.Geometry.blockTensorCoordinates line 9021
theorem OAI.PositiveEinsteinFour.Geometry.frameTensorPairing_add_right line 9024
theorem OAI.PositiveEinsteinFour.Geometry.frameTensorPairing_const_mul_right line 9028
theorem OAI.PositiveEinsteinFour.Geometry.frameTensorPairing_sum_right line 9035
theorem OAI.PositiveEinsteinFour.Geometry.sum_four_coordinates line 9041
theorem OAI.PositiveEinsteinFour.Geometry.frameTensorPairing_twoFormProduct line 9047
theorem OAI.PositiveEinsteinFour.Geometry.frameTensorPairing_blockTensor line 9066
Source documentation
Block assembly is four times the adjoint of the normalized block contraction.
```
theorem frameTensorPairing_blockTensor (R : CovariantCoordinates 4)
    (A : Mat3) (Q : Fin 3 → Mat4) :
    frameTensorPairing R (blockTensorCoordinates A Q) =
      4 * matrixPairing A (blockCoordinates R Q) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.Mat3, OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.frameTensorPairing, OAI.PositiveEinsteinFour.Geometry.blockTensorCoordinates, OAI.PositiveEinsteinFour.Geometry.blockCoordinates
theorem OAI.PositiveEinsteinFour.Geometry.frameTensorSquareNorm_of_blocks line 9086
theorem OAI.PositiveEinsteinFour.Geometry.squareNorm_one_add line 9119
theorem OAI.PositiveEinsteinFour.Geometry.curvature_blockCoordinates line 9132
theorem OAI.PositiveEinsteinFour.Geometry.frame_curvature_norm_energy line 9147
theorem OAI.PositiveEinsteinFour.Geometry.frame_weyl_norm_sum_same_base line 9183
theorem OAI.PositiveEinsteinFour.Geometry.frame_weyl_gradient_norm_energy line 9192
theorem OAI.PositiveEinsteinFour.Geometry.frame_weyl_gradient_sum_same_base line 9216
def OAI.PositiveEinsteinFour.Geometry.varianceDensity line 9243
def OAI.PositiveEinsteinFour.Geometry.traceCouplingTerm line 9248
theorem OAI.PositiveEinsteinFour.Geometry.scalarCouplingTerm_eq_trace_and_tests line 9257
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.totalEnergyField_apply line 9275
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.traceDeficitIntegrand_eq_arrays line 9286
def OAI.PositiveEinsteinFour.Geometry.MetricGreenData.coupledIntegrand line 9298
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.coupledIntegrand_eq_array line 9305
theorem OAI.PositiveEinsteinFour.Geometry.weylWeightGradient_norm_sq line 9343
def OAI.PositiveEinsteinFour.Geometry.plusRadialEnergy line 9354
def OAI.PositiveEinsteinFour.Geometry.minusRadialEnergy line 9357
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.coupledIntegrand_bound line 9360
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.radialEnergy_support line 9415
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.radialDifferenceSq_integrable line 9461
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.radialVarianceEnergy_integrable line 9491
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.varianceDensity_integrable line 9510
theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.coupledIntegrand_integrable line 9520

theorem OAI.PositiveEinsteinFour.Geometry.FrameReflectionData.coupledIntegral_nonneg line 9529

Source documentation

This is the integral assembly conditional on the separate weighted variance statement, not a published-input classification theorem.

theorem coupledIntegral_nonneg (o : OppositeWeylData d) [IsProbabilityMeasure μ]
    (hp : ShiftedCurvaturePositive g)
    (hdecomp : ∀ e : FrameBundle g, frameCurvature g e.base e.frame =
      Angular.einsteinCurvatureTensor (plusWeyl g e.base e.frame) (minusWeyl g e.base e.frame))
    (hpinch : ∀ e : FrameBundle g, normalizedBlockNorm (plusWeyl g e.base e.frame) +
      normalizedBlockNorm (minusWeyl g e.base e.frame) < 2)
    (hsecond : (∫ e, d.plusNormField e ^ 2 ∂μ) = ∫ e, d.minusNormField o e ^ 2 ∂μ)
    (hvariance : (∫ e, (d.plusNormField e - d.minusNormField o e) ^ 2 ∂μ) -
      (∫ e, d.plusNormField e - d.minusNormField o e ∂μ) ^ 2 ≤
      ∫ e, ‖blockRadialGradient (plusWeyl g e.base e.frame) (plusWeylGradient g e.base e.frame) -
        blockRadialGradient (minusWeyl g e.base e.frame) (minusWeylGradient g e.base e.frame)‖ ^ 2 /
        (4 + d.plusNormField e ^ 2 + d.minusNormField o e ^ 2) ∂μ) :
…

def OAI.PositiveEinsteinFour.QuaternionFrame.pfaffianFour line 9571
Source documentation
The Pfaffian with respect to the fixed orientation of four coordinates.
```
def pfaffianFour (A : Mat4) : ℝ :=
…
```
def OAI.PositiveEinsteinFour.QuaternionFrame.upperSquareFour line 9574
theorem OAI.PositiveEinsteinFour.QuaternionFrame.sandwich_apply line 9578
theorem OAI.PositiveEinsteinFour.QuaternionFrame.pfaffian_quaternion_zero line 9583
theorem OAI.PositiveEinsteinFour.QuaternionFrame.pfaffian_quaternion_one line 9591
theorem OAI.PositiveEinsteinFour.QuaternionFrame.pfaffian_quaternion_two line 9599
theorem OAI.PositiveEinsteinFour.QuaternionFrame.pfaffian_quaternion line 9607
theorem OAI.PositiveEinsteinFour.QuaternionFrame.pfaffian_opposite_zero line 9614
theorem OAI.PositiveEinsteinFour.QuaternionFrame.pfaffian_opposite_one line 9623
theorem OAI.PositiveEinsteinFour.QuaternionFrame.pfaffian_opposite_two line 9632
theorem OAI.PositiveEinsteinFour.QuaternionFrame.pfaffian_opposite line 9641
theorem OAI.PositiveEinsteinFour.QuaternionFrame.skew_diagonal_zero line 9648
theorem OAI.PositiveEinsteinFour.QuaternionFrame.upperSquareFour_eq_two line 9652
theorem OAI.PositiveEinsteinFour.QuaternionFrame.selfDual_of_pfaffian line 9668
theorem OAI.PositiveEinsteinFour.QuaternionFrame.antiSelfDual_of_pfaffian line 9689
theorem OAI.PositiveEinsteinFour.QuaternionFrame.selfDual_span line 9710
theorem OAI.PositiveEinsteinFour.QuaternionFrame.antiSelfDual_span line 9720
theorem OAI.PositiveEinsteinFour.QuaternionFrame.quaternion_orthogonal line 9731
theorem OAI.PositiveEinsteinFour.QuaternionFrame.opposite_orthogonal line 9738
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugate_skew line 9745
theorem OAI.PositiveEinsteinFour.QuaternionFrame.conjugate_orthogonal line 9754
theorem OAI.PositiveEinsteinFour.QuaternionFrame.oriented_quaternion_span line 9765
Source documentation
Positive-orientation orthogonal changes preserve the first quaternionic space.
```
theorem oriented_quaternion_span (P : Mat4) (hP : Pᵀ * P = 1) (hdet : P.det = 1)
    (s : Fin 3) :
    P * quaternionMatrix s * Pᵀ = imaginaryCombination quaternionMatrix
      (fun r => (P * quaternionMatrix s * Pᵀ) r.succ 0) := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination
theorem OAI.PositiveEinsteinFour.QuaternionFrame.oriented_opposite_span line 9777
Source documentation
The opposite quaternionic space is preserved by the same frame changes.
```
theorem oriented_opposite_span (P : Mat4) (hP : Pᵀ * P = 1) (hdet : P.det = 1)
    (s : Fin 3) :
    P * oppositeMatrix s * Pᵀ = imaginaryCombination oppositeMatrix
      (fun r => -(P * oppositeMatrix s * Pᵀ) r.succ 0) := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination
def OAI.PositiveEinsteinFour.Geometry.hodgeStarFour line 9810
Source documentation
Hodge star on two-forms in the positively oriented standard basis. The input is represented by a skew matrix; the formula also defines a linear map on arbitrary matrices.
```
def hodgeStarFour : Mat4 →ₗ[ℝ] Mat4 where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4
def OAI.PositiveEinsteinFour.Geometry.hodgeFirstTensor line 9823
Source documentation
Hodge star in the first alternating pair of a covariant four-tensor.
```
def hodgeFirstTensor : CovariantCoordinates 4 →ₗ[ℝ] CovariantCoordinates 4 where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates
theorem OAI.PositiveEinsteinFour.Geometry.hodgeStarFour_quaternion line 9835
theorem OAI.PositiveEinsteinFour.Geometry.hodgeStarFour_opposite line 9840
def OAI.PositiveEinsteinFour.Geometry.twoFormProductCoordinates line 9847
theorem OAI.PositiveEinsteinFour.Geometry.twoFormProductCoordinates_smul_left line 9850
theorem OAI.PositiveEinsteinFour.Geometry.hodgeFirstTensor_twoFormProduct line 9857
theorem OAI.PositiveEinsteinFour.Geometry.blockTensorCoordinates_sum line 9869
theorem OAI.PositiveEinsteinFour.Geometry.hodgeFirstTensor_block line 9876
theorem OAI.PositiveEinsteinFour.Geometry.hodgeFirstTensor_plus line 9883
theorem OAI.PositiveEinsteinFour.Geometry.hodgeFirstTensor_minus line 9889
theorem OAI.PositiveEinsteinFour.Geometry.frameTensorPairing_hodgeFirst_of_blocks line 9896
Source documentation
The signed curvature norm is the difference of the two block norms.
```
theorem frameTensorPairing_hodgeFirst_of_blocks (R : CovariantCoordinates 4)
    (A B : Mat3)
    (hR : R = blockTensorCoordinates A quaternionMatrix +
      blockTensorCoordinates B oppositeMatrix)
    (hA : blockCoordinates R quaternionMatrix = A)
    (hB : blockCoordinates R oppositeMatrix = B) :
    frameTensorPairing R (hodgeFirstTensor R) = 4 * (squareNorm A - squareNorm B) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.Mat3, OAI.PositiveEinsteinFour.Geometry.blockTensorCoordinates, OAI.PositiveEinsteinFour.Geometry.blockCoordinates, OAI.PositiveEinsteinFour.Geometry.frameTensorPairing, OAI.PositiveEinsteinFour.Geometry.hodgeFirstTensor
theorem OAI.PositiveEinsteinFour.Geometry.squareNorm_one_add_trace line 9914
def OAI.PositiveEinsteinFour.Geometry.curvatureEulerDensity line 9926
Source documentation
The curvature polynomial whose integral is the Euler number in the Chern--Gauss--Bonnet theorem. That global theorem is not used here.
```
def curvatureEulerDensity (R : CovariantCoordinates 4) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates
def OAI.PositiveEinsteinFour.Geometry.curvaturePontryaginDensity line 9932
Source documentation
The first Pontryagin density; its third is the signature density.
```
def curvaturePontryaginDensity (R : CovariantCoordinates 4) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates
def OAI.PositiveEinsteinFour.Geometry.curvatureSignatureDensity line 9935
theorem OAI.PositiveEinsteinFour.Geometry.frame_curvature_hodge_pairing line 9941
theorem OAI.PositiveEinsteinFour.Geometry.frame_curvature_eulerDensity line 9989
theorem OAI.PositiveEinsteinFour.Geometry.frame_curvature_pontryaginDensity line 10005
theorem OAI.PositiveEinsteinFour.Geometry.frame_curvature_signatureDensity line 10013
theorem OAI.PositiveEinsteinFour.Geometry.traceCouplingTerm_reflected_swap line 10040
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.traceDeficitIntegrand_reflection line 10052
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.preVarianceIntegrand_reflection line 10067
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.preVarianceGreen_oriented line 10077
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.coupledIntegral_oriented line 10098
def OAI.PositiveEinsteinFour.QuaternionFrame.fourMatrixPairing line 10141
theorem OAI.PositiveEinsteinFour.QuaternionFrame.fourMatrixPairing_eq_trace line 10143
theorem OAI.PositiveEinsteinFour.QuaternionFrame.fourMatrixPairing_add_left line 10149
theorem OAI.PositiveEinsteinFour.QuaternionFrame.fourMatrixPairing_add_right line 10153
theorem OAI.PositiveEinsteinFour.QuaternionFrame.fourMatrixPairing_smul_left line 10157
theorem OAI.PositiveEinsteinFour.QuaternionFrame.fourMatrixPairing_smul_right line 10162
theorem OAI.PositiveEinsteinFour.QuaternionFrame.fourMatrixPairing_conjugate line 10168
theorem OAI.PositiveEinsteinFour.QuaternionFrame.basis_pairing_combinations line 10178
theorem OAI.PositiveEinsteinFour.QuaternionFrame.coefficientMatrix_orthogonal line 10191
Source documentation
An orthogonal action on an orthogonal three-dimensional two-form basis has an orthogonal matrix of coefficients.
```
theorem coefficientMatrix_orthogonal (P : Mat4) (Q : Fin 3 → Mat4) (R : Mat3)
    (hP : Pᵀ * P = 1)
    (hQ : ∀ r s, fourMatrixPairing (Q r) (Q s) = if r = s then 4 else 0)
    (hR : ∀ s, P * Q s * Pᵀ = imaginaryCombination Q (fun r => R r s)) :
    Rᵀ * R = 1 := by
…
```
Mentions: OAI.PositiveEinsteinFour.QuaternionFrame.fourMatrixPairing, OAI.PositiveEinsteinFour.QuaternionFrame.imaginaryCombination
def OAI.PositiveEinsteinFour.QuaternionFrame.positiveOrientationMatrix line 10207
Source documentation
Coefficients of the positive two-form action.
```
def positiveOrientationMatrix (P : Mat4) : Mat3 := fun r s =>
…
```
def OAI.PositiveEinsteinFour.QuaternionFrame.negativeOrientationMatrix line 10211
Source documentation
Coefficients of the negative two-form action.
```
def negativeOrientationMatrix (P : Mat4) : Mat3 := fun r s =>
…
```
theorem OAI.PositiveEinsteinFour.QuaternionFrame.positiveOrientationMatrix_span line 10214
theorem OAI.PositiveEinsteinFour.QuaternionFrame.negativeOrientationMatrix_span line 10220
theorem OAI.PositiveEinsteinFour.QuaternionFrame.positiveOrientationMatrix_orthogonal line 10226
theorem OAI.PositiveEinsteinFour.QuaternionFrame.negativeOrientationMatrix_orthogonal line 10233
abbrev OAI.PositiveEinsteinFour.Geometry.TwoFormFour line 10257
def OAI.PositiveEinsteinFour.Geometry.twoFormMatrix line 10259
def OAI.PositiveEinsteinFour.Geometry.twoFormHodgeLinear line 10265
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodge_norm line 10273
def OAI.PositiveEinsteinFour.Geometry.twoFormHodge line 10279
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodge_involutive line 10283
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMatrix_hodge line 10286
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMatrix_skew line 10292
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMatrix_injective line 10296
def OAI.PositiveEinsteinFour.Geometry.twoFormSelfDual line 10307
def OAI.PositiveEinsteinFour.Geometry.twoFormAntiSelfDual line 10309
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_decomposition line 10311
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSelfDual_hodge line 10316
theorem OAI.PositiveEinsteinFour.Geometry.twoFormAntiSelfDual_hodge line 10321
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_eigenspaces_orthogonal line 10326
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSelfDual_orthogonal line 10332
theorem OAI.PositiveEinsteinFour.Geometry.blockRadialGradient_aestronglyMeasurable line 10353
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.radialVector_measurable line 10371
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.oppositeRadialVector_measurable line 10376
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.radialEnergy_integrable line 10384
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.oppositeRadialEnergy_integrable line 10396
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.one_block_zero_of_variance line 10437
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_one line 10503
theorem OAI.PositiveEinsteinFour.Geometry.frameTensorPairing_adjoint line 10519
Source documentation
The adjoint of tensor pullback by an orthogonal matrix is pullback by its transpose, on all covariant slots.
```
theorem frameTensorPairing_adjoint {n : ℕ} (P : Mat4) (hP : Pᵀ * P = 1)
    (T S : CovariantCoordinates n) :
    frameTensorPairing (frameTensor P T) S =
      frameTensorPairing T (frameTensor Pᵀ S) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.frameTensorPairing, OAI.PositiveEinsteinFour.Geometry.frameTensor
theorem OAI.PositiveEinsteinFour.Geometry.bilinearPullback_apply line 10530
theorem OAI.PositiveEinsteinFour.Geometry.sumPair_product line 10535

theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_twoFormProduct line 10550

Source documentation

Pullback of the tensor product of two two-forms.

theorem frameTensor_twoFormProduct (P A B : Mat4) :
    frameTensor P (fun a : Fin 4 → Fin 4 => twoFormProduct A B (a 0) (a 1) (a 2) (a 3)) =
      fun a => twoFormProduct (Pᵀ * A * P) (Pᵀ * B * P)
        (a 0) (a 1) (a 2) (a 3) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.frameTensor

theorem OAI.PositiveEinsteinFour.Geometry.twoFormPairing_frameTensor line 10571
theorem OAI.PositiveEinsteinFour.Geometry.blockCoordinates_frameTensor line 10583
Source documentation
The block contraction changes by the actual induced three-dimensional orthogonal coefficient matrix.
```
theorem blockCoordinates_frameTensor (P : Mat4) (hP : Pᵀ * P = 1)
    (Q : Fin 3 → Mat4) (R : Mat3)
    (hR : ∀ s, P * Q s * Pᵀ = imaginaryCombination Q (fun r => R r s))
    (T : CovariantCoordinates 4) :
    blockCoordinates (frameTensor P T) Q =
      conjugateMatrix R (blockCoordinates T Q) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.Mat3, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.blockCoordinates, OAI.PositiveEinsteinFour.Geometry.frameTensor
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.changeMatrix_det_one line 10602
Source documentation
Two frames in the same oriented component have an orientation-preserving orthogonal change matrix.
```
theorem OrthonormalFrame.changeMatrix_det_one (e f : OrthonormalFrame g c)
    (hor : 0 < e.matrix.det * f.matrix.det) : (e.changeMatrix f).det = 1 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureBlock_eq line 10618
theorem OAI.PositiveEinsteinFour.Geometry.blockNorm_same_oriented_frame line 10627
theorem OAI.PositiveEinsteinFour.Geometry.plusWeyl_norm_same_oriented_frame line 10647
theorem OAI.PositiveEinsteinFour.Geometry.minusWeyl_norm_same_oriented_frame line 10657
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusNorm_frame line 10668
theorem OAI.PositiveEinsteinFour.Geometry.actual_minusNorm_frame line 10674
def OAI.PositiveEinsteinFour.Geometry.loweredMatrixTensor line 10697
theorem OAI.PositiveEinsteinFour.Geometry.lowered_matrix_transition line 10700
theorem OAI.PositiveEinsteinFour.Geometry.loweredMatrixTensor_transition line 10716
theorem OAI.PositiveEinsteinFour.Geometry.loweredMatrixTensor_curvature line 10742
theorem OAI.PositiveEinsteinFour.Geometry.curvatureCoordinates_transition line 10753
Source documentation
Actual lowered curvature is a covariant four-tensor on chart overlaps.
```
theorem curvatureCoordinates_transition (g : SmoothMetric M) (c d : M)
    (z : FourSpace) (hz : z ∈ (chartAt FourSpace c).target)
    (hx : (chartAt FourSpace c).symm z ∈ (chartAt FourSpace d).source) :
    curvatureCoordinates g c z = frameTensor (chartTransitionMatrix c d z)
      (curvatureCoordinates g d (chartTransition c d z)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.curvatureCoordinates, OAI.PositiveEinsteinFour.Geometry.frameTensor, OAI.PositiveEinsteinFour.Geometry.chartTransitionMatrix, OAI.PositiveEinsteinFour.Geometry.chartTransition
def OAI.PositiveEinsteinFour.Geometry.twoFormSkewAction line 10783
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSkewAction_matrix line 10792
def OAI.PositiveEinsteinFour.Geometry.twoFormSkewActionLinear line 10799
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSkewAction_hodge line 10808
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSkewAction_skewAdjoint line 10813
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSkewAction_selfDual line 10819
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSkewAction_antiSelfDual line 10823
def OAI.PositiveEinsteinFour.Geometry.selfDualTwoForms line 10843
def OAI.PositiveEinsteinFour.Geometry.antiSelfDualTwoForms line 10856
def OAI.PositiveEinsteinFour.Geometry.selfDualTwoFormCoordinates line 10869
def OAI.PositiveEinsteinFour.Geometry.antiSelfDualTwoFormCoordinates line 10872
theorem OAI.PositiveEinsteinFour.Geometry.selfDualTwoFormCoordinates_hodge line 10875
theorem OAI.PositiveEinsteinFour.Geometry.antiSelfDualTwoFormCoordinates_hodge line 10880
def OAI.PositiveEinsteinFour.Geometry.selfDualTwoFormEquiv line 10885
def OAI.PositiveEinsteinFour.Geometry.antiSelfDualTwoFormEquiv line 10916
theorem OAI.PositiveEinsteinFour.Geometry.selfDualTwoForms_finrank line 10947
theorem OAI.PositiveEinsteinFour.Geometry.antiSelfDualTwoForms_finrank line 10951
theorem OAI.PositiveEinsteinFour.Geometry.hodgeStarFour_quaternion_combination line 10972
theorem OAI.PositiveEinsteinFour.Geometry.hodgeStarFour_opposite_combination line 10977
theorem OAI.PositiveEinsteinFour.Geometry.hodgeStarFour_sandwich_quaternion line 10983
theorem OAI.PositiveEinsteinFour.Geometry.hodgeStarFour_sandwich_opposite line 10989
theorem OAI.PositiveEinsteinFour.Geometry.sandwich_combination line 10995
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMatrix_quaternion_decomposition line 11000
theorem OAI.PositiveEinsteinFour.Geometry.hodgeStarFour_oriented_frame_change line 11011
abbrev OAI.PositiveEinsteinFour.Geometry.CoordinateColumn line 11049
def OAI.PositiveEinsteinFour.Geometry.metricPair line 11051
def OAI.PositiveEinsteinFour.Geometry.gramRemove line 11054
def OAI.PositiveEinsteinFour.Geometry.gramColumnZero line 11057
def OAI.PositiveEinsteinFour.Geometry.gramColumnOne line 11059
def OAI.PositiveEinsteinFour.Geometry.gramColumnTwo line 11062
def OAI.PositiveEinsteinFour.Geometry.gramColumnThree line 11065
def OAI.PositiveEinsteinFour.Geometry.gramColumn line 11069
theorem OAI.PositiveEinsteinFour.Geometry.gramColumn_diagonal line 11073
Source documentation
The lower-triangular leading coefficient of every residual is one.
```
theorem gramColumn_diagonal (G : Mat4) (i : Fin 4) : gramColumn G i i = 1 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.gramColumn
theorem OAI.PositiveEinsteinFour.Geometry.gramColumn_above line 11077
theorem OAI.PositiveEinsteinFour.Geometry.gramColumn_ne_zero line 11082
theorem OAI.PositiveEinsteinFour.Geometry.metricPair_pos line 11088
theorem OAI.PositiveEinsteinFour.Geometry.gramColumn_energy_pos line 11093
theorem OAI.PositiveEinsteinFour.Geometry.metricPair_symm line 11097
theorem OAI.PositiveEinsteinFour.Geometry.metricPair_gramRemove line 11108
theorem OAI.PositiveEinsteinFour.Geometry.metricPair_gramRemove_self line 11117
theorem OAI.PositiveEinsteinFour.Geometry.metricPair_gramRemove_orthogonal line 11121
theorem OAI.PositiveEinsteinFour.Geometry.gramColumn_orthogonal line 11128
Source documentation
Orthogonality is proved before normalization, using only the exact projection formula and positivity of the residual energies.
```
theorem gramColumn_orthogonal (G : Mat4) (hG : G.PosDef)
    (i j : Fin 4) (hij : i ≠ j) : metricPair G (gramColumn G i) (gramColumn G j) = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.metricPair, OAI.PositiveEinsteinFour.Geometry.gramColumn
def OAI.PositiveEinsteinFour.Geometry.gramNormalizer line 11165
Source documentation
The inverse square roots of the four residual energies give an orthonormal frame, with no eigenvector selection.
```
def gramNormalizer (G : Mat4) : Mat4 := fun k i =>
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4
theorem OAI.PositiveEinsteinFour.Geometry.metricPair_scaled line 11168
theorem OAI.PositiveEinsteinFour.Geometry.gramNormalizer_normalizes line 11174

theorem OAI.PositiveEinsteinFour.Geometry.metricPair_contDiffAt line 11197

Source documentation

Smoothness of the finite bilinear pairing with varying coefficients.

theorem metricPair_contDiffAt {G : FourSpace → Mat4} {u v : FourSpace → CoordinateColumn}
    {z : FourSpace} (hG : ∀ i j, ContDiffAt ℝ ∞ (fun w => G w i j) z)
    (hu : ∀ i, ContDiffAt ℝ ∞ (fun w => u w i) z)
    (hv : ∀ i, ContDiffAt ℝ ∞ (fun w => v w i) z) :
    ContDiffAt ℝ ∞ (fun w => metricPair (G w) (u w) (v w)) z := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CoordinateColumn, OAI.PositiveEinsteinFour.Geometry.metricPair

theorem OAI.PositiveEinsteinFour.Geometry.gramRemove_contDiffAt line 11209
theorem OAI.PositiveEinsteinFour.Geometry.gramColumn_contDiffAt line 11218
theorem OAI.PositiveEinsteinFour.Geometry.gramNormalizer_contDiffAt line 11247
structure OAI.PositiveEinsteinFour.Geometry.ScalarVarianceInputs line 11280
Source documentation
Only the precise classical inputs of the smooth scalar argument.
```
structure ScalarVarianceInputs (d : MetricGreenData g μ) (orientation : FrameOrientation g) : Prop where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.FrameOrientation
theorem OAI.PositiveEinsteinFour.Geometry.blockRadialGradient_zero_of_norm_zero line 11290
def OAI.PositiveEinsteinFour.Geometry.normRegularizationParameter line 11297
theorem OAI.PositiveEinsteinFour.Geometry.normRegularizationParameter_mem line 11299
theorem OAI.PositiveEinsteinFour.Geometry.normRegularizationParameter_tendsto line 11307
theorem OAI.PositiveEinsteinFour.Geometry.scalarVarianceWeight_continuous line 11311
theorem OAI.PositiveEinsteinFour.Geometry.scalarVarianceWeight_ge_one line 11316
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.normDifferenceVariance line 11323
def OAI.PositiveEinsteinFour.Geometry.twoFormCodifferentialSymbol line 11373
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodifferentialSymbol_matrix line 11379
def OAI.PositiveEinsteinFour.Geometry.twoFormCodifferentialSymbolLinear line 11385
theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamSymbol_norm_sq line 11394
theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamSymbol_inner line 11402
theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamSymbol_injective line 11415
theorem OAI.PositiveEinsteinFour.Geometry.tensorPartial_comp line 11441
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_weighted_sum line 11451

theorem OAI.PositiveEinsteinFour.Geometry.covariantDirection_pullback line 11463

Source documentation

Connection cancellation in one direction, before adding the derivative slot to the tensor pullback.

theorem covariantDirection_pullback {n : ℕ}
    (F : FourSpace → FourSpace) (E : FourSpace → Mat4)
    (C D : Fin 4 → FourSpace → Mat4) (T : FourSpace → CovariantCoordinates n)
    (z : FourSpace) (hF : DifferentiableAt ℝ F z)
    (hE : ∀ a b, DifferentiableAt ℝ (fun w => E w a b) z)
    (hT : ∀ a, DifferentiableAt ℝ (fun w => T w a) (F z))
    (hJ : E z = jacobianMatrix F z) (i : Fin 4)
    (hC : E z * C i z = matrixPartial E i z +
      (∑ r, E z r i • D r (F z)) * E z) :
    tensorCovariantDirection C (fun w => frameTensor (E w) (T (F w))) i z =
      frameTensor (E z) (∑ r, E z r i • tensorCovariantDirection D T r (F z)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.jacobianMatrix, OAI.PositiveEinsteinFour.Geometry.matrixPartial, OAI.PositiveEinsteinFour.Geometry.tensorCovariantDirection, OAI.PositiveEinsteinFour.Geometry.frameTensor

theorem OAI.PositiveEinsteinFour.Geometry.chart_overlap_eventually line 11500

theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_chart_transition line 11515

Source documentation

Naturality of the coordinate Levi-Civita derivative. The tensor equality is local; no choice of a global frame is involved.

theorem covariantDerivative_chart_transition (g : SmoothMetric M) (c d : M)
    {n : ℕ} (S T : FourSpace → CovariantCoordinates n) (z : FourSpace)
    (hz : z ∈ (chartAt FourSpace c).target)
    (hx : (chartAt FourSpace c).symm z ∈ (chartAt FourSpace d).source)
    (hT : ∀ a, DifferentiableAt ℝ (fun w => T w a) (chartTransition c d z))
    (hS : S =ᶠ[𝓝 z] fun w => frameTensor (chartTransitionMatrix c d w)
      (T (chartTransition c d w))) :
    covariantDerivative g c S z = frameTensor (chartTransitionMatrix c d z)
      (covariantDerivative g d T (chartTransition c d z)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.chartTransition, OAI.PositiveEinsteinFour.Geometry.frameTensor, OAI.PositiveEinsteinFour.Geometry.chartTransitionMatrix, OAI.PositiveEinsteinFour.Geometry.covariantDerivative

abbrev OAI.PositiveEinsteinFour.Geometry.ChartTarget line 11558
def OAI.PositiveEinsteinFour.Geometry.chartGramMatrix line 11560
theorem OAI.PositiveEinsteinFour.Geometry.chartGramMatrix_normalizes line 11563
def OAI.PositiveEinsteinFour.Geometry.chartGramFrame line 11573
def OAI.PositiveEinsteinFour.Geometry.chartGramSection line 11588
theorem OAI.PositiveEinsteinFour.Geometry.chartGramMatrix_contDiffAt line 11592
theorem OAI.PositiveEinsteinFour.Geometry.chart_inverse_moving_vector_smooth line 11601
theorem OAI.PositiveEinsteinFour.Geometry.chartInverseMatrix_apply line 11624
theorem OAI.PositiveEinsteinFour.Geometry.chartGramFrame_vector line 11637
theorem OAI.PositiveEinsteinFour.Geometry.continuous_chartGramSection line 11645
def OAI.PositiveEinsteinFour.Geometry.chartGramBlock line 11668
Source documentation
The framed coordinate curvature, expressed entirely in one fixed chart.
```
def chartGramBlock (g : SmoothMetric M) (c : M) (S : Mat4)
    (Q : Fin 3 → Mat4) (z : FourSpace) : Mat3 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.Mat3
theorem OAI.PositiveEinsteinFour.Geometry.chartTransitionMatrix_to_center line 11674
theorem OAI.PositiveEinsteinFour.Geometry.chartGramBlock_eq_frame line 11696
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_contDiffAt line 11722
theorem OAI.PositiveEinsteinFour.Geometry.blockCoordinates_contDiffAt line 11732
theorem OAI.PositiveEinsteinFour.Geometry.chartGramBlock_contDiffAt line 11745
theorem OAI.PositiveEinsteinFour.Geometry.chartGramBlock_squareNorm_contDiffAt line 11758
def OAI.PositiveEinsteinFour.Geometry.localGramSection line 11770
theorem OAI.PositiveEinsteinFour.Geometry.localGramSection_base line 11777
theorem OAI.PositiveEinsteinFour.Geometry.continuousAt_localGramSection line 11785
theorem OAI.PositiveEinsteinFour.Geometry.frame_eq_of_matrix_eq line 11802
Distinct definitions of this name: OAI/Geometry/EinsteinFour/GeodesicGeometry04.lean:11666 (different declaration text), OAI/Geometry/EinsteinFour/WeylEstimates03.lean:951 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.frame_eq_of_matrix_eq@path.
theorem OAI.PositiveEinsteinFour.Geometry.exists_positive_localGramSection line 11812
Source documentation
A constant orthogonal change makes the local smooth frame positive at its center; openness of the chosen component then makes it positive nearby.
```
theorem exists_positive_localGramSection (g : SmoothMetric M) (o : FrameOrientation g)
    (c : M) : ∃ S : Mat4, ∃ hS : Sᵀ * S = 1,
      ∀ᶠ x in 𝓝 c, localGramSection g c S hS x ∈ o.positive := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.localGramSection
abbrev OAI.PositiveEinsteinFour.Geometry.HodgeEvenFiber line 11853
abbrev OAI.PositiveEinsteinFour.Geometry.HodgeOddFiber line 11854
def OAI.PositiveEinsteinFour.Geometry.hodgeDiracEvenSymbol line 11856
theorem OAI.PositiveEinsteinFour.Geometry.hodgeDiracEvenSymbol_apply line 11866
theorem OAI.PositiveEinsteinFour.Geometry.hodgeDiracEvenSymbol_norm_sq line 11871
theorem OAI.PositiveEinsteinFour.Geometry.hodgeDiracEvenSymbol_eq_zero line 11881
theorem OAI.PositiveEinsteinFour.Geometry.hodgeDiracEvenSymbol_injective line 11897
theorem OAI.PositiveEinsteinFour.Geometry.hodgeDiracEvenSymbol_bijective line 11904
def OAI.PositiveEinsteinFour.Geometry.twoFormExtract line 11927
theorem OAI.PositiveEinsteinFour.Geometry.twoFormExtract_matrix line 11930
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMatrix_extract line 11934
def OAI.PositiveEinsteinFour.Geometry.twoFormFrameAction line 11942
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMatrix_frameAction line 11945
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameAction_one line 11951
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameAction_comp line 11955
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMatrix_add line 11960
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMatrix_smul line 11965
def OAI.PositiveEinsteinFour.Geometry.twoFormFrameActionLinear line 11970
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameAction_hodge line 11980
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.plusWeightedNormVariance line 12014
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.plusWeightedHVariance line 12035
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.minusWeightedNormVariance line 12059
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.minusWeightedHVariance line 12080