WeylEstimates03.lean`

1420 declarations, 0 contain sorry, 0 declared as axioms

Continuity of the actual chart density gives sharp local comparison of its weighted measure with the constant density at the chart point.

theorem OAI.PositiveEinsteinFour.Geometry.exists_chartDensity_local_bounds line 104
abbrev OAI.PositiveEinsteinFour.Geometry.OrthogonalFour line 159
theorem OAI.PositiveEinsteinFour.Geometry.orthogonalFour_entry_bound line 161
theorem OAI.PositiveEinsteinFour.Geometry.isCompact_orthogonalFour line 171
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 181) line 181
def OAI.PositiveEinsteinFour.Geometry.coordinateMomentum line 205
theorem OAI.PositiveEinsteinFour.Geometry.coordinateMomentum_det line 209
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian_coordinateMomentum line 222
theorem OAI.PositiveEinsteinFour.Geometry.coordinateMomentum_measurePreserving line 242
Source documentation
At each base point, the lowering map sends Euclidean fiber volume weighted by the metric density to ordinary cotangent fiber volume.
```
theorem coordinateMomentum_measurePreserving (g : SmoothMetric M) (c : M)
    (x : FourSpace) (hx : x ∈ (chartAt FourSpace c).target)
    (E : Mat4) (hE : Eᵀ * metricInChart g c x * E = 1) :
    MeasurePreserving (coordinateMomentum g c x E)
      (ENNReal.ofReal (chartVolumeDensity g c x) • (volume : Measure FourSpace)) volume := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.coordinateMomentum, OAI.PositiveEinsteinFour.Geometry.chartVolumeDensity
theorem OAI.PositiveEinsteinFour.Geometry.chartGramMomentum_det line 267
Source documentation
The concrete smooth Gram frame gives the required lowering map in every chart, without making an eigenvector selection.
```
theorem chartGramMomentum_det (g : SmoothMetric M) (c : M)
    (x : FourSpace) (hx : x ∈ (chartAt FourSpace c).target) :
    |(metricInChart g c x * chartGramMatrix g c 1 x).det| = chartVolumeDensity g c x :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.chartGramMatrix, OAI.PositiveEinsteinFour.Geometry.chartVolumeDensity
theorem OAI.PositiveEinsteinFour.Geometry.chartGramMomentum_energy line 273
theorem OAI.PositiveEinsteinFour.Geometry.sum_cross_pairs line 297
theorem OAI.PositiveEinsteinFour.Geometry.sum_parallel_pairs line 307
def OAI.PositiveEinsteinFour.Geometry.unitMatrixTensor line 319
theorem OAI.PositiveEinsteinFour.Geometry.matrix_pairing_expansion line 322
theorem OAI.PositiveEinsteinFour.Geometry.unitMatrixTensor_pullback line 327
theorem OAI.PositiveEinsteinFour.Geometry.unitCurvatureCoordinates_transition line 371
theorem OAI.PositiveEinsteinFour.Geometry.normalizedWeylCoordinates_transition line 382
def OAI.PositiveEinsteinFour.Geometry.iteratedWeylDerivative line 397
Source documentation
Only three derivatives are used below, but retaining the natural number index makes the local covariance proof a single rank induction.
```
def iteratedWeylDerivative (g : SmoothMetric M) (c : M) :
    (k : ℕ) → FourSpace → CovariantCoordinates (4 + k)
  | 0 => normalizedWeylCoordinates g c
  | k + 1 => covariantDerivative g c (iteratedWeylDerivative g c k)
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.normalizedWeylCoordinates, OAI.PositiveEinsteinFour.Geometry.covariantDerivative
theorem OAI.PositiveEinsteinFour.Geometry.iteratedWeylDerivative_contDiffAt line 402
theorem OAI.PositiveEinsteinFour.Geometry.iteratedWeylDerivative_transition line 414
def OAI.PositiveEinsteinFour.Geometry.twoFormTensor line 447
theorem OAI.PositiveEinsteinFour.Geometry.twoFormTensor_frameAction line 450
theorem OAI.PositiveEinsteinFour.Geometry.twoFormTensor_norm line 468
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameAction_norm line 477
def OAI.PositiveEinsteinFour.Geometry.twoFormFrameIsometry line 483
def OAI.PositiveEinsteinFour.Geometry.frozenFrameMetric line 508
theorem OAI.PositiveEinsteinFour.Geometry.frozenFrameMetric_self line 512
theorem OAI.PositiveEinsteinFour.Geometry.frozenFrameMetric_continuousAt line 516
theorem OAI.PositiveEinsteinFour.Geometry.frozenFrameMetric_near_identity line 526
theorem OAI.PositiveEinsteinFour.Geometry.frozenFrameMetric_pairing line 549
theorem OAI.PositiveEinsteinFour.Geometry.frozenFrameMetric_tangentNorm line 558

theorem OAI.PositiveEinsteinFour.Geometry.frozenFrameMetric_tangentNorm_near line 568

Source documentation

Arbitrarily sharp bounds on the actual inverse-chart tangent norm, uniform over all tangent vectors in the frozen orthonormal coordinates.

theorem frozenFrameMetric_tangentNorm_near (g : SmoothMetric M) (c : M)
    (z₀ : ChartTarget c) (δ : ℝ) (hδ : 0 < δ) (hδone : δ ≤ 1) :
    ∀ᶠ z in 𝓝 z₀.val, ∀ v : FourSpace,
      Real.sqrt (1 - δ) * ‖v‖ ≤
        metricTangentNorm g ((chartAt FourSpace c).symm z)
          (mfderiv I4 I4 (chartAt FourSpace c).symm z
            (WithLp.toLp 2 (chartGramMatrix g c 1 z₀ *ᵥ WithLp.ofLp v))) ∧
      metricTangentNorm g ((chartAt FourSpace c).symm z)
          (mfderiv I4 I4 (chartAt FourSpace c).symm z
            (WithLp.toLp 2 (chartGramMatrix g c 1 z₀ *ᵥ WithLp.ofLp v))) ≤
        Real.sqrt (1 + δ) * ‖v‖ := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.ChartTarget, OAI.PositiveEinsteinFour.Geometry.metricTangentNorm, OAI.PositiveEinsteinFour.Geometry.chartGramMatrix

theorem OAI.PositiveEinsteinFour.Geometry.integral_div_le_of_one_le line 608
theorem OAI.PositiveEinsteinFour.Geometry.hLimitEnergy_split line 622
theorem OAI.PositiveEinsteinFour.Geometry.final_H_variance_le line 629
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.plusNormVariance line 661
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.plusHVariance line 681
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.minusNormVariance line 707
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.minusHVariance line 727
theorem OAI.PositiveEinsteinFour.Geometry.oriented_frame_normSquare_smooth line 773
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusNorm_square_smooth line 805
theorem OAI.PositiveEinsteinFour.Geometry.actual_minusNorm_square_smooth line 811
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_frameTensor line 835
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_coordinate_comp line 858

theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_parallel_frameTensor line 877

Source documentation

A tensor evaluated on a parallel moving frame differentiates to its covariant derivative in the velocity frame direction.

theorem hasDerivAt_parallel_frameTensor {n : ℕ} (g : SmoothMetric M) (c : M)
    (x : ℝ → FourSpace) (E : ℝ → Mat4) (T : FourSpace → CovariantCoordinates n)
    (t : ℝ) (k : Fin 4)
    (hx : HasDerivAt x (WithLp.toLp 2 (fun r => E t r k)) t)
    (hE : ∀ i j, HasDerivAt (fun s => E s i j)
      (-((∑ r, E t r k • connectionMatrix g c r (x t)) * E t) i j) t)
    (hT : ∀ a, DifferentiableAt ℝ (fun z => T z a) (x t))
    (a : Fin n → Fin 4) :
    HasDerivAt (fun s => frameTensor (E s) (T (x s)) a)
      (frameTensor (E t) (covariantDerivative g c T (x t)) (Fin.cons k a)) t := by
…

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

theorem OAI.PositiveEinsteinFour.Geometry.frame_eq_of_matrix_eq line 951
Distinct definitions of this name: OAI/Geometry/EinsteinFour/CurvatureTensors02.lean:11802 (different declaration text), OAI/Geometry/EinsteinFour/GeodesicGeometry04.lean:11666 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.frame_eq_of_matrix_eq@path.
def OAI.PositiveEinsteinFour.Geometry.jointChartGramSection line 961
theorem OAI.PositiveEinsteinFour.Geometry.continuous_jointChartGramSection line 965
theorem OAI.PositiveEinsteinFour.Geometry.chartGramFrame_surjective line 1014
def OAI.PositiveEinsteinFour.Geometry.frameChartMatrix line 1049
Source documentation
Components of an actual frame in the fixed chart at c.
```
def frameChartMatrix (g : SmoothMetric M) (c : M) (e : FrameBundle g) : Mat4 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.Mat4
theorem OAI.PositiveEinsteinFour.Geometry.frameChartMatrix_continuousAt line 1053
theorem OAI.PositiveEinsteinFour.Geometry.frameChartMatrix_eq line 1075

theorem OAI.PositiveEinsteinFour.Geometry.continuous_framedTensor line 1100

Source documentation

A coordinate tensor is evaluated continuously on frames once its local components are continuous and its chart transition law has been proved.

theorem continuous_framedTensor {n : ℕ} (g : SmoothMetric M)
    (T : M → FourSpace → CovariantCoordinates n)
    (hT : ∀ c z, z ∈ (chartAt FourSpace c).target →
      ∀ a, ContinuousAt (fun w => T c w a) z)
    (hchange : ∀ c d z, z ∈ (chartAt FourSpace c).target →
      (chartAt FourSpace c).symm z ∈ (chartAt FourSpace d).source →
      T c z = frameTensor (chartTransitionMatrix c d z) (T d (chartTransition c d z))) :
    Continuous (fun e : FrameBundle g => frameTensor e.frame.matrix
      (T e.base (chartAt FourSpace e.base e.base))) := by
…

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

theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_localGramSection line 1163
theorem OAI.PositiveEinsteinFour.Geometry.exists_measurable_positive_frame line 1180
theorem OAI.PositiveEinsteinFour.Geometry.metricEDistance_chart_symm_linear_le line 1251
abbrev OAI.PositiveEinsteinFour.Geometry.OrientedOrthogonalFour line 1329
theorem OAI.PositiveEinsteinFour.Geometry.isCompact_orientedOrthogonalFour line 1331
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 1341) line 1341
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 1344) line 1344
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 1356) line 1356
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 1357) line 1357
def OAI.PositiveEinsteinFour.Geometry.orientedFrameHaar line 1359
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 1361) line 1361
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 1365) line 1365
theorem OAI.PositiveEinsteinFour.Geometry.orientedFrameHaar_left line 1368
theorem OAI.PositiveEinsteinFour.Geometry.orientedFrameHaar_right line 1372
structure OAI.PositiveEinsteinFour.Geometry.OrientedNormRegularity line 1398
theorem OAI.PositiveEinsteinFour.Geometry.actual_orientedNormRegularity line 1402
theorem OAI.PositiveEinsteinFour.Geometry.OrientedNormRegularity.toPetersenInput line 1407
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.changeMatrix_self line 1434
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.changeMatrix_comp line 1438
def OAI.PositiveEinsteinFour.Geometry.twoFormFrameValue line 1444
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameValue_at_orientation line 1448
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameValue_change line 1452
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameValue_norm line 1458
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameValue_add line 1462
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameValue_zero line 1467
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameValue_smul line 1471
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameValue_hodge line 1476
def OAI.PositiveEinsteinFour.Geometry.twoFormDerivativeRows line 1500
theorem OAI.PositiveEinsteinFour.Geometry.twoFormDerivativeRows_cons line 1503
theorem OAI.PositiveEinsteinFour.Geometry.twoFormDerivativeRows_norm line 1507
theorem OAI.PositiveEinsteinFour.Geometry.twoFormDerivativeRows_hodge_norm line 1516
def OAI.PositiveEinsteinFour.Geometry.orientedEulerDensity line 1543
def OAI.PositiveEinsteinFour.Geometry.orientedSignatureDensity line 1547
theorem OAI.PositiveEinsteinFour.Geometry.orientedEulerDensity_eq line 1552
theorem OAI.PositiveEinsteinFour.Geometry.orientedSignatureDensity_eq line 1558
theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_integral_eq_total_mul line 1563
theorem OAI.PositiveEinsteinFour.Geometry.integral_orientedEulerDensity line 1572
theorem OAI.PositiveEinsteinFour.Geometry.integral_orientedSignatureDensity line 1592
theorem OAI.PositiveEinsteinFour.Geometry.exists_compact_frame_neighborhood line 1629
theorem OAI.PositiveEinsteinFour.Geometry.actual_compactFrameBundle line 1671
theorem OAI.PositiveEinsteinFour.Geometry.frame_ext_matrix line 1705
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 1715) line 1715
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 1716) line 1716
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 1717) line 1717
def OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.rotate line 1723
def OAI.PositiveEinsteinFour.Geometry.FrameBundle.rotate line 1734
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.rotate_vector line 1737
def OAI.PositiveEinsteinFour.Geometry.orientedToOrthogonal line 1747
theorem OAI.PositiveEinsteinFour.Geometry.continuous_orientedToOrthogonal line 1752
theorem OAI.PositiveEinsteinFour.Geometry.trivialization_sum_vectors line 1755
theorem OAI.PositiveEinsteinFour.Geometry.continuous_frameRotate line 1765
theorem OAI.PositiveEinsteinFour.Geometry.frameRotate_oriented_positive line 1812
theorem OAI.PositiveEinsteinFour.Geometry.frameRotate_one line 1820
theorem OAI.PositiveEinsteinFour.Geometry.frameRotate_mul line 1828
theorem OAI.PositiveEinsteinFour.Geometry.continuous_blockCoordinates line 1855
theorem OAI.PositiveEinsteinFour.Geometry.continuous_framedWeylDerivative line 1874
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeyl_continuous line 1883
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylGradient_continuous line 1891
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylHessian_continuous line 1903
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylThirdDerivative_continuous line 1915
theorem OAI.PositiveEinsteinFour.Geometry.iInf_open_interval line 1952
Also declared: OAI/Geometry/EinsteinFour/MetricChartLipschitz.lean:22 (same declaration text).
theorem OAI.PositiveEinsteinFour.Geometry.exists_linear_chart_lipschitz_of_bound line 1962
def OAI.PositiveEinsteinFour.Geometry.orientationLinearMatrix line 2048
theorem OAI.PositiveEinsteinFour.Geometry.orientationLinearMatrix_det line 2051
theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_frameChartMatrix line 2060
theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_frameChartMatrix_det line 2094
structure OAI.PositiveEinsteinFour.Geometry.ParallelFrameCurveAt line 2124
Source documentation
The local velocity and parallel-frame equations in the fixed chart centered at the current base point.
```
structure ParallelFrameCurveAt (g : SmoothMetric M) (γ : ℝ → FrameBundle g)
    (k : Fin 4) (t : ℝ) : Prop where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle
theorem OAI.PositiveEinsteinFour.Geometry.framedTensor_eq_fixedChart line 2135

theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_framedTensor line 2155

Source documentation

A chart-covariant tensor differentiates along an actual parallel frame curve to its framed covariant derivative, with the new direction first.

theorem hasDerivAt_framedTensor {n : ℕ} (g : SmoothMetric M)
    (T : M → FourSpace → CovariantCoordinates n)
    (hT : ∀ c z, z ∈ (chartAt FourSpace c).target →
      ∀ a, DifferentiableAt ℝ (fun w => T c w a) z)
    (hchange : ∀ c d z, z ∈ (chartAt FourSpace c).target →
      (chartAt FourSpace c).symm z ∈ (chartAt FourSpace d).source →
      T c z = frameTensor (chartTransitionMatrix c d z) (T d (chartTransition c d z)))
    (hDchange : ∀ c d z, z ∈ (chartAt FourSpace c).target →
      (chartAt FourSpace c).symm z ∈ (chartAt FourSpace d).source →
      covariantDerivative g c (T c) z = frameTensor (chartTransitionMatrix c d z)
        (covariantDerivative g d (T d) (chartTransition c d z)))
    (γ : ℝ → FrameBundle g) (t : ℝ) (k : Fin 4)
…

theorem OAI.PositiveEinsteinFour.Geometry.scalar_field_contDiffAt line 2215
theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinates_transition line 2223
def OAI.PositiveEinsteinFour.Geometry.iteratedScalarDerivative line 2234
theorem OAI.PositiveEinsteinFour.Geometry.iteratedScalarDerivative_contDiffAt line 2239
theorem OAI.PositiveEinsteinFour.Geometry.iteratedScalarDerivative_transition line 2249
theorem OAI.PositiveEinsteinFour.Geometry.continuous_framedScalarDerivative line 2266
theorem OAI.PositiveEinsteinFour.Geometry.actual_scalarValue_continuous line 2276
theorem OAI.PositiveEinsteinFour.Geometry.actual_scalarGradient_continuous line 2281
theorem OAI.PositiveEinsteinFour.Geometry.actual_scalarHessian_continuous line 2287
theorem OAI.PositiveEinsteinFour.Geometry.actual_scalarThird_continuous line 2293
def OAI.PositiveEinsteinFour.Geometry.twoFormChartValue line 2319
def OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth line 2325
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartValue_zero line 2331
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartValue_add line 2336
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartValue_smul line 2345
def OAI.PositiveEinsteinFour.Geometry.smoothTwoForms line 2353
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.hodge line 2368
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormHodge line 2380
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormHodge_involutive line 2391
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 2415) line 2415
theorem OAI.PositiveEinsteinFour.Geometry.orthogonalEuclidean_norm line 2421
def OAI.PositiveEinsteinFour.Geometry.orthogonalEuclideanIsometry line 2431
def OAI.PositiveEinsteinFour.Geometry.orthogonalDirection line 2449
def OAI.PositiveEinsteinFour.Geometry.orientedDirection line 2452
theorem OAI.PositiveEinsteinFour.Geometry.directionFrameMatrix_det line 2457
def OAI.PositiveEinsteinFour.Geometry.directionOrientedMatrix line 2465
theorem OAI.PositiveEinsteinFour.Geometry.continuous_directionOrientedMatrix line 2470
theorem OAI.PositiveEinsteinFour.Geometry.sum3_swap_first line 2500
theorem OAI.PositiveEinsteinFour.Geometry.sum3_swap_last line 2503
theorem OAI.PositiveEinsteinFour.Geometry.sum3_cycle line 2509
def OAI.PositiveEinsteinFour.Geometry.twoFormExteriorComponent line 2513
def OAI.PositiveEinsteinFour.Geometry.twoFormCodiffComponent line 2516
theorem OAI.PositiveEinsteinFour.Geometry.twoFormExterior_square_sum line 2519
def OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamQuadratic line 2566
theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamQuadratic_nonneg line 2570
theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamQuadratic_eq line 2575
theorem OAI.PositiveEinsteinFour.Geometry.chartGramMatrix_isUnit line 2615
theorem OAI.PositiveEinsteinFour.Geometry.fourMatrix_bijective line 2620
def OAI.PositiveEinsteinFour.Geometry.frozenFrameLinearEquiv line 2633
theorem OAI.PositiveEinsteinFour.Geometry.frozenFrameLinearEquiv_apply line 2638
theorem OAI.PositiveEinsteinFour.Geometry.frozenFrame_forward_bound line 2643
theorem OAI.PositiveEinsteinFour.Geometry.frozenFrame_inverse_bound line 2657
theorem OAI.PositiveEinsteinFour.Geometry.exists_frozenFrame_chart_lipschitz line 2695
Source documentation
The frozen orthonormal chart is locally Lipschitz with the sharp constant coming from the lower quadratic-form estimate.
```
theorem exists_frozenFrame_chart_lipschitz [T3Space M]
    (g : SmoothMetric M) (c : M) (δ : ℝ) (hδ : 0 < δ) (hδone : δ < 1) :
    let z₀ : ChartTarget c := ⟨chartAt FourSpace c c,
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ChartTarget
theorem OAI.PositiveEinsteinFour.Geometry.bool_orientation_change line 2748
def OAI.PositiveEinsteinFour.Geometry.orientationCoverPositiveFrames line 2760
theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_positive_in_chart line 2764
theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_positive_eventually line 2780
theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverPositiveFrames_clopen line 2820
theorem OAI.PositiveEinsteinFour.Geometry.reflected_frame_det line 2832
def OAI.PositiveEinsteinFour.Geometry.orientationCoverFrameOrientation line 2842
theorem OAI.PositiveEinsteinFour.Geometry.frame_matrix_ext line 2889
def OAI.PositiveEinsteinFour.Geometry.orientedFrameMap line 2899
theorem OAI.PositiveEinsteinFour.Geometry.continuous_orientedFrameMap line 2902
def OAI.PositiveEinsteinFour.Geometry.orientedFiberMeasure line 2906
instance OAI.PositiveEinsteinFour.Geometry.orientedFiberMeasure_probability line 2909
def OAI.PositiveEinsteinFour.Geometry.orientedFrameChange line 2914
theorem OAI.PositiveEinsteinFour.Geometry.orientedFrameMap_change line 2920
theorem OAI.PositiveEinsteinFour.Geometry.orientedFrameMap_mul line 2928
theorem OAI.PositiveEinsteinFour.Geometry.orientedFiberMeasure_eq line 2934
def OAI.PositiveEinsteinFour.Geometry.positiveFrameSection line 2967
theorem OAI.PositiveEinsteinFour.Geometry.measurable_positiveFrameSection line 2970
theorem OAI.PositiveEinsteinFour.Geometry.positiveFrameSection_base line 2974
theorem OAI.PositiveEinsteinFour.Geometry.positiveFrameSection_positive line 2978
def OAI.PositiveEinsteinFour.Geometry.orientedFrameParametrization line 2982
theorem OAI.PositiveEinsteinFour.Geometry.measurable_orientedFrameParametrization line 2986
theorem OAI.PositiveEinsteinFour.Geometry.orientedFrameParametrization_base line 2992
theorem OAI.PositiveEinsteinFour.Geometry.orientedFrameParametrization_positive line 2997
def OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure line 3008
instance OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure_probability line 3013
theorem OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure_supported line 3018
theorem OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure_base line 3024
theorem OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure_integral line 3035
theorem OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure_rotate line 3048
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_blockCoordinates line 3091
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_framedWeylDerivative line 3101
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeyl_parallel_derivative line 3121
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylGradient_parallel_derivative line 3131
theorem OAI.PositiveEinsteinFour.Geometry.actual_plusWeylHessian_parallel_derivative line 3140
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_framedScalarDerivative line 3149
theorem OAI.PositiveEinsteinFour.Geometry.actual_scalarValue_parallel_derivative line 3169
theorem OAI.PositiveEinsteinFour.Geometry.actual_scalarGradient_parallel_derivative line 3183
theorem OAI.PositiveEinsteinFour.Geometry.actual_scalarHessian_parallel_derivative line 3191
theorem OAI.PositiveEinsteinFour.Geometry.frameChartMatrix_reflection line 3219
theorem OAI.PositiveEinsteinFour.Geometry.reflection_parallel_rhs line 3231
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameCurveAt_reflection line 3266
Source documentation
The reflected curve follows the same horizontal direction when time is multiplied by the sign of the reflected frame axis.
```
theorem parallelFrameCurveAt_reflection (g : SmoothMetric M)
    (γ : ℝ → FrameBundle g) (k : Fin 4) (t : ℝ)
    (h : ParallelFrameCurveAt g γ k (orientationSign k * t)) :
    ParallelFrameCurveAt g
      (fun s => frameReflection (γ (orientationSign k * s))) k t := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.ParallelFrameCurveAt, OAI.PositiveEinsteinFour.Geometry.orientationSign, OAI.PositiveEinsteinFour.Geometry.frameReflection
abbrev OAI.PositiveEinsteinFour.Geometry.CoordinateFrameSpace line 3362
def OAI.PositiveEinsteinFour.Geometry.parallelFrameConnection line 3367
def OAI.PositiveEinsteinFour.Geometry.parallelFrameVectorField line 3372
Source documentation
Horizontal motion in the kth frame direction in a fixed chart.
```
def parallelFrameVectorField (g : SmoothMetric M) (c : M) (k : Fin 4)
    (p : CoordinateFrameSpace) : CoordinateFrameSpace :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CoordinateFrameSpace
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameVectorField_contDiffAt line 3376
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameVectorField_contDiffOn line 3407
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_matrix_mul_entry line 3412
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrame_metric_rate line 3422
theorem OAI.PositiveEinsteinFour.Geometry.parallelGram_rate_zero line 3435

theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_parallelGram_zero line 3442

Source documentation

The horizontal ODE preserves all inner products of frame columns.

theorem hasDerivAt_parallelGram_zero (g : SmoothMetric M) (c : M)
    (x : ℝ → FourSpace) (E : ℝ → Mat4) (t : ℝ) (k : Fin 4)
    (hz : x t ∈ (chartAt FourSpace c).target)
    (hx : HasDerivAt x (WithLp.toLp 2 (fun r => E t r k)) t)
    (hE : ∀ i j, HasDerivAt (fun s => E s i j)
      (-((∑ r, E t r k • connectionMatrix g c r (x t)) * E t) i j) t) :
    HasDerivAt (fun s => (E s)ᵀ * metricInChart g c (x s) * E s) 0 t := by
…

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

theorem OAI.PositiveEinsteinFour.Geometry.parallelGram_eq_on_interval line 3476

Source documentation

Along a local solution, one orthonormal initial frame remains orthonormal throughout its open interval of definition.

theorem parallelGram_eq_on_interval (g : SmoothMetric M) (c : M)
    (x : ℝ → FourSpace) (E : ℝ → Mat4) (k : Fin 4) (a b s t : ℝ)
    (hs : s ∈ Set.Ioo a b) (ht : t ∈ Set.Ioo a b)
    (hz : ∀ r ∈ Set.Ioo a b, x r ∈ (chartAt FourSpace c).target)
    (hx : ∀ r ∈ Set.Ioo a b,
      HasDerivAt x (WithLp.toLp 2 (fun i => E r i k)) r)
    (hE : ∀ r ∈ Set.Ioo a b, ∀ i j, HasDerivAt (fun u => E u i j)
      (-((∑ l, E r l k • connectionMatrix g c l (x r)) * E r) i j) r) :
    (E s)ᵀ * metricInChart g c (x s) * E s =
      (E t)ᵀ * metricInChart g c (x t) * E t := by
…

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

theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_two line 3509
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_trace_two line 3520
theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacian_eq_inverse_trace line 3536
def OAI.PositiveEinsteinFour.Geometry.scalarLaplacianBase line 3544
theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacian_eq_base line 3547
def OAI.PositiveEinsteinFour.Geometry.chartScalarLaplacian line 3553
theorem OAI.PositiveEinsteinFour.Geometry.chartScalarLaplacian_contDiffAt line 3556
theorem OAI.PositiveEinsteinFour.Geometry.chartScalarLaplacian_eq_base line 3572
theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacianBase_smooth line 3586
theorem OAI.PositiveEinsteinFour.Geometry.sphereCompletion_haar_preserving line 3623
Source documentation
Multiplication by a sphere-dependent orthogonal completion preserves the Haar marginal.
```
theorem sphereCompletion_haar_preserving :
    MeasurePreserving
      (fun p : Directions × OrientedOrthogonalFour => p.2 * directionOrientedMatrix p.1)
      (sphereMeasure.prod orientedFrameHaar) orientedFrameHaar := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrientedOrthogonalFour, OAI.PositiveEinsteinFour.Geometry.directionOrientedMatrix, OAI.PositiveEinsteinFour.Geometry.orientedFrameHaar
theorem OAI.PositiveEinsteinFour.Geometry.haar_integral_eq_sphere_of_rotation line 3640
Source documentation
An integrable Haar-fiber function whose rotated values depend only on the corresponding unit direction has the spherical average.
```
theorem haar_integral_eq_sphere_of_rotation
    (f : OrientedOrthogonalFour → ℝ) (G : Directions → ℝ)
    (hf : Integrable f orientedFrameHaar)
    (heq : ∀ P q, f (P * directionOrientedMatrix q) =
      G (orientedDirection P q)) :
    (∫ P, f P ∂orientedFrameHaar) = ∫ q, G q ∂sphereMeasure := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrientedOrthogonalFour, OAI.PositiveEinsteinFour.Geometry.orientedFrameHaar, OAI.PositiveEinsteinFour.Geometry.directionOrientedMatrix, OAI.PositiveEinsteinFour.Geometry.orientedDirection
theorem OAI.PositiveEinsteinFour.Geometry.sum_four_nonneg_zero line 3681
theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamQuadratic_eq_zero line 3685
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_rows_exterior_hodge line 3727
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_rows_deRham_hodge line 3736
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_positive_chart line 3764
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartValue_norm line 3786
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_chartVolumeDensity line 3814
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_parallelFrame_det line 3852

theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_parallel_density_det_zero line 3862

Source documentation

The metric density cancels the determinant rate of a parallel frame. This uses the coordinate ODE itself, without assuming a flow preserves a measure.

theorem hasDerivAt_parallel_density_det_zero (g : SmoothMetric M) (c : M)
    (x : ℝ → FourSpace) (E : ℝ → Mat4) (t : ℝ) (k : Fin 4)
    (hz : x t ∈ (chartAt FourSpace c).target)
    (hx : HasDerivAt x (WithLp.toLp 2 (fun r => E t r k)) t)
    (hE : ∀ i j, HasDerivAt (fun s => E s i j)
      (-((∑ r, E t r k • connectionMatrix g c r (x t)) * E t) i j) t) :
    HasDerivAt (fun s => chartVolumeDensity g c (x s) * (E s).det) 0 t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.chartVolumeDensity

theorem OAI.PositiveEinsteinFour.Geometry.frozenFrameLinearEquiv_det line 3896
theorem OAI.PositiveEinsteinFour.Geometry.frozenFrameLinearEquiv_symm_abs_det line 3902
theorem OAI.PositiveEinsteinFour.Geometry.volume_frozenFrame_symm_image line 3923
theorem OAI.PositiveEinsteinFour.Geometry.hausdorff_frozenFrame_symm_image line 3930
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_jacobi_mulVec line 3955
def OAI.PositiveEinsteinFour.Geometry.geodesicCovariantDerivative line 3970
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_jacobiConnection line 3975

theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_geodesicCovariantDerivative line 4016

Source documentation

The derivative of the covariant first derivative is computed from ordinary first and second variation data.

theorem hasDerivAt_geodesicCovariantDerivative (g : SmoothMetric M) (c : M)
    (x : ℝ → FourSpace) (v y w : ℝ → JacobiCoordinateVector)
    (a b : JacobiCoordinateVector) (t : ℝ)
    (hz : x t ∈ (chartAt FourSpace c).target)
    (hx : HasDerivAt x (WithLp.toLp 2 (v t)) t) (hv : HasDerivAt v a t)
    (hy : HasDerivAt y (w t) t) (hw : HasDerivAt w b t) :
    HasDerivAt (geodesicCovariantDerivative g c x v y w)
      (b + (jacobiConnectionDerivative
          (fun i j => matrixPartial (connectionMatrix g c j) i (x t)) (v t) (v t) +
        jacobiConnection (fun i => connectionMatrix g c i (x t)) a) *ᵥ y t +
        jacobiConnection (fun i => connectionMatrix g c i (x t)) (v t) *ᵥ w t) t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.geodesicCovariantDerivative, OAI.PositiveEinsteinFour.Geometry.jacobiConnectionDerivative, OAI.PositiveEinsteinFour.Geometry.matrixPartial, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.jacobiConnection

theorem OAI.PositiveEinsteinFour.Geometry.coordinate_geodesic_jacobi line 4034

Source documentation

A first variation satisfying the linearized geodesic ODE satisfies the covariant Jacobi equation, expressed through ordinary coordinate derivatives.

theorem coordinate_geodesic_jacobi (g : SmoothMetric M) (c : M)
    (x : ℝ → FourSpace) (v y w : ℝ → JacobiCoordinateVector)
    (a b : JacobiCoordinateVector) (t : ℝ)
    (hz : x t ∈ (chartAt FourSpace c).target)
    (hx : HasDerivAt x (WithLp.toLp 2 (v t)) t) (hv : HasDerivAt v a t)
    (hy : HasDerivAt y (w t) t) (hw : HasDerivAt w b t)
    (ha : a = -(jacobiConnection (fun i => connectionMatrix g c i (x t)) (v t) *ᵥ v t))
    (hb : b = -(jacobiConnectionDerivative
        (fun i j => matrixPartial (connectionMatrix g c j) i (x t)) (y t) (v t) *ᵥ v t) -
      jacobiConnection (fun i => connectionMatrix g c i (x t)) (w t) *ᵥ v t -
      jacobiConnection (fun i => connectionMatrix g c i (x t)) (v t) *ᵥ w t) :
    deriv (geodesicCovariantDerivative g c x v y w) t +
…

Mentions: OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.jacobiConnection, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.jacobiConnectionDerivative, OAI.PositiveEinsteinFour.Geometry.matrixPartial, OAI.PositiveEinsteinFour.Geometry.geodesicCovariantDerivative

abbrev OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameSpace line 4072
def OAI.PositiveEinsteinFour.Geometry.heatRadialFrameVelocity line 4077
def OAI.PositiveEinsteinFour.Geometry.heatRadialFrameConnection line 4080
def OAI.PositiveEinsteinFour.Geometry.heatRadialFrameField line 4084
theorem OAI.PositiveEinsteinFour.Geometry.heatRadialFrameField_contDiffAt line 4089
theorem OAI.PositiveEinsteinFour.Geometry.heatRadialFrameField_zero_direction line 4125
theorem OAI.PositiveEinsteinFour.Geometry.exists_frozenFrame_symm_lipschitz line 4150
theorem OAI.PositiveEinsteinFour.Geometry.frameChartMatrix_det_transition line 4200
def OAI.PositiveEinsteinFour.Geometry.orientationFrameClass line 4220
theorem OAI.PositiveEinsteinFour.Geometry.orientationFrameClass_proj line 4223
theorem OAI.PositiveEinsteinFour.Geometry.orientationFrameClass_local line 4226
theorem OAI.PositiveEinsteinFour.Geometry.continuous_orientationFrameClass line 4244
theorem OAI.PositiveEinsteinFour.Geometry.orientedFiberMeasure_eq_of_positive line 4297
theorem OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure_eq_section line 4312
Source documentation
Changing the measurable positive reference frame leaves the actual normalized frame probability unchanged.
```
theorem canonicalFrameMeasure_eq_section (g : SmoothMetric M) (o : FrameOrientation g)
    (s : M → FrameBundle g) (hs : Measurable s)
    (hbase : ∀ x, (s x).base = x) (hpos : ∀ x, s x ∈ o.positive) :
    canonicalFrameMeasure g o =
      Measure.map (fun p : M × OrientedOrthogonalFour =>
        (s p.1).rotate (orientedToOrthogonal p.2))
        ((normalizedVolume g).prod orientedFrameHaar) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.OrientedOrthogonalFour, OAI.PositiveEinsteinFour.Geometry.orientedToOrthogonal, OAI.PositiveEinsteinFour.Geometry.normalizedVolume, OAI.PositiveEinsteinFour.Geometry.orientedFrameHaar
theorem OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField_contDiffAt line 4362
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonianField_contDiffAt line 4375
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian_directional line 4380
theorem OAI.PositiveEinsteinFour.Geometry.inverseMetric_symm line 4428
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian_momentum_partial line 4434
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian_position_partial line 4456
theorem OAI.PositiveEinsteinFour.Geometry.inverse_metric_force line 4471
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian_force line 4482
theorem OAI.PositiveEinsteinFour.Geometry.parallel_momentum_algebra line 4496
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_frameCotangentMomentum line 4500
theorem OAI.PositiveEinsteinFour.Geometry.inverseMetric_frameMomentum line 4539
theorem OAI.PositiveEinsteinFour.Geometry.frameMomentum_force line 4550
theorem OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField_frame line 4566
Source documentation
The metric-lowered frame direction obeys the actual kinetic Hamiltonian field, with no energy-shell or normalization assumption.
```
theorem cotangentHamiltonianField_frame (g : SmoothMetric M) (c : M)
    (x : FourSpace) (hx : x ∈ (chartAt FourSpace c).target)
    (E : Mat4) (k : Fin 4) :
    cotangentHamiltonianField (kineticHamiltonian g c)
      (x, frameCotangentMomentum g c x E k) =
      (WithLp.toLp 2 (fun r => E r k),
        WithLp.toLp 2 ((parallelFrameConnection g c k (x, E))ᵀ *ᵥ
          WithLp.ofLp (frameCotangentMomentum g c x E k))) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField, OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian, OAI.PositiveEinsteinFour.Geometry.frameCotangentMomentum, OAI.PositiveEinsteinFour.Geometry.parallelFrameConnection

theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_parallelFrame_cotangentLift line 4589

Source documentation

A primitive parallel-frame curve has a cotangent lift satisfying Hamilton's equations for the actual metric Hamiltonian.

theorem hasDerivAt_parallelFrame_cotangentLift (g : SmoothMetric M) (c : M)
    (x : ℝ → FourSpace) (E : ℝ → Mat4) (t : ℝ) (k : Fin 4)
    (hz : x t ∈ (chartAt FourSpace c).target)
    (hx : HasDerivAt x (WithLp.toLp 2 (fun r => E t r k)) t)
    (hE : ∀ i j, HasDerivAt (fun s => E s i j)
      (-(parallelFrameConnection g c k (x t, E t) * E t) i j) t) :
    HasDerivAt (fun s => (x s, frameCotangentMomentum g c (x s) (E s) k))
      (cotangentHamiltonianField (kineticHamiltonian g c)
        (x t, frameCotangentMomentum g c (x t) (E t) k)) t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.parallelFrameConnection, OAI.PositiveEinsteinFour.Geometry.frameCotangentMomentum, OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField, OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian

theorem OAI.PositiveEinsteinFour.Geometry.exists_local_parallelFrame_curve line 4621
def OAI.PositiveEinsteinFour.Geometry.chartMatrixFrame line 4669
Source documentation
A matrix normalized by the chart metric gives an actual orthonormal frame, after applying the inverse-chart tangent map.
```
def chartMatrixFrame (g : SmoothMetric M) (c : M) (z : ChartTarget c)
    (E : Mat4) (hE : Eᵀ * metricInChart g c z * E = 1) :
    OrthonormalFrame g ((chartAt FourSpace c).symm z) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ChartTarget, OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame
theorem OAI.PositiveEinsteinFour.Geometry.exists_local_orthonormalFrame_curve line 4682
abbrev OAI.PositiveEinsteinFour.Geometry.ParallelFrameVariationSpace line 4724
def OAI.PositiveEinsteinFour.Geometry.parallelFrameVariationalField line 4730
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameVariationalField_contDiffAt line 4735

theorem OAI.PositiveEinsteinFour.Geometry.exists_local_parallelFrame_variation line 4749

Source documentation

A genuine local solution of the variational ODE with identity initial linear map. Identifying this linear map with the derivative in initial conditions is a separate estimate.

theorem exists_local_parallelFrame_variation (g : SmoothMetric M) (c : M)
    (k : Fin 4) (p : CoordinateFrameSpace)
    (hp : p.1 ∈ (chartAt FourSpace c).target) :
    ∃ ε > (0 : ℝ), ∃ x : ℝ → CoordinateFrameSpace,
      ∃ V : ℝ → CoordinateFrameSpace →L[ℝ] CoordinateFrameSpace,
        x 0 = p ∧ V 0 = ContinuousLinearMap.id ℝ CoordinateFrameSpace ∧
        ∀ t ∈ Ioo (-ε) ε,
          (x t).1 ∈ (chartAt FourSpace c).target ∧
          HasDerivAt x (parallelFrameVectorField g c k (x t)) t ∧
          HasDerivAt V ((fderiv ℝ (parallelFrameVectorField g c k) (x t)).comp (V t)) t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.CoordinateFrameSpace, OAI.PositiveEinsteinFour.Geometry.parallelFrameVectorField

theorem OAI.PositiveEinsteinFour.Geometry.parallelFrame_variation_remainder_derivative line 4774

Source documentation

Exact remainder equation used to compare the true nearby trajectory with the candidate first variation.

theorem parallelFrame_variation_remainder_derivative (g : SmoothMetric M) (c : M)
    (k : Fin 4) (x y : ℝ → CoordinateFrameSpace)
    (V : ℝ → CoordinateFrameSpace →L[ℝ] CoordinateFrameSpace)
    (h : CoordinateFrameSpace) (t : ℝ)
    (hx : HasDerivAt x (parallelFrameVectorField g c k (x t)) t)
    (hy : HasDerivAt y (parallelFrameVectorField g c k (y t)) t)
    (hV : HasDerivAt V
      ((fderiv ℝ (parallelFrameVectorField g c k) (x t)).comp (V t)) t) :
    HasDerivAt (fun s => y s - x s - V s h)
      ((fderiv ℝ (parallelFrameVectorField g c k) (x t)) (y t - x t - V t h) +
        (parallelFrameVectorField g c k (y t) - parallelFrameVectorField g c k (x t) -
          (fderiv ℝ (parallelFrameVectorField g c k) (x t)) (y t - x t))) t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.CoordinateFrameSpace, OAI.PositiveEinsteinFour.Geometry.parallelFrameVectorField

structure OAI.PositiveEinsteinFour.Geometry.ParallelMetricData line 4816
Source documentation
Only raw flow, parallel differentiation and normalized Ricci data remain in the classical frame-calculus input.
```
structure ParallelMetricData (g : SmoothMetric M) (μ : Measure (FrameBundle g)) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle
theorem OAI.PositiveEinsteinFour.Geometry.ParallelMetricData.continuousWeyl line 4827
theorem OAI.PositiveEinsteinFour.Geometry.ParallelMetricData.continuousGradient line 4831
theorem OAI.PositiveEinsteinFour.Geometry.ParallelMetricData.continuousHessian line 4835
theorem OAI.PositiveEinsteinFour.Geometry.ParallelMetricData.continuousThird line 4839
theorem OAI.PositiveEinsteinFour.Geometry.ParallelMetricData.curve_continuous line 4843
theorem OAI.PositiveEinsteinFour.Geometry.ParallelMetricData.derivativeWeyl line 4847
theorem OAI.PositiveEinsteinFour.Geometry.ParallelMetricData.derivativeGradient line 4854
theorem OAI.PositiveEinsteinFour.Geometry.ParallelMetricData.derivativeHessian line 4861
theorem OAI.PositiveEinsteinFour.Geometry.ParallelMetricData.ricciThree line 4868
def OAI.PositiveEinsteinFour.Geometry.ParallelMetricData.toMetricGreenData line 4872
Source documentation
Metric differential identities give the tensor-identity structure.
```
def toMetricGreenData (d : ParallelMetricData g μ) : MetricGreenData g μ where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.MetricGreenData
theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_finite_contDiffAt line 4911
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_derivative_contDiffAt line 4927
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_derivative_transition line 4941
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_framed_continuous line 4958
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_gradient_continuous line 4968
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_hessian_continuous line 4974
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_parallel_derivative line 4980
theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinate_gradient line 5020
theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinate_hessian line 5027
theorem OAI.PositiveEinsteinFour.Geometry.chartGramMatrix_mul_transpose line 5045
theorem OAI.PositiveEinsteinFour.Geometry.chartScalarLaplacian_coefficients line 5059
theorem OAI.PositiveEinsteinFour.Geometry.scalarPrincipalCoefficients_posDef line 5069
theorem OAI.PositiveEinsteinFour.Geometry.scalarPrincipalCoefficients_smooth line 5074
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.continuous_norm line 5099
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_norm_continuous line 5113
theorem OAI.PositiveEinsteinFour.Geometry.orientedDirection_mul line 5134
theorem OAI.PositiveEinsteinFour.Geometry.orientedDirection_completion line 5144
theorem OAI.PositiveEinsteinFour.Geometry.continuous_orientedDirection line 5152
theorem OAI.PositiveEinsteinFour.Geometry.haar_integral_direction line 5172
Source documentation
Haar averaging of the orbit of any direction gives the fixed spherical probability, independently of the starting direction.
```
theorem haar_integral_direction (f : Directions → ℝ) (hf : Continuous f) (q : Directions) :
    (∫ P, f (orientedDirection P q) ∂orientedFrameHaar) = ∫ r, f r ∂sphereMeasure := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.orientedDirection, OAI.PositiveEinsteinFour.Geometry.orientedFrameHaar
theorem OAI.PositiveEinsteinFour.Geometry.sphereMeasure_unique line 5204
Source documentation
Every probability invariant under the actual SO(4) action agrees with the normalized Hausdorff measure on the unit three-sphere.
```
theorem sphereMeasure_unique (μ : Measure Directions) [IsProbabilityMeasure μ]
    (hμ : ∀ P, MeasurePreserving (orientedDirection P) μ μ) : μ = sphereMeasure := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.orientedDirection
def OAI.PositiveEinsteinFour.Geometry.twoFormTensorLinear line 5245
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.eq_of_matrix_eq line 5257
def OAI.PositiveEinsteinFour.Geometry.twoFormTensorAt line 5264
def OAI.PositiveEinsteinFour.Geometry.twoFormCoordinates line 5268
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartValue_tensor line 5273
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoordinates_from_chart line 5283
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_positive_chart_at line 5293
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.coordinates_contDiffAt line 5323
theorem OAI.PositiveEinsteinFour.Geometry.sum_two_indices line 5367
theorem OAI.PositiveEinsteinFour.Geometry.sum_four_indices line 5373
Distinct definitions of this name: OAI/Geometry/EinsteinFour/CurvatureForm.lean:26 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.sum_four_indices@path.
def OAI.PositiveEinsteinFour.Geometry.twoTensorProduct line 5379
def OAI.PositiveEinsteinFour.Geometry.twoTensorContraction line 5382
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_twoProduct line 5385
theorem OAI.PositiveEinsteinFour.Geometry.twoTensorContraction_pairing line 5398
theorem OAI.PositiveEinsteinFour.Geometry.frameTensorPairing_ext line 5409
theorem OAI.PositiveEinsteinFour.Geometry.twoTensorContraction_frame line 5415

theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_parallel_frameVector line 5455

Source documentation

Multiplication by a parallel frame converts ordinary component derivatives into covariant derivatives along the curve.

theorem hasDerivAt_parallel_frameVector (E : ℝ → Mat4)
    (y : ℝ → JacobiCoordinateVector) (U : Mat4) (y' : JacobiCoordinateVector)
    (t : ℝ) (hE : ∀ i j, HasDerivAt (fun s => E s i j) (-(U * E t) i j) t)
    (hy : HasDerivAt y y' t) :
    HasDerivAt (fun s => E s *ᵥ y s)
      (E t *ᵥ y' - U *ᵥ (E t *ᵥ y t)) t := by
…

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

theorem OAI.PositiveEinsteinFour.Geometry.parallel_frame_covariant_derivative line 5474
theorem OAI.PositiveEinsteinFour.Geometry.parallel_frame_covariant_second_derivative line 5486
Source documentation
The same cancellation applies to the first covariant derivative. Thus the second covariant derivative is the ordinary second derivative of the components in a parallel frame.
```
theorem parallel_frame_covariant_second_derivative (E : ℝ → Mat4)
    (F z : ℝ → JacobiCoordinateVector) (U : Mat4) (z' : JacobiCoordinateVector)
    (t : ℝ) (hE : ∀ i j, HasDerivAt (fun s => E s i j) (-(U * E t) i j) t)
    (hz : HasDerivAt z z' t) (hF : F =ᶠ[𝓝 t] fun s => E s *ᵥ z s) :
    deriv F t + U *ᵥ F t = E t *ᵥ z' := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector
def OAI.PositiveEinsteinFour.Geometry.jacobiCurvatureCombination line 5495
def OAI.PositiveEinsteinFour.Geometry.curvatureFirstLinear line 5498
theorem OAI.PositiveEinsteinFour.Geometry.jacobi_mulVec_sum line 5508
theorem OAI.PositiveEinsteinFour.Geometry.jacobiCurvatureCombination_frame line 5516
theorem OAI.PositiveEinsteinFour.Geometry.actual_jacobiCurvatureCombination_frame line 5532
theorem OAI.PositiveEinsteinFour.Geometry.actual_normal_jacobi_curvature line 5541
theorem OAI.PositiveEinsteinFour.Geometry.actual_normal_jacobi_equation line 5587
def OAI.PositiveEinsteinFour.Geometry.geodesicCoordinateField line 5621
def OAI.PositiveEinsteinFour.Geometry.geodesicVariationAcceleration line 5626
theorem OAI.PositiveEinsteinFour.Geometry.geodesicCoordinateField_contDiffAt line 5636
theorem OAI.PositiveEinsteinFour.Geometry.connection_variation_derivative line 5659
theorem OAI.PositiveEinsteinFour.Geometry.geodesicCoordinateField_curve_derivative line 5702
theorem OAI.PositiveEinsteinFour.Geometry.geodesicCoordinateField_fderiv line 5736

theorem OAI.PositiveEinsteinFour.Geometry.geodesic_variation_derivatives line 5758

Source documentation

The variational equation of the actual tangent vector field gives the two ordinary derivative inputs of the coordinate Jacobi theorem.

theorem geodesic_variation_derivatives (g : SmoothMetric M) (c : M)
    (γ Z : ℝ → FourSpace × FourSpace) (t : ℝ)
    (hz : (γ t).1 ∈ (chartAt FourSpace c).target)
    (hZ : HasDerivAt Z (fderiv ℝ (geodesicCoordinateField g c) (γ t) (Z t)) t) :
    HasDerivAt (fun s => (Z s).1) (Z t).2 t ∧
      HasDerivAt (fun s => (Z s).2)
        (geodesicVariationAcceleration g c (γ t).1 (γ t).2 (Z t).1 (Z t).2) t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.geodesicCoordinateField, OAI.PositiveEinsteinFour.Geometry.geodesicVariationAcceleration

def OAI.PositiveEinsteinFour.Geometry.geodesicVariationCovariantDerivative line 5768
theorem OAI.PositiveEinsteinFour.Geometry.geodesic_variation_covariant_differentiableAt line 5774

theorem OAI.PositiveEinsteinFour.Geometry.geodesic_variation_jacobi line 5800

Source documentation

A true first variation of the actual coordinate geodesic field satisfies the curvature Jacobi equation.

theorem geodesic_variation_jacobi (g : SmoothMetric M) (c : M)
    (γ Z : ℝ → FourSpace × FourSpace) (t : ℝ)
    (hz : (γ t).1 ∈ (chartAt FourSpace c).target)
    (hγ : HasDerivAt γ (geodesicCoordinateField g c (γ t)) t)
    (hZ : HasDerivAt Z (fderiv ℝ (geodesicCoordinateField g c) (γ t) (Z t)) t) :
    deriv (geodesicVariationCovariantDerivative g c γ Z) t +
      jacobiConnection (fun i => connectionMatrix g c i (γ t).1)
        (WithLp.ofLp (γ t).2) *ᵥ geodesicVariationCovariantDerivative g c γ Z t +
      (∑ i, ∑ j, ((Z t).1 i * (γ t).2 j) •
        coordinateCurvatureMatrix g c i j (γ t).1) *ᵥ WithLp.ofLp (γ t).2 = 0 := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.geodesicCoordinateField, OAI.PositiveEinsteinFour.Geometry.geodesicVariationCovariantDerivative, OAI.PositiveEinsteinFour.Geometry.jacobiConnection, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.coordinateCurvatureMatrix

theorem OAI.PositiveEinsteinFour.Geometry.weightedMetricSecond_identity line 5851
def OAI.PositiveEinsteinFour.Geometry.jacobiMetricFirstDirectional line 5887
def OAI.PositiveEinsteinFour.Geometry.jacobiMetricSecondDirectional line 5891
theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricFirstDirectional_eq line 5895
theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricSecondDirectional_eq line 5902
theorem OAI.PositiveEinsteinFour.Geometry.actual_jacobiCurvature_metric_skew line 5919
theorem OAI.PositiveEinsteinFour.Geometry.actual_coordinateEnergySecondDensity line 5938
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_metricPair line 5958
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_connection_weighted line 5983
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_matrix_vector line 6021

theorem OAI.PositiveEinsteinFour.Geometry.actual_coordinateEnergyBoundary_hasDerivAt line 6035

Source documentation

The boundary correction is the derivative of an actual scalar along a coordinate geodesic. Its vanishing at zero variation endpoints can therefore be used by the ordinary fundamental theorem of calculus.

theorem actual_coordinateEnergyBoundary_hasDerivAt (g : SmoothMetric M) (c : M)
    (x : ℝ → FourSpace) (v y : ℝ → JacobiCoordinateVector)
    (a w : JacobiCoordinateVector) (t : ℝ)
    (hz : x t ∈ (chartAt FourSpace c).target)
    (hx : HasDerivAt x (WithLp.toLp 2 (v t)) t)
    (hv : HasDerivAt v a t) (hy : HasDerivAt y w t)
    (ha : a = -(jacobiConnection (fun i => connectionMatrix g c i (x t)) (v t) *ᵥ v t)) :
    HasDerivAt
      (fun s => jacobiMetricPair (metricInChart g c (x s)) (v s)
        (jacobiConnection (fun i => connectionMatrix g c i (x s)) (y s) *ᵥ y s))
      (coordinateEnergyBoundaryRate (metricInChart g c (x t))
        (fun i => connectionMatrix g c i (x t))
…

Mentions: OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.jacobiConnection, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair, OAI.PositiveEinsteinFour.Geometry.coordinateEnergyBoundaryRate

structure OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow line 6106
Source documentation
A constructed local solution and its first variation. This is output of the local ODE theorem, not a geometric input.
```
structure KineticLocalFlow (g : SmoothMetric M) (c : M) (p : CotangentCoordinates) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates
theorem OAI.PositiveEinsteinFour.Geometry.exists_kineticLocalFlow line 6132
def OAI.PositiveEinsteinFour.Geometry.kineticVariationMatrix line 6181
theorem OAI.PositiveEinsteinFour.Geometry.kineticVariationMatrix_derivative line 6185
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.initial_derivative line 6217
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.energy line 6229
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.jacobian_det line 6245
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.eq_on line 6277
Source documentation
Uniqueness against any other actual kinetic trajectory on the common interval, including cotangent lifts of the global frame flow.
```
theorem eq_on (F : KineticLocalFlow g c p)
    (q : CotangentCoordinates) (hq : q ∈ Metric.ball p F.radius)
    (γ : ℝ → CotangentCoordinates) (hγ0 : γ 0 = q)
    (hγ : ∀ t ∈ Ioo (-F.time) F.time,
      HasDerivAt γ (cotangentHamiltonianField (kineticHamiltonian g c) (γ t)) t) :
    EqOn (fun s => F.map (q, s)) γ (Ioo (-F.time) F.time) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow, OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField, OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.injective_slice line 6317
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.map_volume line 6356
Source documentation
The local flow of the actual kinetic Hamiltonian preserves coordinate volume on its initial ball. No preservation assumption is used.
```
theorem map_volume (F : KineticLocalFlow g c p)
    (t : ℝ) (ht : t ∈ Ioo (-F.time) F.time) :
    Measure.map (fun q => F.map (q, t)) (volume.restrict (Metric.ball p F.radius)) =
      volume.restrict ((fun q => F.map (q, t)) '' Metric.ball p F.radius) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow
structure OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow line 6385
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatRadialFrameFlow line 6399
def OAI.PositiveEinsteinFour.Geometry.kineticMomentumScale line 6458
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian_scale line 6461
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonianField_scale line 6471

theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_kineticMomentumScale line 6499

Source documentation

The radial extension of a unit-energy trajectory is an actual kinetic trajectory, with the expected rescaling of its time parameter.

theorem hasDerivAt_kineticMomentumScale (g : SmoothMetric M) (c : M)
    (γ : ℝ → CotangentCoordinates) (r t : ℝ)
    (hz : (γ (r * t)).1 ∈ (chartAt FourSpace c).target)
    (hγ : HasDerivAt γ
      (cotangentHamiltonianField (kineticHamiltonian g c) (γ (r * t))) (r * t)) :
    HasDerivAt (fun s => kineticMomentumScale r (γ (r * s)))
      (cotangentHamiltonianField (kineticHamiltonian g c)
        (kineticMomentumScale r (γ (r * t)))) t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField, OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian, OAI.PositiveEinsteinFour.Geometry.kineticMomentumScale

theorem OAI.PositiveEinsteinFour.Geometry.exists_frozenFrame_chart_lipschitz_at line 6543
theorem OAI.PositiveEinsteinFour.Geometry.matrixVector_norm_sq line 6597
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.integratedWeylEquation line 6607
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousMinusWeyl line 6692
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousMinusGradient line 6697
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.minusWeyl_reflected_flow line 6710
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.minusGradient_reflected_flow line 6718
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.derivativeMinusWeyl line 6728
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.oppositeData line 6747
theorem OAI.PositiveEinsteinFour.Geometry.frame_reflect_det line 6778
theorem OAI.PositiveEinsteinFour.Geometry.orientationFrameClass_fiber_surjective line 6787
theorem OAI.PositiveEinsteinFour.Geometry.frame_sign_eq_iff line 6802
def OAI.PositiveEinsteinFour.Geometry.frameOrientation_of_clopen_sheet line 6815
theorem OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure_apply_base_inter line 6873
Source documentation
Disintegration on a measurable base set using any positive reference frame over that set. In particular, a local smooth frame may be used without extending its positivity or its base identity to the whole manifold.
```
theorem canonicalFrameMeasure_apply_base_inter (g : SmoothMetric M)
    (o : FrameOrientation g) (U : Set M) (hU : MeasurableSet U)
    (s : M → FrameBundle g)
    (hbase : ∀ x ∈ U, (s x).base = x)
    (hpos : ∀ x ∈ U, s x ∈ o.positive)
    (A : Set (FrameBundle g)) (hA : MeasurableSet A) :
    canonicalFrameMeasure g o (FrameBundle.base ⁻¹' U ∩ A) =
      ∫⁻ x in U, orientedFiberMeasure (s x).frame A ∂normalizedVolume g := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.orientedFiberMeasure, OAI.PositiveEinsteinFour.Geometry.normalizedVolume
abbrev OAI.PositiveEinsteinFour.Geometry.OrthonormalChartState line 6935
def OAI.PositiveEinsteinFour.Geometry.chartFrameStateToBundle line 6939
theorem OAI.PositiveEinsteinFour.Geometry.frameChartMatrix_apply line 6944
theorem OAI.PositiveEinsteinFour.Geometry.frameChartMatrix_vector line 6957
theorem OAI.PositiveEinsteinFour.Geometry.chartTransitionMatrix_mulVec line 6965
theorem OAI.PositiveEinsteinFour.Geometry.frameChartMatrix_change line 6977
theorem OAI.PositiveEinsteinFour.Geometry.chartMatrixFrame_vector line 7006
theorem OAI.PositiveEinsteinFour.Geometry.frameChartMatrix_chartFrameState line 7029
theorem OAI.PositiveEinsteinFour.Geometry.chartFrameState_coordinate line 7044
theorem OAI.PositiveEinsteinFour.Geometry.continuous_chartFrameStateToBundle line 7049
theorem OAI.PositiveEinsteinFour.Geometry.frameChartMatrix_normalizes line 7086
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrame_taylor_remainder_le line 7136

theorem OAI.PositiveEinsteinFour.Geometry.exists_parallelFrame_taylor_neighborhood line 7150

Source documentation

Around each valid chart state the actual vector field is Lipschitz, and its first-order remainder has a uniform quadratic bound.

theorem exists_parallelFrame_taylor_neighborhood (g : SmoothMetric M) (c : M)
    (k : Fin 4) (p : CoordinateFrameSpace)
    (hp : p.1 ∈ (chartAt FourSpace c).target) :
    ∃ r > (0 : ℝ), ∃ K L : ℝ≥0,
      LipschitzOnWith K (parallelFrameVectorField g c k) (ball p r) ∧
      LipschitzOnWith L (fderiv ℝ (parallelFrameVectorField g c k)) (ball p r) ∧
      ∀ x ∈ ball p r, ∀ y ∈ ball p r,
        ‖parallelFrameVectorField g c k y - parallelFrameVectorField g c k x -
          (fderiv ℝ (parallelFrameVectorField g c k) x) (y - x)‖ ≤
            (L : ℝ) * ‖y - x‖ ^ 2 := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.CoordinateFrameSpace, OAI.PositiveEinsteinFour.Geometry.parallelFrameVectorField

theorem OAI.PositiveEinsteinFour.Geometry.exists_continuous_local_parallelFrame_flow line 7197
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrame_solution_unique_near line 7283
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrame_solution_unique_interval line 7298
abbrev OAI.PositiveEinsteinFour.Geometry.EuclideanUnitSphere line 7346
def OAI.PositiveEinsteinFour.Geometry.sphereToDirection line 7348
def OAI.PositiveEinsteinFour.Geometry.euclideanSphereIsometry line 7355
theorem OAI.PositiveEinsteinFour.Geometry.sphere_cone_preimage line 7365
theorem OAI.PositiveEinsteinFour.Geometry.euclideanSphere_measurePreserving line 7381
Source documentation
Orthogonal maps preserve the angular measure supplied by the polar decomposition of Euclidean volume.
```
theorem euclideanSphere_measurePreserving (e : FourSpace ≃ₗᵢ[ℝ] FourSpace) :
    MeasurePreserving (euclideanSphereIsometry e)
      (volume : Measure FourSpace).toSphere (volume : Measure FourSpace).toSphere := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.euclideanSphereIsometry
def OAI.PositiveEinsteinFour.Geometry.polarAngularProbability line 7392
instance OAI.PositiveEinsteinFour.Geometry.polarAngularProbability_probability line 7395
def OAI.PositiveEinsteinFour.Geometry.polarDirectionProbability line 7401
instance OAI.PositiveEinsteinFour.Geometry.polarDirectionProbability_probability line 7404
theorem OAI.PositiveEinsteinFour.Geometry.polarDirectionProbability_eq_sphereMeasure line 7408
theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinates_contDiffAt line 7447
theorem OAI.PositiveEinsteinFour.Geometry.actual_scalarHessian_symmetric line 7454
theorem OAI.PositiveEinsteinFour.Geometry.actual_scalarThird_commutator line 7471
structure OAI.PositiveEinsteinFour.Geometry.ScalarParallelData line 7508
Source documentation
Only differentiation along the chosen parallel flow remains input. Regularity, symmetry and the Ricci commutator follow from the metric.
```
structure ScalarParallelData {μ : MeasureTheory.Measure (FrameBundle g)}
    (d : MetricGreenData g μ) (a : M → ℝ) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.MetricGreenData
theorem OAI.PositiveEinsteinFour.Geometry.ScalarParallelData.toCovariantData line 7519
def OAI.PositiveEinsteinFour.Geometry.ParallelScalarCalculusInput line 7532
theorem OAI.PositiveEinsteinFour.Geometry.ParallelScalarCalculusInput.toPetersenInput line 7536
theorem OAI.PositiveEinsteinFour.Geometry.ParallelMetricData.scalarCalculus line 7544
Source documentation
Primitive parallel-frame equations supply the full scalar calculus.
```
theorem ParallelMetricData.scalarCalculus {μ : MeasureTheory.Measure (FrameBundle g)}
    (d : ParallelMetricData g μ) : ParallelScalarCalculusInput d.toMetricGreenData := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.ParallelScalarCalculusInput
def OAI.PositiveEinsteinFour.Geometry.frozenScalarPrincipal line 7578
theorem OAI.PositiveEinsteinFour.Geometry.frozenScalarPrincipal_self line 7581
theorem OAI.PositiveEinsteinFour.Geometry.frozenScalarPrincipal_continuousAt line 7585
theorem OAI.PositiveEinsteinFour.Geometry.frozenScalarPrincipal_entry_near line 7594
theorem OAI.PositiveEinsteinFour.Geometry.frozenScalarPrincipal_near_identity line 7610
theorem OAI.PositiveEinsteinFour.Geometry.frozenScalarPrincipal_elliptic line 7621
theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacianBase_coordinate_formula line 7649
theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacianBase_congr_nhds line 7661
theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacianBase_zero line 7690
theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacianBase_tsupport line 7696
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_pairing_continuous line 7729
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner line 7748
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_pairing_integrable line 7751
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner_comm line 7757
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner_add line 7764
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner_smul line 7771
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner_self line 7778
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner_nonneg line 7783
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner_definite line 7787
theorem OAI.PositiveEinsteinFour.Geometry.continuous_haar_sphere_orbit line 7815
theorem OAI.PositiveEinsteinFour.Geometry.sphereMeasure_eq_haar_orbit line 7824
theorem OAI.PositiveEinsteinFour.Geometry.sphereMeasure_openPos line 7837
theorem OAI.PositiveEinsteinFour.Geometry.chartInverseMatrix_transition line 7862
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoordinates_transition line 7891
def OAI.PositiveEinsteinFour.Geometry.twoFormCovariantCoordinates line 7902
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.covariant_contDiffAt line 7906
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.covariant_transition line 7913
def OAI.PositiveEinsteinFour.Geometry.twoFormFramedCovariantDerivative line 7926
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.continuous_framedCovariantDerivative line 7931
def OAI.PositiveEinsteinFour.Geometry.twoTensorContractionLinear line 7956
def OAI.PositiveEinsteinFour.Geometry.twoTensorMatrixLinear line 7968
def OAI.PositiveEinsteinFour.Geometry.twoFormExtractLinear line 7973
def OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureLinear line 7978
def OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureAction line 7982
theorem OAI.PositiveEinsteinFour.Geometry.twoFormTensor_injective line 7985
theorem OAI.PositiveEinsteinFour.Geometry.twoFormTensor_curvature line 7991
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureAction_frame line 8017
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_regularity_cutoff line 8050
theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_preconnected_of_not_orientable line 8094
theorem OAI.PositiveEinsteinFour.Geometry.actual_hatcherOrientationCoverInput line 8108
def OAI.PositiveEinsteinFour.Geometry.polarAngularMass line 8145
theorem OAI.PositiveEinsteinFour.Geometry.polarAngularMass_ne_zero line 8147
theorem OAI.PositiveEinsteinFour.Geometry.polarAngularMass_ne_top line 8150
theorem OAI.PositiveEinsteinFour.Geometry.polarAngularMass_pos line 8152
theorem OAI.PositiveEinsteinFour.Geometry.polarAngularMass_eq_ball line 8155
theorem OAI.PositiveEinsteinFour.Geometry.map_euclidean_angular_measure line 8160
def OAI.PositiveEinsteinFour.Geometry.euclideanPolarCoordinates line 8173
theorem OAI.PositiveEinsteinFour.Geometry.euclideanPolarCoordinates_measurePreserving line 8179
Source documentation
Euclidean volume decomposes into spherical probability and the cubic radial density, with its fixed positive angular factor.
```
theorem euclideanPolarCoordinates_measurePreserving :
    MeasurePreserving euclideanPolarCoordinates
      ((volume : Measure FourSpace).comap Subtype.val)
      ((polarAngularMass • sphereMeasure).prod (Measure.volumeIoiPow 3)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.euclideanPolarCoordinates, OAI.PositiveEinsteinFour.Geometry.polarAngularMass
theorem OAI.PositiveEinsteinFour.Geometry.continuous_gradientSquareNorm line 8221
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.weylCubic_integrable line 8233
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.weylGradientEnergy_le line 8247
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.reflected_gradientSquareNorm line 8258
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.oppositeWeylGradientEnergy_le line 8269
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.totalWeylGradientEnergy_le line 8281
theorem OAI.PositiveEinsteinFour.Geometry.jacobi_det_differentiableAt line 8324
theorem OAI.PositiveEinsteinFour.Geometry.jacobi_inverse_differentiableAt line 8339
def OAI.PositiveEinsteinFour.Geometry.inverseFrameComponents line 8357
theorem OAI.PositiveEinsteinFour.Geometry.inverseFrameComponents_mul line 8360
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_inverseFrameComponents line 8368
Source documentation
In a parallel frame, ordinary component differentiation is the inverse-frame image of covariant differentiation.
```
theorem hasDerivAt_inverseFrameComponents (E : ℝ → Mat4)
    (Y : ℝ → JacobiCoordinateVector) (U : Mat4) (Y' : JacobiCoordinateVector)
    (t : ℝ) (hE : ∀ i j, HasDerivAt (fun s => E s i j) (-(U * E t) i j) t)
    (hY : HasDerivAt Y Y' t) (hdet : (E t).det ≠ 0) :
    HasDerivAt (inverseFrameComponents E Y)
      ((E t)⁻¹ *ᵥ (Y' + U *ᵥ Y t)) t := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.inverseFrameComponents

theorem OAI.PositiveEinsteinFour.Geometry.inverseFrameComponents_covariant_pair line 8401

Source documentation

Derivatives of the position and covariant-velocity components.

theorem inverseFrameComponents_covariant_pair (E : ℝ → Mat4)
    (Y F : ℝ → JacobiCoordinateVector) (U : Mat4)
    (Y' F' : JacobiCoordinateVector) (t : ℝ)
    (hE : ∀ i j, HasDerivAt (fun s => E s i j) (-(U * E t) i j) t)
    (hY : HasDerivAt Y Y' t) (hF : HasDerivAt F F' t)
    (hFvalue : F t = Y' + U *ᵥ Y t) (hdet : (E t).det ≠ 0) :
    HasDerivAt (inverseFrameComponents E Y) (inverseFrameComponents E F t) t ∧
      HasDerivAt (inverseFrameComponents E F)
        ((E t)⁻¹ *ᵥ (F' + U *ᵥ F t)) t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.inverseFrameComponents

theorem OAI.PositiveEinsteinFour.Geometry.energyPair_hasDerivAt line 8431
theorem OAI.PositiveEinsteinFour.Geometry.matrixEnergy_secondDerivative line 8456
def OAI.PositiveEinsteinFour.Geometry.straightChartVariationEnergy line 8497
theorem OAI.PositiveEinsteinFour.Geometry.straightChartVariationEnergy_secondDerivative line 8502
theorem OAI.PositiveEinsteinFour.Geometry.straightChartVariationEnergy_index_formula line 8561
theorem OAI.PositiveEinsteinFour.Geometry.matrixEnergy_secondJet line 8572

theorem OAI.PositiveEinsteinFour.Geometry.actual_metricEnergy_secondJet line 8606

Source documentation

The second derivative for an arbitrary two-jet of the position and velocity. The hypotheses are ordinary parameter derivatives of these data.

theorem actual_metricEnergy_secondJet (g : SmoothMetric M) (c : M)
    (x : ℝ → FourSpace) (y v w : ℝ → JacobiCoordinateVector)
    (u q : JacobiCoordinateVector) (hz : x 0 ∈ (chartAt FourSpace c).target)
    (hx : ∀ᶠ s in 𝓝 (0 : ℝ), HasDerivAt x (WithLp.toLp 2 (y s)) s)
    (hy : HasDerivAt y u 0)
    (hv : ∀ᶠ s in 𝓝 (0 : ℝ), HasDerivAt v (w s) s) (hw : HasDerivAt w q 0) :
    HasDerivAt (deriv (fun s : ℝ => (1 / 2 : ℝ) *
      jacobiMetricPair (metricInChart g c (x s)) (v s) (v s)))
      (coordinateEnergySecondDensity (metricInChart g c (x 0))
        (jacobiMetricFirstDirectional g c (x 0) (y 0))
        (jacobiMetricSecondDirectional g c (x 0) (y 0)) (v 0) (w 0) +
        (1 / 2 : ℝ) * jacobiMetricPair (jacobiMetricFirstDirectional g c (x 0) u) (v 0) (v 0) +
…

Mentions: OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair, OAI.PositiveEinsteinFour.Geometry.coordinateEnergySecondDensity, OAI.PositiveEinsteinFour.Geometry.jacobiMetricFirstDirectional, OAI.PositiveEinsteinFour.Geometry.jacobiMetricSecondDirectional

theorem OAI.PositiveEinsteinFour.Geometry.actual_metricEnergy_jetBoundary_hasDerivAt line 8680

Source documentation

The second-jet correction is itself a boundary derivative along a geodesic; together with the straight term its boundary is the covariant parameter acceleration.

theorem actual_metricEnergy_jetBoundary_hasDerivAt (g : SmoothMetric M) (c : M)
    (x : ℝ → FourSpace) (v u : ℝ → JacobiCoordinateVector)
    (a q : JacobiCoordinateVector) (t : ℝ)
    (hz : x t ∈ (chartAt FourSpace c).target)
    (hx : HasDerivAt x (WithLp.toLp 2 (v t)) t)
    (hv : HasDerivAt v a t) (hu : HasDerivAt u q t)
    (ha : a = -(jacobiConnection (fun i => connectionMatrix g c i (x t)) (v t) *ᵥ v t)) :
    HasDerivAt (fun s => jacobiMetricPair (metricInChart g c (x s)) (v s) (u s))
      ((1 / 2 : ℝ) * jacobiMetricPair (jacobiMetricFirstDirectional g c (x t) (u t))
        (v t) (v t) + jacobiMetricPair (metricInChart g c (x t)) (v t) q) t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.jacobiConnection, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair, OAI.PositiveEinsteinFour.Geometry.jacobiMetricFirstDirectional

theorem OAI.PositiveEinsteinFour.Geometry.framed_pairMatrix line 8735
theorem OAI.PositiveEinsteinFour.Geometry.framed_lowered_endomorphism line 8746
theorem OAI.PositiveEinsteinFour.Geometry.normalized_frame_inverse line 8761
theorem OAI.PositiveEinsteinFour.Geometry.frameChart_curvatureEndomorphism line 8772
theorem OAI.PositiveEinsteinFour.Geometry.frameChart_normal_jacobi_curvature line 8801
Source documentation
The curvature action on an arbitrary variation vector has zero tangential component and the actual normal Jacobi matrix as its tail.
```
theorem frameChart_normal_jacobi_curvature (g : SmoothMetric M) (c : M)
    (e : FrameBundle g) (he : e.base ∈ (chartAt FourSpace c).source)
    (v : JacobiCoordinateVector) :
    (frameChartMatrix g c e)⁻¹ *ᵥ (jacobiCurvatureCombination
      (fun i j => coordinateCurvatureMatrix g c i j (chartAt FourSpace c e.base))
      (frameChartMatrix g c e *ᵥ v) (fun a => frameChartMatrix g c e a 0) *ᵥ
        (fun a => frameChartMatrix g c e a 0)) =
      Fin.cons 0 ((1 + frameCurvatureField g e) *ᵥ (fun i => v i.succ)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix, OAI.PositiveEinsteinFour.Geometry.jacobiCurvatureCombination, OAI.PositiveEinsteinFour.Geometry.coordinateCurvatureMatrix, OAI.PositiveEinsteinFour.Geometry.frameCurvatureField
theorem OAI.PositiveEinsteinFour.Geometry.heatMatrixProduct_hasDerivAt line 8856
theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.direction line 8867
theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.stationary line 8879
theorem OAI.PositiveEinsteinFour.Geometry.heatRadialFrameGram_hasDerivAt_zero line 8897
theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.gram line 8931
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.contDiffAt_slice line 8966
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonianField_coordinates line 8999
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonianField_zero_momentum line 9012
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.zero_momentum_fixed line 9019
def OAI.PositiveEinsteinFour.Geometry.kineticZeroDifferential line 9031
Source documentation
The differential sends a momentum perturbation to its raised velocity; the position perturbation has zero rate at zero momentum.
```
def kineticZeroDifferential (g : SmoothMetric M) (c : M) (x : FourSpace) :
    CotangentCoordinates →L[ℝ] CotangentCoordinates :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonianField_zero_directional line 9037
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonianField_hasFDerivAt_zero line 9111
Source documentation
At zero momentum the derivative of the kinetic Hamiltonian vector field is the nilpotent position-from-momentum map.
```
theorem kineticHamiltonianField_hasFDerivAt_zero (g : SmoothMetric M) (c : M)
    (x : FourSpace) (hx : x ∈ (chartAt FourSpace c).target) :
    HasFDerivAt (cotangentHamiltonianField (kineticHamiltonian g c))
      (kineticZeroDifferential g c x) (x, 0) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField, OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian, OAI.PositiveEinsteinFour.Geometry.kineticZeroDifferential
theorem OAI.PositiveEinsteinFour.Geometry.metric_chart_local_edist_bound line 9140
theorem OAI.PositiveEinsteinFour.Geometry.metric_chart_lipschitz_image line 9168
def OAI.PositiveEinsteinFour.Geometry.metricHausdorffMeasure line 9204
theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_eq_scaled_hausdorff line 9211
theorem OAI.PositiveEinsteinFour.Geometry.exists_metricHausdorff_chart_bounds line 9214
def OAI.PositiveEinsteinFour.Geometry.normalDeviationLinear line 9305
def OAI.PositiveEinsteinFour.Geometry.normalDeviationCLM line 9319
theorem OAI.PositiveEinsteinFour.Geometry.continuous_normalDeviation_comp line 9322
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_normalDeviation line 9327
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureField_eq_normalDeviation line 9335
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousCurvatureField line 9343
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.continuousCurvatureDerivative line 9352
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.derivativeCurvatureField line 9363
theorem OAI.PositiveEinsteinFour.Geometry.weightedConnection_frame line 9396
theorem OAI.PositiveEinsteinFour.Geometry.weighted_chart_connection line 9411
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_changedChart_velocity line 9444
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_changedChart_parallel line 9459

theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameCurveAt_of_fixedChart line 9496

Source documentation

A local solution written in any fixed chart satisfies the centered primitive equations used by all actual Weyl and scalar derivative theorems.

theorem parallelFrameCurveAt_of_fixedChart (g : SmoothMetric M) (c : M)
    (γ : ℝ → FrameBundle g) (t : ℝ) (k : Fin 4)
    (hγ : ContinuousAt γ t) (hc : (γ t).base ∈ (chartAt FourSpace c).source)
    (hx : HasDerivAt (fun s => chartAt FourSpace c (γ s).base)
      (WithLp.toLp 2 (fun r => frameChartMatrix g c (γ t) r k)) t)
    (hE : ∀ i j, HasDerivAt (fun s => frameChartMatrix g c (γ s) i j)
      (-(parallelFrameConnection g c k
        (chartAt FourSpace c (γ t).base, frameChartMatrix g c (γ t)) *
          frameChartMatrix g c (γ t)) i j) t) :
    ParallelFrameCurveAt g γ k t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix, OAI.PositiveEinsteinFour.Geometry.parallelFrameConnection, OAI.PositiveEinsteinFour.Geometry.ParallelFrameCurveAt

theorem OAI.PositiveEinsteinFour.Geometry.parallelFrame_variation_quadratic_error line 9574
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrame_gronwall_quadratic line 9595
Source documentation
The Grönwall remainder is uniformly quadratic in the initial increment.
```
theorem parallelFrame_gronwall_quadratic (K A T : ℝ) (h : CoordinateFrameSpace) :
    gronwallBound 0 K (A * ‖h‖ ^ 2) T = gronwallBound 0 K A T * ‖h‖ ^ 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CoordinateFrameSpace

theorem OAI.PositiveEinsteinFour.Geometry.hasFDerivAt_of_parallelFrame_quadratic_error line 9601

Source documentation

A quadratic remainder for a local endpoint map proves the claimed Fréchet derivative; no differentiability premise on that map is needed.

theorem hasFDerivAt_of_parallelFrame_quadratic_error
    (F : CoordinateFrameSpace → CoordinateFrameSpace) (p : CoordinateFrameSpace)
    (V : CoordinateFrameSpace →L[ℝ] CoordinateFrameSpace) (C : ℝ)
    (hb : ∀ᶠ q in 𝓝 p, ‖F q - F p - V (q - p)‖ ≤ C * ‖q - p‖ ^ 2) :
    HasFDerivAt F V p := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.CoordinateFrameSpace

theorem OAI.PositiveEinsteinFour.Geometry.hasFDerivAt_parallelFrame_endpoint line 9611

Source documentation

The endpoint map of a local family of genuine solutions has the variational derivative. All quantitative hypotheses concern the local vector field and its containing convex neighborhood.

theorem hasFDerivAt_parallelFrame_endpoint (g : SmoothMetric M) (c : M)
    (k : Fin 4) (α : CoordinateFrameSpace × ℝ → CoordinateFrameSpace)
    (p : CoordinateFrameSpace) (S B : Set CoordinateFrameSpace) (hS : S ∈ 𝓝 p)
    (hB : Convex ℝ B) (hdom : ∀ z ∈ B, z.1 ∈ (chartAt FourSpace c).target)
    (K L : ℝ≥0) (T : ℝ) (hT : 0 ≤ T)
    (hK : LipschitzOnWith K (parallelFrameVectorField g c k) B)
    (hL : LipschitzOnWith L (fderiv ℝ (parallelFrameVectorField g c k)) B)
    (hD : ∀ z ∈ B, ‖fderiv ℝ (parallelFrameVectorField g c k) z‖ ≤ K)
    (hα0 : ∀ q ∈ S, α (q, 0) = q)
    (hα : ∀ q ∈ S, ∀ t ∈ Icc 0 T,
      HasDerivAt (fun s => α (q, s)) (parallelFrameVectorField g c k (α (q, t))) t)
    (hαB : ∀ q ∈ S, ∀ t ∈ Icc 0 T, α (q, t) ∈ B)
…

Mentions: OAI.PositiveEinsteinFour.Geometry.CoordinateFrameSpace, OAI.PositiveEinsteinFour.Geometry.parallelFrameVectorField

theorem OAI.PositiveEinsteinFour.Geometry.frozenScalarPrincipal_eq_conjugate line 9652
theorem OAI.PositiveEinsteinFour.Geometry.frozenScalarPrincipal_contDiffAt line 9660
theorem OAI.PositiveEinsteinFour.Geometry.frozenScalarPrincipal_contDiffOn line 9672
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartValue_extract line 9698
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.of_coordinates line 9709
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSmooth_iff_coordinates line 9733
def OAI.PositiveEinsteinFour.Geometry.twoFormCovariantPairing line 9758
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCovariantPairing_eq_frame line 9763
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCovariantPairing_comm line 9774
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCovariantPairing_self_nonneg line 9779
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.covariantPairing_continuous line 9785
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCovariantEnergy line 9811
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCovariantPairing_integrable line 9814
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCovariantEnergy_comm line 9820
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCovariantEnergy_nonneg line 9827
theorem OAI.PositiveEinsteinFour.Geometry.twoFormExtract_apply line 9847
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_curvature_row line 9851
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureAction_component line 9867
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureAction_symmetric line 9881
def OAI.PositiveEinsteinFour.Geometry.twoTensorContractionFamily line 9915
def OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureFamily line 9933
def OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureOperator line 9950
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureOperator_apply line 9965
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureAction_norm_le line 9968
theorem OAI.PositiveEinsteinFour.Geometry.chartGramMatrix_det_ne_zero line 9994
def OAI.PositiveEinsteinFour.Geometry.chartTwoFormConnection line 9999
theorem OAI.PositiveEinsteinFour.Geometry.chartTwoFormConnection_equation line 10003
theorem OAI.PositiveEinsteinFour.Geometry.chartTwoFormConnection_skew line 10010
theorem OAI.PositiveEinsteinFour.Geometry.chartTwoFormConnection_as_twoForm line 10041
theorem OAI.PositiveEinsteinFour.Geometry.chartInverseMatrix_center line 10066
def OAI.PositiveEinsteinFour.Geometry.twoFormFramedValue line 10079
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFramedValue_eq line 10083
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.continuous_framedValue line 10092
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFramedValue_norm line 10099
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.framedValue_parallel_derivative line 10104
def OAI.PositiveEinsteinFour.Geometry.SmoothL2TwoForm line 10141
Source comment
The L2 topology of the completion differs from the pointwise topology on the smooth function submodule.
```
def SmoothL2TwoForm (o : FrameOrientation g) : Type _ := ↥(smoothTwoForms o)
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.smoothTwoForms
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 10144) line 10144
instance OAI.PositiveEinsteinFour.Geometry.smoothTwoFormInnerCore line 10146
instance OAI.PositiveEinsteinFour.Geometry.smoothTwoFormNormedAddCommGroup line 10158
instance OAI.PositiveEinsteinFour.Geometry.smoothTwoFormInnerProductSpace line 10161
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_inner_eq line 10164
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_norm_sq line 10168
def OAI.PositiveEinsteinFour.Geometry.TwoFormL2 line 10173
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormToL2 line 10176
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormToL2_dense line 10179
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormToL2_injective line 10182
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormToL2_inner line 10185
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormToL2_norm_sq line 10191
theorem OAI.PositiveEinsteinFour.classified_of_actual_oriented_models line 10219
def OAI.PositiveEinsteinFour.Geometry.measurableChart line 10259
theorem OAI.PositiveEinsteinFour.Geometry.measurable_measurableChart line 10264
theorem OAI.PositiveEinsteinFour.Geometry.measurableChart_eq line 10270
def OAI.PositiveEinsteinFour.Geometry.chartHausdorffMeasure line 10275
theorem OAI.PositiveEinsteinFour.Geometry.chartHausdorffMeasure_apply line 10279
abbrev OAI.PositiveEinsteinFour.Geometry.PositiveRadius line 10316
instance OAI.PositiveEinsteinFour.Geometry.radialCubicMeasure_openPos line 10318

theorem OAI.PositiveEinsteinFour.Geometry.measurePreserving_energyShell line 10347

Source documentation

Product measure preservation and continuity imply preservation on every radial slice, including the unit kinetic-energy shell.

theorem measurePreserving_energyShell
    (ν : Measure X) [IsProbabilityMeasure ν]
    (ρ : Measure PositiveRadius) [SigmaFinite ρ] [IsOpenPosMeasure ρ]
    (F : PositiveRadius × X → X) (hF : Continuous F)
    (hambient : MeasurePreserving (fun p : PositiveRadius × X => (p.1, F p))
      (ρ.prod ν) (ρ.prod ν)) (r : PositiveRadius) :
    MeasurePreserving (fun x => F (r, x)) ν ν := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.PositiveRadius

theorem OAI.PositiveEinsteinFour.Geometry.measurePreserving_cubicEnergyShell line 10415
def OAI.PositiveEinsteinFour.Geometry.euclideanPolarHomeomorph line 10441
theorem OAI.PositiveEinsteinFour.Geometry.euclideanPolarHomeomorph_apply line 10446
def OAI.PositiveEinsteinFour.Geometry.euclideanPolarReconstruction line 10449
theorem OAI.PositiveEinsteinFour.Geometry.euclideanPolarHomeomorph_symm_coe line 10452
theorem OAI.PositiveEinsteinFour.Geometry.euclideanPolarReconstruction_measurePreserving line 10455
theorem OAI.PositiveEinsteinFour.Geometry.euclideanPolarReconstruction_norm line 10470
theorem OAI.PositiveEinsteinFour.Geometry.actual_baseCurvature line 10498
theorem OAI.PositiveEinsteinFour.Geometry.actual_baseDerivative line 10504
theorem OAI.PositiveEinsteinFour.Geometry.compactSpace_of_compact_frames line 10512
theorem OAI.PositiveEinsteinFour.Geometry.continuous_totalGradientEnergy line 10520
theorem OAI.PositiveEinsteinFour.Geometry.totalGradientEnergy_integrable line 10541
theorem OAI.PositiveEinsteinFour.Geometry.orientedNormSquares_integrable line 10549
theorem OAI.PositiveEinsteinFour.Geometry.BrinKarcherAveraging.integral_of_base_value line 10584
theorem OAI.PositiveEinsteinFour.Geometry.frame_derivative_energy_le_of_parallel_data line 10598
theorem OAI.PositiveEinsteinFour.Geometry.jacobiConnection_weighted line 10667
theorem OAI.PositiveEinsteinFour.Geometry.jacobiConnection_pullback line 10680
def OAI.PositiveEinsteinFour.Geometry.jacobiCovariantSecondJet line 10695
theorem OAI.PositiveEinsteinFour.Geometry.jacobiCovariantSecondJet_pullback line 10699
theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair_pullback line 10710
def OAI.PositiveEinsteinFour.Geometry.chartTransitionSecondVector line 10718
def OAI.PositiveEinsteinFour.Geometry.chartTransitionSecondJet line 10722
theorem OAI.PositiveEinsteinFour.Geometry.chartTransition_connection_equation line 10726

theorem OAI.PositiveEinsteinFour.Geometry.actual_covariantSecondJet_transition line 10742

Source documentation

The corrected second coordinate jet transforms as a tangent vector.

theorem actual_covariantSecondJet_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)
    (y u : JacobiCoordinateVector) :
    chartTransitionMatrix c d z *ᵥ
        jacobiCovariantSecondJet (fun i => connectionMatrix g c i z) y u =
      jacobiCovariantSecondJet
        (fun i => connectionMatrix g d i (chartTransition c d z))
        (chartTransitionMatrix c d z *ᵥ y) (chartTransitionSecondJet c d z y u) :=
…

Mentions: OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.chartTransitionMatrix, OAI.PositiveEinsteinFour.Geometry.jacobiCovariantSecondJet, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.chartTransition, OAI.PositiveEinsteinFour.Geometry.chartTransitionSecondJet

theorem OAI.PositiveEinsteinFour.Geometry.actual_secondVariationBoundary_transition line 10755

Source documentation

The full second-variation boundary scalar agrees on overlapping charts.

theorem actual_secondVariationBoundary_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)
    (v y u : JacobiCoordinateVector) :
    jacobiMetricPair (metricInChart g c z) v
        (jacobiCovariantSecondJet (fun i => connectionMatrix g c i z) y u) =
      jacobiMetricPair (metricInChart g d (chartTransition c d z))
        (chartTransitionMatrix c d z *ᵥ v)
        (jacobiCovariantSecondJet
          (fun i => connectionMatrix g d i (chartTransition c d z))
          (chartTransitionMatrix c d z *ᵥ y) (chartTransitionSecondJet c d z y u)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair, OAI.PositiveEinsteinFour.Geometry.jacobiCovariantSecondJet, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.chartTransition, OAI.PositiveEinsteinFour.Geometry.chartTransitionMatrix, OAI.PositiveEinsteinFour.Geometry.chartTransitionSecondJet

theorem OAI.PositiveEinsteinFour.Geometry.chartTransition_hasDerivAt line 10769

theorem OAI.PositiveEinsteinFour.Geometry.chartTransition_secondJet_hasDerivAt line 10781

Source documentation

A genuine raw second jet has the Hessian-corrected transformation used above.

theorem chartTransition_secondJet_hasDerivAt (c d : M)
    (x : ℝ → FourSpace) (y : ℝ → JacobiCoordinateVector)
    (u : JacobiCoordinateVector) (t : ℝ)
    (hz : x t ∈ (chartAt FourSpace c).target)
    (hd : (chartAt FourSpace c).symm (x t) ∈ (chartAt FourSpace d).source)
    (hx : HasDerivAt x (WithLp.toLp 2 (y t)) t) (hy : HasDerivAt y u t) :
    HasDerivAt (fun s => chartTransitionMatrix c d (x s) *ᵥ y s)
      (chartTransitionSecondJet c d (x t) (y t) u) t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.chartTransitionMatrix, OAI.PositiveEinsteinFour.Geometry.chartTransitionSecondJet

def OAI.PositiveEinsteinFour.Geometry.kineticVelocityCoordinates line 10827
def OAI.PositiveEinsteinFour.Geometry.kineticVelocityRate line 10831
theorem OAI.PositiveEinsteinFour.Geometry.kineticVelocityCoordinates_contDiffAt line 10837
theorem OAI.PositiveEinsteinFour.Geometry.kineticVelocityCoordinates_curve_derivative line 10854
theorem OAI.PositiveEinsteinFour.Geometry.kineticVelocityCoordinates_fderiv line 10880
theorem OAI.PositiveEinsteinFour.Geometry.kinetic_force_transpose line 10898
theorem OAI.PositiveEinsteinFour.Geometry.kinetic_inverse_metric_rate line 10913
theorem OAI.PositiveEinsteinFour.Geometry.inverse_rate_cancel line 10925
theorem OAI.PositiveEinsteinFour.Geometry.kineticVelocityCoordinates_intertwines line 10931
Source documentation
Exact intertwining of the actual Hamiltonian and geodesic fields.
```
theorem kineticVelocityCoordinates_intertwines (g : SmoothMetric M) (c : M)
    (p : CotangentCoordinates) (hp : p.1 ∈ (chartAt FourSpace c).target) :
    fderiv ℝ (kineticVelocityCoordinates g c) p
      (cotangentHamiltonianField (kineticHamiltonian g c) p) =
      geodesicCoordinateField g c (kineticVelocityCoordinates g c p) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.kineticVelocityCoordinates, OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField, OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian, OAI.PositiveEinsteinFour.Geometry.geodesicCoordinateField
theorem OAI.PositiveEinsteinFour.Geometry.kinetic_geodesic_curve line 10950
def OAI.PositiveEinsteinFour.Geometry.geodesicFramePosition line 10982
def OAI.PositiveEinsteinFour.Geometry.geodesicFrameVelocity line 10988
def OAI.PositiveEinsteinFour.Geometry.geodesicNormalPosition line 10994
def OAI.PositiveEinsteinFour.Geometry.geodesicNormalVelocity line 10998

theorem OAI.PositiveEinsteinFour.Geometry.actual_geodesic_normal_variation line 11005

Source documentation

The actual linearized tangent geodesic equation, expressed using the inverse of an actual parallel orthonormal frame. Its coefficient is the same one defining actualJacobiSolution.

theorem actual_geodesic_normal_variation (g : SmoothMetric M) (c : M)
    (e : ℝ → FrameBundle g) (γ Z : ℝ → FourSpace × FourSpace) (t : ℝ)
    (hc : (e t).base ∈ (chartAt FourSpace c).source)
    (hposition : (γ t).1 = chartAt FourSpace c (e t).base)
    (hvelocity : WithLp.ofLp (γ t).2 = fun i => frameChartMatrix g c (e t) i 0)
    (hγ : HasDerivAt γ (geodesicCoordinateField g c (γ t)) t)
    (hZ : HasDerivAt Z (fderiv ℝ (geodesicCoordinateField g c) (γ t) (Z t)) t)
    (hE : ∀ i j, HasDerivAt (fun s => frameChartMatrix g c (e s) i j)
      (-(jacobiConnection (fun k => connectionMatrix g c k (γ t).1)
        (WithLp.ofLp (γ t).2) * frameChartMatrix g c (e t)) i j) t) :
    HasDerivAt (geodesicNormalPosition g c e Z)
      (geodesicNormalVelocity g c e γ Z t) t ∧
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix, OAI.PositiveEinsteinFour.Geometry.geodesicCoordinateField, OAI.PositiveEinsteinFour.Geometry.jacobiConnection, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.geodesicNormalPosition, OAI.PositiveEinsteinFour.Geometry.geodesicNormalVelocity

theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.exists_pos_slice line 11095
def OAI.PositiveEinsteinFour.Geometry.heatRadialFrameEndpoint line 11113
theorem OAI.PositiveEinsteinFour.Geometry.heatRadialFrameEndpoint_zero line 11117
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatRadialFrameEndpoint line 11122
def OAI.PositiveEinsteinFour.Geometry.heatRadialCotangentState line 11178
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_heatRadialCotangentState line 11182
theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.cotangent_derivative line 11209
theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.eq_on line 11251
abbrev OAI.PositiveEinsteinFour.Geometry.TwoFormMatrix line 11307
def OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureMatrix line 11309
def OAI.PositiveEinsteinFour.Geometry.twoFormPotentialMatrix line 11313
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureMatrix_apply line 11316
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotentialMatrix_apply line 11325
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotentialMatrix_trace line 11340
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotentialMatrix_square_trace line 11344
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureMatrix_symmetric line 11354
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureMatrix_square_trace line 11360
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.contDiffAt_initial line 11393
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.exists_pos_contDiffAt_slice line 11412
theorem OAI.PositiveEinsteinFour.Geometry.kineticZeroDifferential_apply line 11450
theorem OAI.PositiveEinsteinFour.Geometry.kineticZeroDifferential_square line 11455

theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.zero_momentum_variation line 11462

Source documentation

The first variation is exactly the shear id + t D, where D² = 0.

theorem KineticLocalFlow.zero_momentum_variation (g : SmoothMetric M) (c : M)
    (x : FourSpace) (hx : x ∈ (chartAt FourSpace c).target)
    (F : KineticLocalFlow g c (x, 0)) (t : ℝ) (ht : t ∈ Ioo (-F.time) F.time) :
    F.variation ((x, 0), t) = ContinuousLinearMap.id ℝ CotangentCoordinates +
      t • kineticZeroDifferential g c x := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow, OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.kineticZeroDifferential

theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.zero_momentum_endpoint_derivative line 11496

Source documentation

Varying only the initial momentum differentiates the endpoint by t times the inverse metric at the starting point.

theorem KineticLocalFlow.zero_momentum_endpoint_derivative (g : SmoothMetric M) (c : M)
    (x : FourSpace) (hx : x ∈ (chartAt FourSpace c).target)
    (F : KineticLocalFlow g c (x, 0)) (t : ℝ) (ht : t ∈ Ioo (-F.time) F.time) :
    HasFDerivAt (fun p : FourSpace => (F.map ((x, p), t)).1)
      (t • Matrix.toEuclideanCLM (n := Fin 4) (𝕜 := ℝ) ((metricInChart g c x)⁻¹)) 0 := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow

theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.zero_momentum_endpoint_strictDerivative line 11517

Source documentation

The same endpoint derivative is strict, as required by the inverse function theorem. It follows directly from the constructed joint flow.

theorem KineticLocalFlow.zero_momentum_endpoint_strictDerivative (g : SmoothMetric M) (c : M)
    (x : FourSpace) (hx : x ∈ (chartAt FourSpace c).target)
    (F : KineticLocalFlow g c (x, 0)) (t : ℝ) (ht : t ∈ Ioo (-F.time) F.time) :
    HasStrictFDerivAt (fun p : FourSpace => (F.map ((x, p), t)).1)
      (t • Matrix.toEuclideanCLM (n := Fin 4) (𝕜 := ℝ) ((metricInChart g c x)⁻¹)) 0 := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow

theorem OAI.PositiveEinsteinFour.Geometry.frame_eq_of_chart_coordinates line 11556
theorem OAI.PositiveEinsteinFour.Geometry.chartFrameStateToBundle_fromFrame line 11586
theorem OAI.PositiveEinsteinFour.Geometry.exists_local_intrinsic_parallelFrame line 11600
Source documentation
The actual coordinate ODE gives a continuous local curve in the frame bundle through every prescribed frame.
```
theorem exists_local_intrinsic_parallelFrame (g : SmoothMetric M)
    (e : FrameBundle g) (k : Fin 4) :
    ∃ ε > (0 : ℝ), ∃ γ : ℝ → FrameBundle g, γ 0 = e ∧
      ContinuousOn γ (Set.Ioo (-ε) ε) ∧
      ∀ t ∈ Set.Ioo (-ε) ε, ParallelFrameCurveAt g γ k t := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.ParallelFrameCurveAt
def OAI.PositiveEinsteinFour.Geometry.scalarRescaledPoint line 11689
def OAI.PositiveEinsteinFour.Geometry.scalarRescaledPrincipal line 11693
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledPrincipal_zero line 11697
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledPoint_mem_nhds line 11702
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledPrincipal_uniform line 11720
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledPrincipal_contDiffAt line 11733
def OAI.PositiveEinsteinFour.Geometry.scalarFrozenDrift line 11742
def OAI.PositiveEinsteinFour.Geometry.scalarRescaledDrift line 11747
theorem OAI.PositiveEinsteinFour.Geometry.scalarFrozenDrift_contDiffAt line 11751
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledDrift_uniform line 11766
def OAI.PositiveEinsteinFour.Geometry.covariantFieldCoordinates line 11816
def OAI.PositiveEinsteinFour.Geometry.CovariantFieldSmooth line 11820
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldCoordinates_center line 11824
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldCoordinates_transition line 11830
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldCoordinates_add line 11842
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldCoordinates_smul line 11849
def OAI.PositiveEinsteinFour.Geometry.smoothCovariantFields line 11854
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCovariantField line 11874
theorem OAI.PositiveEinsteinFour.Geometry.twoTensorMatrix_frame line 11895
theorem OAI.PositiveEinsteinFour.Geometry.twoTensorMatrix_skew line 11907
theorem OAI.PositiveEinsteinFour.Geometry.twoTensor_frame_skew line 11913
theorem OAI.PositiveEinsteinFour.Geometry.twoFormTensor_extract line 11924
def OAI.PositiveEinsteinFour.Geometry.twoFormFromCoordinates line 11936
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFromCoordinates_tensorAt line 11941
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFromCoordinates_coordinates line 11949
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFromCoordinates_smooth line 11963
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoordinates_add line 11998
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoordinates_smul line 12007
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCovariantCoordinates_add line 12020
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCovariantCoordinates_smul line 12030
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFramedCovariantDerivative_add line 12049
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFramedCovariantDerivative_smul line 12058
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCovariantPairing_add line 12067
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCovariantPairing_smul line 12074
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCovariantEnergy_add line 12083
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCovariantEnergy_smul line 12092
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvature_sum_two_indices line 12114
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvature_sum_four_indices line 12120
theorem OAI.PositiveEinsteinFour.Geometry.twoFormTensor_pairing line 12126
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMatrix_pairing line 12133
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvature_quadratic line 12139
theorem OAI.PositiveEinsteinFour.Geometry.sum_four_swap_middle_last line 12165
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvature_cross_contraction line 12177
def OAI.PositiveEinsteinFour.Geometry.smoothL2HodgeLinear line 12247
theorem OAI.PositiveEinsteinFour.Geometry.smoothL2HodgeLinear_involutive line 12251
def OAI.PositiveEinsteinFour.Geometry.smoothL2Hodge line 12254
def OAI.PositiveEinsteinFour.Geometry.twoFormL2Hodge line 12264
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2Hodge_smooth line 12267
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2Hodge_involutive line 12271
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2Hodge_norm line 12281
def OAI.PositiveEinsteinFour.Geometry.twoFormL2HodgeIsometry line 12291
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2Hodge_inner line 12295
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2Hodge_selfAdjoint line 12299
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_twoForm line 12321
theorem OAI.PositiveEinsteinFour.Geometry.tensorPartial_twoForm line 12340
def OAI.PositiveEinsteinFour.Geometry.twoFormLocalNabla line 12353
theorem OAI.PositiveEinsteinFour.Geometry.twoFormLocalNabla_hodge line 12358
def OAI.PositiveEinsteinFour.Geometry.twoFormMetricCurvatureTensor line 12390
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMetricCurvatureTensor_continuous line 12394
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMetricCurvatureTensor_skew line 12402
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMetricCurvatureTensor_change line 12410
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMetricCurvatureTensor_chart line 12417
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMetricCurvatureTensor_bound line 12427
def OAI.PositiveEinsteinFour.Geometry.twoFormSecondCovariantCoordinates line 12456
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.secondCovariant_contDiffAt line 12460
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.secondCovariant_transition line 12467
def OAI.PositiveEinsteinFour.Geometry.twoFormFramedSecondDerivative line 12480
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.continuous_framedSecondDerivative line 12485
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.framedCovariant_parallel_derivative line 12492
def OAI.PositiveEinsteinFour.Geometry.twoFormFramedRoughTrace line 12505
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.continuous_framedRoughTrace line 12509
def OAI.PositiveEinsteinFour.Geometry.chartCoordinateMeasure line 12539
instance OAI.PositiveEinsteinFour.Geometry.chartCoordinateMeasure_sigmaFinite line 12542
def OAI.PositiveEinsteinFour.Geometry.chartCotangentLowering line 12550
theorem OAI.PositiveEinsteinFour.Geometry.continuous_chartCotangentLowering line 12554
theorem OAI.PositiveEinsteinFour.Geometry.chartCotangentLowering_measurePreserving line 12583
def OAI.PositiveEinsteinFour.Geometry.chartPolarLowering line 12613
Source documentation
Base point, direction and positive radius as actual cotangent coordinates, using the smooth Gram frame on the chart.
```
def chartPolarLowering (g : SmoothMetric M) (c : M)
    (p : ChartTarget c × (Angular.Directions × Set.Ioi (0 : ℝ))) :
    ChartTarget c × FourSpace :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ChartTarget, OAI.PositiveEinsteinFour.Angular.Directions
theorem OAI.PositiveEinsteinFour.Geometry.chartPolarLowering_measurePreserving line 12618
theorem OAI.PositiveEinsteinFour.Geometry.chartPolarLowering_energy line 12627
theorem OAI.PositiveEinsteinFour.Geometry.skew_square_sum line 12654
theorem OAI.PositiveEinsteinFour.Geometry.sum_four_components line 12663
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureMatrix_tensorNorm line 12669
def OAI.PositiveEinsteinFour.Geometry.chartEnergyDensity line 12729
def OAI.PositiveEinsteinFour.Geometry.chartEnergyFirstDensity line 12733
def OAI.PositiveEinsteinFour.Geometry.chartEnergySecondDensity line 12738
def OAI.PositiveEinsteinFour.Geometry.chartEnergyIndexDensity line 12745
def OAI.PositiveEinsteinFour.Geometry.chartEnergyBoundary line 12750
theorem OAI.PositiveEinsteinFour.Geometry.chartEnergy_firstJet_hasDerivAt line 12755
theorem OAI.PositiveEinsteinFour.Geometry.secondDeriv_at_of_shift line 12794
theorem OAI.PositiveEinsteinFour.Geometry.chartEnergy_secondJet_hasDerivAt line 12811
theorem OAI.PositiveEinsteinFour.Geometry.chartEnergyFirst_hasDerivAt line 12843

theorem OAI.PositiveEinsteinFour.Geometry.chartEnergyIntegral_secondDeriv line 12861

Source documentation

Differentiation under the energy integral uses only the ordinary raw parameter jets and joint continuity of the three explicit scalar densities.

theorem chartEnergyIntegral_secondDeriv (g : SmoothMetric M) (c : M)
    (x : ℝ → ℝ → FourSpace) (y v w u q : ℝ → ℝ → JacobiCoordinateVector)
    {δ a b : ℝ} (hδ : 0 < δ) (hab : a ≤ b)
    (hz : ∀ s ∈ Icc (-δ) δ, ∀ t ∈ Icc a b, x s t ∈ (chartAt FourSpace c).target)
    (hx : ∀ s ∈ Ioo (-δ) δ, ∀ t ∈ Icc a b,
      HasDerivAt (fun r => x r t) (WithLp.toLp 2 (y s t)) s)
    (hy : ∀ s ∈ Ioo (-δ) δ, ∀ t ∈ Icc a b,
      HasDerivAt (fun r => y r t) (u s t) s)
    (hv : ∀ s ∈ Ioo (-δ) δ, ∀ t ∈ Icc a b,
      HasDerivAt (fun r => v r t) (w s t) s)
    (hw : ∀ s ∈ Ioo (-δ) δ, ∀ t ∈ Icc a b,
      HasDerivAt (fun r => w r t) (q s t) s)
…

Mentions: OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector

theorem OAI.PositiveEinsteinFour.Geometry.chartEnergyBoundary_hasDerivAt line 12905

Source documentation

The derivative of the total boundary, with no omitted second-jet term.

theorem chartEnergyBoundary_hasDerivAt (g : SmoothMetric M) (c : M)
    (x : ℝ → FourSpace) (v y u : ℝ → JacobiCoordinateVector)
    (w q : JacobiCoordinateVector) (t : ℝ)
    (hz : x t ∈ (chartAt FourSpace c).target)
    (hx : HasDerivAt x (WithLp.toLp 2 (v t)) t)
    (hv : HasDerivAt v
      (-(jacobiConnection (fun i => connectionMatrix g c i (x t)) (v t) *ᵥ v t)) t)
    (hy : HasDerivAt y w t) (hu : HasDerivAt u q t) :
    HasDerivAt (fun s => chartEnergyBoundary g c (x s) (v s) (y s) (u s))
      (chartEnergySecondDensity g c (x t) (y t) (v t) w (u t) q -
        chartEnergyIndexDensity g c (x t) (v t) (y t) w) t := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.jacobiConnection, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.chartEnergyBoundary, OAI.PositiveEinsteinFour.Geometry.chartEnergySecondDensity, OAI.PositiveEinsteinFour.Geometry.chartEnergyIndexDensity

theorem OAI.PositiveEinsteinFour.Geometry.chartEnergySecond_integral line 12935
theorem OAI.PositiveEinsteinFour.Geometry.chartEnergyBoundary_zero line 12957
theorem OAI.PositiveEinsteinFour.Geometry.chartEnergySecond_integral_fixedEndpoints line 12961
theorem OAI.PositiveEinsteinFour.Geometry.chartEnergyBoundary_transition line 12980
theorem OAI.PositiveEinsteinFour.Geometry.kineticVelocityCoordinates_vertical_fderiv line 13012
Source documentation
A momentum change obtained by lowering w raises back to w, with zero change of the base point.
```
theorem kineticVelocityCoordinates_vertical_fderiv (g : SmoothMetric M) (c : M)
    (p : CotangentCoordinates) (w : Fin 4 → ℝ)
    (hp : p.1 ∈ (chartAt FourSpace c).target) :
    fderiv ℝ (kineticVelocityCoordinates g c) p
      (0, WithLp.toLp 2 (metricInChart g c p.1 *ᵥ w)) =
        (0, WithLp.toLp 2 w) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.kineticVelocityCoordinates

theorem OAI.PositiveEinsteinFour.Geometry.geodesicNormal_initial_of_vertical line 13034

Source documentation

The inverse frame reads a vertical normal variation as initial position zero and initial velocity w.

theorem geodesicNormal_initial_of_vertical (g : SmoothMetric M) (c : M)
    (e : ℝ → FrameBundle g) (γ Z : ℝ → FourSpace × FourSpace)
    (w : Fin 3 → ℝ) (t : ℝ)
    (he : (e t).base ∈ (chartAt FourSpace c).source)
    (hZ : Z t = (0, WithLp.toLp 2
      (frameChartMatrix g c (e t) *ᵥ Fin.cons 0 w))) :
    geodesicNormalPosition g c e Z t = 0 ∧
      geodesicNormalVelocity g c e γ Z t = w := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix, OAI.PositiveEinsteinFour.Geometry.geodesicNormalPosition, OAI.PositiveEinsteinFour.Geometry.geodesicNormalVelocity

theorem OAI.PositiveEinsteinFour.Geometry.kinetic_normal_initial_data line 13064

Source documentation

Apply the preceding identities directly to the differential of momentum raising, at a frame-based initial normal momentum.

theorem kinetic_normal_initial_data (g : SmoothMetric M) (c : M)
    (e : ℝ → FrameBundle g) (γ Z : ℝ → FourSpace × FourSpace)
    (p : CotangentCoordinates) (w : Fin 3 → ℝ) (t : ℝ)
    (he : (e t).base ∈ (chartAt FourSpace c).source)
    (hp : p.1 ∈ (chartAt FourSpace c).target)
    (hZ : Z t = fderiv ℝ (kineticVelocityCoordinates g c) p
      (0, WithLp.toLp 2 (metricInChart g c p.1 *ᵥ
        (frameChartMatrix g c (e t) *ᵥ Fin.cons 0 w)))) :
    geodesicNormalPosition g c e Z t = 0 ∧
      geodesicNormalVelocity g c e γ Z t = w := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.kineticVelocityCoordinates, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix, OAI.PositiveEinsteinFour.Geometry.geodesicNormalPosition, OAI.PositiveEinsteinFour.Geometry.geodesicNormalVelocity

theorem OAI.PositiveEinsteinFour.Geometry.actual_geodesic_frame_variation line 13099

Source documentation

The actual frame variation has zero radial acceleration and the true normal Jacobi acceleration.

theorem actual_geodesic_frame_variation (g : SmoothMetric M) (c : M)
    (e : ℝ → FrameBundle g) (γ Z : ℝ → FourSpace × FourSpace) (t : ℝ)
    (hc : (e t).base ∈ (chartAt FourSpace c).source)
    (hposition : (γ t).1 = chartAt FourSpace c (e t).base)
    (hvelocity : WithLp.ofLp (γ t).2 = fun i => frameChartMatrix g c (e t) i 0)
    (hγ : HasDerivAt γ (geodesicCoordinateField g c (γ t)) t)
    (hZ : HasDerivAt Z (fderiv ℝ (geodesicCoordinateField g c) (γ t) (Z t)) t)
    (hE : ∀ i j, HasDerivAt (fun s => frameChartMatrix g c (e s) i j)
      (-(jacobiConnection (fun k => connectionMatrix g c k (γ t).1)
        (WithLp.ofLp (γ t).2) * frameChartMatrix g c (e t)) i j) t) :
    HasDerivAt (geodesicFramePosition g c e Z)
      (geodesicFrameVelocity g c e γ Z t) t ∧
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix, OAI.PositiveEinsteinFour.Geometry.geodesicCoordinateField, OAI.PositiveEinsteinFour.Geometry.jacobiConnection, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.geodesicFramePosition, OAI.PositiveEinsteinFour.Geometry.geodesicFrameVelocity

theorem OAI.PositiveEinsteinFour.Geometry.actual_geodesic_radial_variation line 13159

theorem OAI.PositiveEinsteinFour.Geometry.radial_jacobi_pair_eq line 13177

Source documentation

The zero-position radial solution is exactly linear.

theorem radial_jacobi_pair_eq (y z : ℝ → ℝ) (w a b : ℝ)
    (hzero : (0 : ℝ) ∈ Ioo a b) (hy0 : y 0 = 0) (hz0 : z 0 = w)
    (hy : ∀ s ∈ Ioo a b, HasDerivAt y (z s) s)
    (hz : ∀ s ∈ Ioo a b, HasDerivAt z 0 s) :
    ∀ s ∈ Ioo a b, y s = s * w ∧ z s = w := by
…

theorem OAI.PositiveEinsteinFour.Geometry.variational_equation_of_intertwining line 13217

theorem OAI.PositiveEinsteinFour.Geometry.kinetic_geodesic_variation line 13253

Source documentation

The first variation of the actual kinetic flow becomes the first variation of the actual geodesic field after raising momentum.

theorem kinetic_geodesic_variation (g : SmoothMetric M) (c : M)
    (γ Z : ℝ → CotangentCoordinates) (t : ℝ)
    (hp : (γ t).1 ∈ (chartAt FourSpace c).target)
    (hγ : HasDerivAt γ
      (cotangentHamiltonianField (kineticHamiltonian g c) (γ t)) t)
    (hZ : HasDerivAt Z
      (fderiv ℝ (cotangentHamiltonianField (kineticHamiltonian g c)) (γ t) (Z t)) t) :
    HasDerivAt (fun s => fderiv ℝ (kineticVelocityCoordinates g c) (γ s) (Z s))
      (fderiv ℝ (geodesicCoordinateField g c)
        (kineticVelocityCoordinates g c (γ t))
        (fderiv ℝ (kineticVelocityCoordinates g c) (γ t) (Z t))) t := by
…

structure OAI.PositiveEinsteinFour.Geometry.WeylEnergyIdentities line 13309
Source documentation
Disintegration of the normalized frame measure for the metric energy calculation.
```
structure WeylEnergyIdentities (g : SmoothMetric M) (_o : FrameOrientation g)
    (μ : Measure (FrameBundle g)) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle
theorem OAI.PositiveEinsteinFour.Geometry.WeylEnergyIdentities.curvature_energy line 13313
theorem OAI.PositiveEinsteinFour.Geometry.WeylEnergyIdentities.derivative_energy line 13327
structure OAI.PositiveEinsteinFour.Geometry.ParallelJacobiData line 13347
Source documentation
Ordinary parallel-frame Jacobi data and the polar formula. The matrix curve is the actual curvature along this same flow, and RegularJacobi contains its ordinary Jacobi equation and initial conditions.
```
structure ParallelJacobiData (g : SmoothMetric M) (μ : Measure (FrameBundle g)) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle
theorem OAI.PositiveEinsteinFour.Geometry.volume_ratio_upper_of_geometric_identities line 13369
Source documentation
The manuscript's upper-volume deficit from the classical geometric identities and the proved Jacobi comparison. Both required energies and the Jacobi trace are derived here, rather than included among the inputs.
```
theorem volume_ratio_upper_of_geometric_identities
    (g : SmoothMetric M) (o : FrameOrientation g) {μ : Measure (FrameBundle g)}
    (w : WeylEnergyIdentities g o μ) (j : ParallelJacobiData g μ)
    (d : MetricGreenData g μ) (opposite : OppositeWeylData d)
    (hparallel : ParallelReflection d) (h : FollandMoments)
    (hnorm : PetersenOrientedNormInput o) (hvolume : FinitePositiveVolume g)
    (hRic : RicciThree g) (hpositive : HasPositiveSectionalCurvature g) :
    volumeRatio g ≤ 1 - (3 / 40) *
      (∫ c, plusNorm o c ^ 2 + minusNorm o c ^ 2 ∂normalizedVolume g) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.WeylEnergyIdentities, OAI.PositiveEinsteinFour.Geometry.ParallelJacobiData, OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.OppositeWeylData, OAI.PositiveEinsteinFour.Geometry.ParallelReflection, OAI.PositiveEinsteinFour.Geometry.PetersenOrientedNormInput, OAI.PositiveEinsteinFour.Geometry.FinitePositiveVolume, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.volumeRatio, OAI.PositiveEinsteinFour.Geometry.plusNorm, OAI.PositiveEinsteinFour.Geometry.minusNorm, OAI.PositiveEinsteinFour.Geometry.normalizedVolume
theorem OAI.PositiveEinsteinFour.Geometry.heat_alternating_smooth_approx line 13418
theorem OAI.PositiveEinsteinFour.Geometry.heatRadialCotangentState_continuousAt line 13480
theorem OAI.PositiveEinsteinFour.Geometry.continuous_family_ball line 13506
theorem OAI.PositiveEinsteinFour.Geometry.heatRadialCotangentState_common_domain line 13520
def OAI.PositiveEinsteinFour.Geometry.heatRadialFrameFamily line 13555
theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.stationary_at line 13559
theorem OAI.PositiveEinsteinFour.Geometry.heatRadialFrameFamily_zero line 13575
theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.exists_joint_frame_family line 13580
theorem OAI.PositiveEinsteinFour.Geometry.kineticEndpointDerivative_isUnit line 13629

theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.zero_momentum_localChart line 13648

Source documentation

At every nonzero sufficiently small time, the actual endpoint map is a local homeomorphism at zero initial momentum.

theorem KineticLocalFlow.zero_momentum_localChart (g : SmoothMetric M) (c : M)
    (x : FourSpace) (hx : x ∈ (chartAt FourSpace c).target)
    (F : KineticLocalFlow g c (x, 0)) (t : ℝ) (ht : t ∈ Ioo (-F.time) F.time)
    (ht0 : t ≠ 0) :
    ∃ C : OpenPartialHomeomorph FourSpace FourSpace,
      (C : FourSpace → FourSpace) = (fun p => (F.map ((x, p), t)).1) ∧
      0 ∈ C.source ∧ C 0 = x := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow

def OAI.PositiveEinsteinFour.Geometry.frameCoordinateState line 13686
theorem OAI.PositiveEinsteinFour.Geometry.frameCoordinateState_continuousAt line 13690
theorem OAI.PositiveEinsteinFour.Geometry.frameCoordinateState_normalizes line 13700
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameCurveAt_fixedChart line 13708
theorem OAI.PositiveEinsteinFour.Geometry.intrinsic_parallelFrame_unique_near line 13761

theorem OAI.PositiveEinsteinFour.Geometry.intrinsic_parallelFrame_unique_interval line 13796

Source documentation

Two intrinsic horizontal curves with one common value agree throughout any common open interval. Local uniqueness is transported through a fixed chart only near each comparison point.

theorem intrinsic_parallelFrame_unique_interval [T2Space M]
    (g : SmoothMetric M) (γ η : ℝ → FrameBundle g) (k : Fin 4)
    (a b t : ℝ) (ht : t ∈ Set.Ioo a b)
    (hγc : ContinuousOn γ (Set.Ioo a b))
    (hηc : ContinuousOn η (Set.Ioo a b))
    (hγ : ∀ s ∈ Set.Ioo a b, ParallelFrameCurveAt g γ k s)
    (hη : ∀ s ∈ Set.Ioo a b, ParallelFrameCurveAt g η k s)
    (heq : γ t = η t) : Set.EqOn γ η (Set.Ioo a b) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.ParallelFrameCurveAt

theorem OAI.PositiveEinsteinFour.Geometry.intrinsic_parallelFrame_unique_global line 13830

Source documentation

Global intrinsic parallel curves are determined by their initial frame.

theorem intrinsic_parallelFrame_unique_global [T2Space M]
    (g : SmoothMetric M) (γ η : ℝ → FrameBundle g) (k : Fin 4)
    (hγc : Continuous γ) (hηc : Continuous η)
    (hγ : ∀ t, ParallelFrameCurveAt g γ k t)
    (hη : ∀ t, ParallelFrameCurveAt g η k t)
    (heq : γ 0 = η 0) : γ = η := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.ParallelFrameCurveAt

theorem OAI.PositiveEinsteinFour.Geometry.scalarParameter_partial_contDiffAt line 13862
theorem OAI.PositiveEinsteinFour.Geometry.scalarParameter_second_contDiffAt line 13873
theorem OAI.PositiveEinsteinFour.Geometry.scalarCompactParameter_small line 13881
theorem OAI.PositiveEinsteinFour.Geometry.scalarParameter_jets_uniform line 13905
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaled_function_contDiffAt line 13941
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledPrincipal_jets_uniform line 13954
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledDrift_jets_uniform line 13971
def OAI.PositiveEinsteinFour.Geometry.covariantFieldDerivative line 14006
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldDerivative_coordinates line 14010
theorem OAI.PositiveEinsteinFour.Geometry.CovariantFieldSmooth.derivative line 14026
def OAI.PositiveEinsteinFour.Geometry.smoothCovariantDerivative line 14035
def OAI.PositiveEinsteinFour.Geometry.covariantFieldFramed line 14039
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldFramed_eq line 14043
theorem OAI.PositiveEinsteinFour.Geometry.CovariantFieldSmooth.continuous_framed line 14049
theorem OAI.PositiveEinsteinFour.Geometry.CovariantFieldSmooth.parallel_derivative line 14056
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_zero_two line 14092
theorem OAI.PositiveEinsteinFour.Geometry.chartInverseMatrix_det_ne_zero line 14100
def OAI.PositiveEinsteinFour.Geometry.twoFormChartTensor line 14106
def OAI.PositiveEinsteinFour.Geometry.twoFormChartFamily line 14113
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartFamily_transition line 14117
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartFamily_eq line 14127
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartFamily_skew line 14144
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartTensor_zero_off line 14156
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.framed_commutator line 14188
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_two line 14210
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.framed_commutator_components line 14222
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSkewAction_antisymm line 14250
theorem OAI.PositiveEinsteinFour.Geometry.chartTwoFormConnection_formula line 14258
theorem OAI.PositiveEinsteinFour.Geometry.chartTwoFormConnection_contDiffAt line 14271
theorem OAI.PositiveEinsteinFour.Geometry.twoFormConnectionAction_contDiffAt line 14302
def OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureField line 14349
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureField_frame line 14352
theorem OAI.PositiveEinsteinFour.Geometry.chartMetricCurvature_contDiffAt line 14372
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.curvature line 14384
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCurvature line 14400
def OAI.PositiveEinsteinFour.Geometry.twoFormMatrixMul line 14419
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMatrixMul_hodge line 14422
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMetricCurvatureAction_hodge line 14450
def OAI.PositiveEinsteinFour.Geometry.SmoothH1TwoForm line 14506
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 14509) line 14509
instance OAI.PositiveEinsteinFour.Geometry.smoothH1TwoFormInnerCore line 14511
instance OAI.PositiveEinsteinFour.Geometry.smoothH1TwoFormNormedAddCommGroup line 14538
instance OAI.PositiveEinsteinFour.Geometry.smoothH1TwoFormInnerProductSpace line 14541
theorem OAI.PositiveEinsteinFour.Geometry.smoothH1TwoForm_norm_sq line 14544
def OAI.PositiveEinsteinFour.Geometry.smoothH1ToL2Linear line 14550
theorem OAI.PositiveEinsteinFour.Geometry.smoothH1ToL2Linear_norm_le line 14555
def OAI.PositiveEinsteinFour.Geometry.smoothH1ToL2 line 14564
def OAI.PositiveEinsteinFour.Geometry.TwoFormH1 line 14567
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormToH1 line 14570
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormToH1_dense line 14573
def OAI.PositiveEinsteinFour.Geometry.twoFormH1ToL2 line 14576
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1ToL2_smooth line 14579
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1ToL2_norm_le line 14583
def OAI.PositiveEinsteinFour.Geometry.selfDualTwoFormsL2 line 14611
def OAI.PositiveEinsteinFour.Geometry.antiSelfDualTwoFormsL2 line 14614
theorem OAI.PositiveEinsteinFour.Geometry.mem_selfDualTwoFormsL2 line 14617
theorem OAI.PositiveEinsteinFour.Geometry.mem_antiSelfDualTwoFormsL2 line 14622
theorem OAI.PositiveEinsteinFour.Geometry.selfDualTwoFormsL2_closed line 14627
theorem OAI.PositiveEinsteinFour.Geometry.antiSelfDualTwoFormsL2_closed line 14630
def OAI.PositiveEinsteinFour.Geometry.twoFormL2Plus line 14634
def OAI.PositiveEinsteinFour.Geometry.twoFormL2Minus line 14637
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2Plus_apply line 14640
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2Minus_apply line 14643
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2Plus_mem line 14646
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2Minus_mem line 14651
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2_decomposition line 14656
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2_eigenspaces_orthogonal line 14660
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2_split_orthogonal line 14668
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2_norm_sq_split line 14672
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.localNabla_tensor line 14698
def OAI.PositiveEinsteinFour.Geometry.twoFormSecondTrace line 14762
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSecondTrace_frame line 14765
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSecondTrace_orthogonal line 14798
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFramedSecondDerivative_change line 14811
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFramedRoughTrace_change line 14818
def OAI.PositiveEinsteinFour.Geometry.chartCotangentRaising line 14847
theorem OAI.PositiveEinsteinFour.Geometry.continuous_chartCotangentRaising line 14851
theorem OAI.PositiveEinsteinFour.Geometry.chartCotangentRaising_lowering line 14870
theorem OAI.PositiveEinsteinFour.Geometry.chartCotangentLowering_raising line 14880
def OAI.PositiveEinsteinFour.Geometry.chartCotangentHomeomorph line 14893
theorem OAI.PositiveEinsteinFour.Geometry.chartCotangentRaising_measurePreserving line 14902
theorem OAI.PositiveEinsteinFour.Geometry.CovariantFieldSmooth.framed_second line 14929
theorem OAI.PositiveEinsteinFour.Geometry.CovariantFieldSmooth.framed_commutator line 14946
theorem OAI.PositiveEinsteinFour.Geometry.covariantField_eq_of_framed line 14989
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldFramed_add line 15003
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldFramed_smul line 15009
def OAI.PositiveEinsteinFour.Geometry.covariantFieldNormSq line 15034
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldNormSq_eq_frame line 15037
theorem OAI.PositiveEinsteinFour.Geometry.CovariantFieldSmooth.continuous_normSq line 15043
def OAI.PositiveEinsteinFour.Geometry.CovariantTwoFormSkew line 15076
theorem OAI.PositiveEinsteinFour.Geometry.CovariantTwoFormSkew.coordinates line 15080
def OAI.PositiveEinsteinFour.Geometry.covariantFieldTwoForm line 15086
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldTwoForm_tensorAt line 15092
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldTwoForm_coordinates line 15098
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldTwoForm_framed line 15106
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureMatrix_tensorPairing line 15130
def OAI.PositiveEinsteinFour.Geometry.jacobiBlockMatrix line 15183
theorem OAI.PositiveEinsteinFour.Geometry.jacobiBlockMatrix_mulVec line 15186
theorem OAI.PositiveEinsteinFour.Geometry.jacobiBlockMatrix_det line 15195
theorem OAI.PositiveEinsteinFour.Geometry.eq_jacobiBlockMatrix_of_mulVec line 15209
Source documentation
Equality of the radial and normal actions identifies the entire four-dimensional linear map.
```
theorem eq_jacobiBlockMatrix_of_mulVec (A : Mat4) (a : ℝ)
    (J : Matrix (Fin 3) (Fin 3) ℝ)
    (hA : ∀ v : Fin 4 → ℝ, A *ᵥ v =
      Fin.cons (a * v 0) (J *ᵥ fun i => v i.succ)) :
    A = jacobiBlockMatrix a J := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.jacobiBlockMatrix
theorem OAI.PositiveEinsteinFour.Geometry.jacobiBlockMatrix_scaled_det line 15220
Source documentation
This algebraic identity also holds at zero with Lean's division convention; the geometric application uses positive t.
```
theorem jacobiBlockMatrix_scaled_det (t : ℝ)
    (J : Matrix (Fin 3) (Fin 3) ℝ) :
    (jacobiBlockMatrix 1 (t⁻¹ • J)).det = J.det / t ^ 3 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.jacobiBlockMatrix
theorem OAI.PositiveEinsteinFour.Geometry.jacobiBlockMatrix_metric_density line 15231
Source documentation
Multiplication by a genuine orthonormal frame cancels exactly the coordinate metric density.
```
theorem jacobiBlockMatrix_metric_density (g : SmoothMetric M) (c : M)
    (e : FrameBundle g) (he : e.base ∈ (chartAt FourSpace c).source)
    (A : Mat4) :
    chartVolumeDensity g c (chartAt FourSpace c e.base) *
      |(frameChartMatrix g c e * A).det| = |A.det| := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.chartVolumeDensity, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix
theorem OAI.PositiveEinsteinFour.Geometry.jacobiBlockMatrix_scaled_metric_density line 15241
theorem OAI.PositiveEinsteinFour.Geometry.jacobiBlockMatrix_scaled_linear_density line 15249
def OAI.PositiveEinsteinFour.Geometry.endpointWeightLeft line 15277
def OAI.PositiveEinsteinFour.Geometry.endpointWeightRight line 15278
theorem OAI.PositiveEinsteinFour.Geometry.endpointWeightLeft_hasDerivAt line 15280
theorem OAI.PositiveEinsteinFour.Geometry.endpointWeightRight_hasDerivAt line 15285
def OAI.PositiveEinsteinFour.Geometry.endpointResidual line 15294
def OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition line 15296
def OAI.PositiveEinsteinFour.Geometry.endpointCorrectedParameter line 15300
def OAI.PositiveEinsteinFour.Geometry.endpointCorrectedSecond line 15304
def OAI.PositiveEinsteinFour.Geometry.endpointCorrectedVelocity line 15307
def OAI.PositiveEinsteinFour.Geometry.endpointCorrectedMixed line 15311
def OAI.PositiveEinsteinFour.Geometry.endpointCorrectedMixedSecond line 15314
theorem OAI.PositiveEinsteinFour.Geometry.endpointResidual_hasDerivAt line 15317
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition_left line 15323
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition_right line 15330
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition_zero line 15337
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedParameter_zero line 15342
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedParameter_left line 15347
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedParameter_right line 15355
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedSecond_left line 15363
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedSecond_right line 15369
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedVelocity_zero line 15375
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedMixed_zero line 15380
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition_parameter line 15385
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedParameter_parameter line 15397
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedVelocity_parameter line 15406
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedMixed_parameter line 15416
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition_time line 15425
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedParameter_time line 15437
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedSecond_time line 15446
theorem OAI.PositiveEinsteinFour.Geometry.continuous_endpointCorrectedPosition line 15453
theorem OAI.PositiveEinsteinFour.Geometry.continuous_endpointCorrectedVelocity line 15459
theorem OAI.PositiveEinsteinFour.Geometry.continuous_endpointCorrectedParameter line 15465
theorem OAI.PositiveEinsteinFour.Geometry.continuous_endpointCorrectedSecond line 15471
theorem OAI.PositiveEinsteinFour.Geometry.continuous_endpointCorrectedMixed line 15477
theorem OAI.PositiveEinsteinFour.Geometry.continuous_endpointCorrectedMixedSecond line 15483

theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition_inside line 15490

Source documentation

One parameter interval works for the entire compact segment.

theorem endpointCorrectedPosition_inside (x y A B : ℝ → E) (a b : ℝ)
    (hx : Continuous x) (hy : Continuous y) (hA : Continuous A) (hB : Continuous B)
    (hA0 : A 0 = x a) (hB0 : B 0 = x b) (U : Set E) (hU : IsOpen U)
    (hxU : ∀ t ∈ Icc a b, x t ∈ U) :
    ∃ δ > 0, ∀ ε ∈ Icc (-δ) δ, ∀ t ∈ Icc a b,
      endpointCorrectedPosition x y A B a b ε t ∈ U := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition

theorem OAI.PositiveEinsteinFour.Geometry.geodesicFrame_initial_of_vertical line 15535
theorem OAI.PositiveEinsteinFour.Geometry.kinetic_frame_initial_data line 15556
theorem OAI.PositiveEinsteinFour.Geometry.localMin_secondDeriv_nonneg line 15587
theorem OAI.PositiveEinsteinFour.Geometry.finite_piece_secondDeriv line 15624

theorem OAI.PositiveEinsteinFour.Geometry.finite_piece_index_secondDeriv line 15639

Source documentation

The chartwise energy derivatives have the index sum as second derivative after interior boundary matching and fixed endpoint jets.

theorem finite_piece_index_secondDeriv (n : ℕ) (E : ℕ → ℝ → ℝ)
    (I L R : ℕ → ℝ)
    (hfd : ∀ᶠ s in 𝓝 (0 : ℝ), ∀ i < n, DifferentiableAt ℝ (E i) s)
    (hD : ∀ i < n, HasDerivAt (deriv (E i)) (I i + R i - L i) 0)
    (hjoin : ∀ i < n, R i = L (i + 1)) (hleft : L 0 = 0) (hright : L n = 0) :
    HasDerivAt (deriv (fun s => ∑ i ∈ Finset.range n, E i s))
      (∑ i ∈ Finset.range n, I i) 0 := by
…

theorem OAI.PositiveEinsteinFour.Geometry.finite_piece_index_nonneg line 15653
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_curvature_matrix_negative line 15678
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_curvature_action_negative line 15697
theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.regular_at line 15739
def OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.recenter line 15763
theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.recenter_family line 15782
theorem OAI.PositiveEinsteinFour.Geometry.symmetric_zero_diagonal_sum line 15805
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureMatrix_trace_contraction line 15813
theorem OAI.PositiveEinsteinFour.Geometry.actual_twoFormCurvatureMatrix_trace line 15836
theorem OAI.PositiveEinsteinFour.Geometry.actual_twoFormPotential_trace line 15853
theorem OAI.PositiveEinsteinFour.Geometry.actual_twoFormPotential_square_trace line 15858
structure OAI.PositiveEinsteinFour.Geometry.JacobiRealizationData line 15895
def OAI.PositiveEinsteinFour.Geometry.JacobiRealizationData.toParallelJacobiData line 15908
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_zero_one line 15940
def OAI.PositiveEinsteinFour.Geometry.oneFormChartTensor line 15948
def OAI.PositiveEinsteinFour.Geometry.oneFormChartFamily line 15955
theorem OAI.PositiveEinsteinFour.Geometry.oneFormChartFamily_transition line 15959
theorem OAI.PositiveEinsteinFour.Geometry.oneFormChartFamily_eq line 15969
theorem OAI.PositiveEinsteinFour.Geometry.oneFormChartTensor_zero_off line 15986
theorem OAI.PositiveEinsteinFour.Geometry.orientedFrameMap_completion_first line 16022
Source documentation
Right multiplication by the explicit completion produces the direction obtained by the orthogonal action on the sphere.
```
theorem orientedFrameMap_completion_first (e : OrthonormalFrame g c)
    (P : OrientedOrthogonalFour) (q : Directions) :
    (orientedFrameMap e (P * directionOrientedMatrix q)).frame.vector 0 =
      (frameTurn e (orientedDirection P q)).frame.vector 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.OrientedOrthogonalFour, OAI.PositiveEinsteinFour.Geometry.orientedFrameMap, OAI.PositiveEinsteinFour.Geometry.directionOrientedMatrix, OAI.PositiveEinsteinFour.Geometry.frameTurn, OAI.PositiveEinsteinFour.Geometry.orientedDirection
theorem OAI.PositiveEinsteinFour.Geometry.orientedHaar_integral_eq_sphere line 16035
Source documentation
Haar averaging of a direction-invariant function equals its spherical average. Only integrability on the Haar fiber is required.
```
theorem orientedHaar_integral_eq_sphere (e : OrthonormalFrame g c)
    (F : FrameBundle g → ℝ) (hInv : DirectionInvariant F)
    (hF : Integrable (fun Q => F (orientedFrameMap e Q)) orientedFrameHaar) :
    (∫ Q, F (orientedFrameMap e Q) ∂orientedFrameHaar) =
      ∫ q, F (frameTurn e q) ∂sphereMeasure := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.DirectionInvariant, OAI.PositiveEinsteinFour.Geometry.orientedFrameMap, OAI.PositiveEinsteinFour.Geometry.orientedFrameHaar, OAI.PositiveEinsteinFour.Geometry.frameTurn
theorem OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure_integral_base line 16050
Source documentation
Base averages for the constructed frame measure are precisely the normalized Riemannian averages, as used in the Poisson equation.
```
theorem canonicalFrameMeasure_integral_base (g : SmoothMetric M)
    (o : FrameOrientation g) (A : M → ℝ) (hA : Integrable A (normalizedVolume g)) :
    (∫ e : FrameBundle g, A e.base ∂canonicalFrameMeasure g o) =
      ∫ x, A x ∂normalizedVolume g := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.normalizedVolume, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure
theorem OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure_averaging line 16065
Source documentation
The precise Brin--Karcher averaging input holds for the frame probability constructed from actual Riemannian volume.
```
theorem canonicalFrameMeasure_averaging (g : SmoothMetric M) (o : FrameOrientation g) :
    BrinKarcherAveraging g (canonicalFrameMeasure g o) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.BrinKarcherAveraging, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure
theorem OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure_energy line 16087
Source documentation
The canonical frame probability gives the averaged energy identities.
```
theorem canonicalFrameMeasure_energy (g : SmoothMetric M) (o : FrameOrientation g) :
    WeylEnergyIdentities g o (canonicalFrameMeasure g o) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.WeylEnergyIdentities, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameCurveAt_congr line 16111
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameCurveAt_comp_add line 16127
def OAI.PositiveEinsteinFour.Geometry.IsParallelFrameCurveOn line 16138
Source documentation
A curve on an open time set is continuous and satisfies the genuine velocity and Levi-Civita parallel equations there.
```
def IsParallelFrameCurveOn (g : SmoothMetric M) (k : Fin 4)
    (γ : ℝ → FrameBundle g) (s : Set ℝ) : Prop :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle
theorem OAI.PositiveEinsteinFour.Geometry.IsParallelFrameCurveOn.mono line 16142
theorem OAI.PositiveEinsteinFour.Geometry.IsParallelFrameCurveOn.eqOn_interval line 16148
theorem OAI.PositiveEinsteinFour.Geometry.IsParallelFrameCurveOn.comp_add line 16156

theorem OAI.PositiveEinsteinFour.Geometry.parallelFrame_piecewise_eqOn line 16171

Source documentation

The two local curves agree on the entire overlap, so choosing the first one on its interval leaves the second one unchanged on its own interval.

theorem parallelFrame_piecewise_eqOn [T2Space M]
    {g : SmoothMetric M} {k : Fin 4} {γ η : ℝ → FrameBundle g}
    {a b c d t : ℝ}
    (hγ : IsParallelFrameCurveOn g k γ (Set.Ioo a b))
    (hη : IsParallelFrameCurveOn g k η (Set.Ioo c d))
    (ht : t ∈ Set.Ioo a b ∩ Set.Ioo c d) (heq : γ t = η t) :
    Set.EqOn ((Set.Ioo a b).piecewise γ η) η (Set.Ioo c d) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.IsParallelFrameCurveOn

theorem OAI.PositiveEinsteinFour.Geometry.IsParallelFrameCurveOn.piecewise line 16191

Source documentation

Gluing two overlapping local parallel curves produces a parallel curve on the union of their time intervals.

theorem IsParallelFrameCurveOn.piecewise [T2Space M]
    {g : SmoothMetric M} {k : Fin 4} {γ η : ℝ → FrameBundle g}
    {a b c d t : ℝ}
    (hγ : IsParallelFrameCurveOn g k γ (Set.Ioo a b))
    (hη : IsParallelFrameCurveOn g k η (Set.Ioo c d))
    (ht : t ∈ Set.Ioo a b ∩ Set.Ioo c d) (heq : γ t = η t) :
    IsParallelFrameCurveOn g k ((Set.Ioo a b).piecewise γ η)
      (Set.Ioo a b ∪ Set.Ioo c d) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.IsParallelFrameCurveOn

theorem OAI.PositiveEinsteinFour.Geometry.exists_continuous_local_intrinsic_parallelFrame_flow line 16239
def OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunGapInput line 16364
def OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunHodgeInput line 16370
theorem OAI.PositiveEinsteinFour.Geometry.BrinKarcherAveraging.base_integral line 16379
theorem OAI.PositiveEinsteinFour.Geometry.norm_square_frame_integrals line 16392
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartFamily_self line 16435
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartFamily_smooth line 16443
def OAI.PositiveEinsteinFour.Geometry.twoFormChartTest line 16483
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartTest_coordinates line 16494
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartTest_zero_off line 16508
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartTest_support line 16524
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoordinates_eq_zero line 16556
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoordinates_congr_nhds line 16563
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCovariantCoordinates_zero line 16573
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFramedCovariantDerivative_zero_of_nhds line 16583
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCovariantPairing_tsupport_right line 16600
def OAI.PositiveEinsteinFour.Geometry.twoFormLocalNablaRows line 16631
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.gramCovariantDerivative line 16635
theorem OAI.PositiveEinsteinFour.Geometry.twoFormLocalNabla_congr line 16664
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.localNablaRows_hodge line 16670
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvature_slot_sum line 16706
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMetricCurvature_slot_sum line 16755
theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_metricPair line 16795
theorem OAI.PositiveEinsteinFour.Geometry.metricPartial_contDiffAt line 16810
theorem OAI.PositiveEinsteinFour.Geometry.metricSecondPartial_contDiffAt line 16816
theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_chartMatrix line 16824
theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_jacobiMetricFirstDirectional line 16834
theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_jacobiMetricSecondDirectional line 16846
theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_actualMetric line 16860
theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_chartEnergyDensity line 16867
theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_chartEnergyFirstDensity line 16874
theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_chartEnergySecondDensity line 16883

theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrected_energy_continuousOn line 16901

Source documentation

The endpoint-corrected position and velocity give continuous scalar energy densities.

theorem endpointCorrected_energy_continuousOn (g : SmoothMetric M) (c : M)
    (x y v w A B A' B' A'' B'' : ℝ → FourSpace) (a b δ : ℝ)
    (hx : Continuous x) (hy : Continuous y) (hv : Continuous v) (hw : Continuous w)
    (hA : Continuous A) (hB : Continuous B) (hA' : Continuous A') (hB' : Continuous B')
    (hA'' : Continuous A'') (hB'' : Continuous B'')
    (hz : ∀ ε ∈ Icc (-δ) δ, ∀ t ∈ Icc a b,
      endpointCorrectedPosition x y A B a b ε t ∈ (chartAt FourSpace c).target) :
    let X := fun p : ℝ × ℝ => endpointCorrectedPosition x y A B a b p.1 p.2
…

Mentions: OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition

theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_ofLp line 16946

theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrected_energy_secondDeriv line 16954

Source documentation

The corrected curve has an actual twice differentiable energy integral. All parameter derivatives come from the prescribed endpoint curves.

theorem endpointCorrected_energy_secondDeriv (g : SmoothMetric M) (c : M)
    (x y v w A B A' B' A'' B'' : ℝ → FourSpace) {a b δ : ℝ}
    (hδ : 0 < δ) (hab : a ≤ b)
    (hx : Continuous x) (hy : Continuous y) (hv : Continuous v) (hw : Continuous w)
    (hA : Continuous A) (hB : Continuous B) (hA' : Continuous A') (hB' : Continuous B')
    (hA'' : Continuous A'') (hB'' : Continuous B'')
    (hdA : ∀ ε ∈ Ioo (-δ) δ, HasDerivAt A (A' ε) ε)
    (hdB : ∀ ε ∈ Ioo (-δ) δ, HasDerivAt B (B' ε) ε)
    (hddA : ∀ ε ∈ Ioo (-δ) δ, HasDerivAt A' (A'' ε) ε)
    (hddB : ∀ ε ∈ Ioo (-δ) δ, HasDerivAt B' (B'' ε) ε)
    (hz : ∀ ε ∈ Icc (-δ) δ, ∀ t ∈ Icc a b,
      endpointCorrectedPosition x y A B a b ε t ∈ (chartAt FourSpace c).target) :
…

Mentions: OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition

def OAI.PositiveEinsteinFour.Geometry.twoFormHodgeMatrix line 17022
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeMatrix_apply line 17030
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeMatrix_trace line 17037
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeMatrix_involutive line 17040
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureMatrix_hodgeFirst line 17045
theorem OAI.PositiveEinsteinFour.Geometry.hodgeFirstTensor_firstSkew line 17052
theorem OAI.PositiveEinsteinFour.Geometry.hodgeFirstTensor_lastSkew line 17056
theorem OAI.PositiveEinsteinFour.Geometry.oneFormChartFamily_self line 17088
theorem OAI.PositiveEinsteinFour.Geometry.oneFormChartFamily_smooth line 17096
def OAI.PositiveEinsteinFour.Geometry.oneFormChartTest line 17136
theorem OAI.PositiveEinsteinFour.Geometry.oneFormChartTest_coordinates line 17143
theorem OAI.PositiveEinsteinFour.Geometry.oneFormChartTest_zero_off line 17151
def OAI.PositiveEinsteinFour.Geometry.twoCovariantAlternation line 17175
theorem OAI.PositiveEinsteinFour.Geometry.twoCovariantAlternation_apply line 17178
theorem OAI.PositiveEinsteinFour.Geometry.twoCovariantAlternation_skew line 17185
theorem OAI.PositiveEinsteinFour.Geometry.twoCovariantAlternation_frame line 17190
def OAI.PositiveEinsteinFour.Geometry.smoothCovariantAlternation line 17199
def OAI.PositiveEinsteinFour.Geometry.smoothOneFormExterior line 17207
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormExterior_framed line 17211
theorem OAI.PositiveEinsteinFour.Geometry.oneForm_squareNorm line 17240
theorem OAI.PositiveEinsteinFour.Geometry.oneForm_norm_integral line 17262
theorem OAI.PositiveEinsteinFour.Geometry.oneForm_eq_zero_of_norm_integral line 17272
theorem OAI.PositiveEinsteinFour.Geometry.orthogonal_three_fixed_vector line 17322
theorem OAI.PositiveEinsteinFour.Geometry.oriented_four_fixed_normal line 17340
theorem OAI.PositiveEinsteinFour.Geometry.exists_uniform_parallelFrame_time line 17401
theorem OAI.PositiveEinsteinFour.Geometry.continuous_integral_cauchy_schwarz line 17459

theorem OAI.PositiveEinsteinFour.Geometry.norm_gap_of_regularized_sobolev line 17474

Source documentation

A uniform positive fourth moment and arbitrarily small regularization errors turn the sharp scalar inequality into a norm gap.

theorem norm_gap_of_regularized_sobolev (v : C(Ω, ℝ)) (F : ℝ → C(Ω, ℝ))
    (E : ℝ → ℝ) (hv : ∀ x, 0 ≤ v x) (c : ℝ) (hc : 0 < c)
    (hminorant : ∀ ε > 0, c ≤ ∫ x, F ε x ^ 4 ∂μ)
    (hsob : ∀ ε > 0, Real.sqrt (∫ x, F ε x ^ 4 ∂μ) ≤
      (∫ x, F ε x ^ 2 ∂μ) + E ε / 2)
    (henergy : ∀ ε > 0, E ε + 2 * (∫ x, F ε x ^ 2 ∂μ) ≤
      2 * (∫ x, v x * F ε x ^ 2 ∂μ) + 2 * ε ^ (2 / 3 : ℝ)) :
    1 ≤ ∫ x, v x ^ 2 ∂μ := by
…

theorem OAI.PositiveEinsteinFour.Geometry.regularizedWeylRoot_fourth_lower line 17507
theorem OAI.PositiveEinsteinFour.Geometry.continuous_plusNorm line 17525
theorem OAI.PositiveEinsteinFour.Geometry.canonical_plusNorm_moment line 17532

theorem OAI.PositiveEinsteinFour.Geometry.plus_gap_of_regularized_sharp_sobolev line 17549

Source documentation

The sharp Sobolev premise is exposed explicitly. All other ingredients are the actual Weyl equation, canonical measure, and regularized energy.

theorem plus_gap_of_regularized_sharp_sobolev (g : SmoothMetric M) (o : FrameOrientation g)
    (d : MetricGreenData g (canonicalFrameMeasure g o))
    (hsob : ∀ (ε : ℝ) (hε : 0 < ε),
      Real.sqrt (∫ e, d.weylRootField ε e ^ 4 ∂canonicalFrameMeasure g o) ≤
        (∫ e, d.weylRootField ε e ^ 2 ∂canonicalFrameMeasure g o) +
          (∫ e, ∑ i, d.weylRootFirstField ε hε i e ^ 2
            ∂canonicalFrameMeasure g o) / 2)
    (hnonzero : ∃ x, plusNorm o x ≠ 0) :
    1 ≤ ∫ x, plusNorm o x ^ 2 ∂normalizedVolume g := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.plusNorm, OAI.PositiveEinsteinFour.Geometry.normalizedVolume

theorem OAI.PositiveEinsteinFour.Geometry.scalar_second_variation_decreases line 17624
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_deRham_curvature line 17672
def OAI.PositiveEinsteinFour.Geometry.twoFormGramTestTensor line 17732
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramTestTensor_smooth line 17736
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramTestTensor_skew line 17759
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramTestTensor_support line 17766
def OAI.PositiveEinsteinFour.Geometry.twoFormGramTest line 17778
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramTest_value line 17786
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramTest_nabla line 17799
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.covariantPairing_hodge_self line 17829
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCovariantEnergy_hodge line 17854
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner_hodge_self line 17862
def OAI.PositiveEinsteinFour.Geometry.smoothH1Hodge line 17871
structure OAI.PositiveEinsteinFour.Geometry.MetricFrameMoments line 17903
Source documentation
The actual frame moments in the normalization of balanced_moments: its volume variable is twice the round-sphere volume ratio.
```
structure MetricFrameMoments (d : MetricGreenData g μ) (o : OppositeWeylData d)
    (orientation : FrameOrientation g) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.OppositeWeylData, OAI.PositiveEinsteinFour.Geometry.FrameOrientation
theorem OAI.PositiveEinsteinFour.Geometry.frame_norm_moment_sum_lt_four line 17928
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.frameMomentData line 17964

theorem OAI.PositiveEinsteinFour.Geometry.MetricFrameMoments.balanced line 18025

Source documentation

The scalar moment obstruction applies to oriented-frame moments under the two H-variance bounds.

theorem MetricFrameMoments.balanced {d : MetricGreenData g μ} {o : OppositeWeylData d}
    {orientation : FrameOrientation g} (D : MetricFrameMoments d o orientation)
    (hp : ∃ e ∈ orientation.positive, d.plusNormField e ≠ 0)
    (hm : ∃ e ∈ orientation.positive, d.minusNormField o e ≠ 0)
    (hvp : (∫ e, MomentObstruction.H (d.plusNormField e) ^ 2 ∂μ) -
        (∫ e, MomentObstruction.H (d.plusNormField e) ∂μ) ^ 2 ≤
      (9 / 16 : ℝ) * ((∫ e, d.plusNormField e ^ 2 ∂μ) - ∫ e, d.plusNormField e ∂μ))
    (hvm : (∫ e, MomentObstruction.H (d.minusNormField o e) ^ 2 ∂μ) -
        (∫ e, MomentObstruction.H (d.minusNormField o e) ∂μ) ^ 2 ≤
      (9 / 16 : ℝ) * ((∫ e, d.minusNormField o e ^ 2 ∂μ) - ∫ e, d.minusNormField o e ∂μ)) :
    (∫ e, d.plusNormField e ^ 2 ∂μ) = (∫ e, d.minusNormField o e ^ 2 ∂μ) ∧
      D.plusCount = D.minusCount := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.MetricGreenData, OAI.PositiveEinsteinFour.Geometry.OppositeWeylData, OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.MetricFrameMoments, OAI.PositiveEinsteinFour.MomentObstruction.H

theorem OAI.PositiveEinsteinFour.Geometry.models_of_published_oriented_inputs line 18079
theorem OAI.PositiveEinsteinFour.Geometry.classified_of_published_oriented_inputs line 18129
def OAI.PositiveEinsteinFour.Geometry.endpointChartLine line 18167
def OAI.PositiveEinsteinFour.Geometry.endpointChartPosition line 18170
def OAI.PositiveEinsteinFour.Geometry.endpointChartFirst line 18174
def OAI.PositiveEinsteinFour.Geometry.endpointChartSecond line 18178
theorem OAI.PositiveEinsteinFour.Geometry.endpointChartPosition_zero line 18182
theorem OAI.PositiveEinsteinFour.Geometry.endpointChartFirst_zero line 18186
theorem OAI.PositiveEinsteinFour.Geometry.endpointChartSecond_zero line 18191
theorem OAI.PositiveEinsteinFour.Geometry.endpointChartPosition_symm line 18196
theorem OAI.PositiveEinsteinFour.Geometry.endpointChartLine_hasDerivAt line 18206
theorem OAI.PositiveEinsteinFour.Geometry.continuous_endpointChartLine line 18211
theorem OAI.PositiveEinsteinFour.Geometry.endpointChartPosition_hasDerivAt line 18216
theorem OAI.PositiveEinsteinFour.Geometry.endpointChartFirst_hasDerivAt line 18225
theorem OAI.PositiveEinsteinFour.Geometry.continuousAt_transitionFirst line 18238
theorem OAI.PositiveEinsteinFour.Geometry.continuousAt_transitionSecond line 18249
theorem OAI.PositiveEinsteinFour.Geometry.endpointChartJets_continuousAt line 18266
theorem OAI.PositiveEinsteinFour.Geometry.exists_endpointChartOverlap line 18282
theorem OAI.PositiveEinsteinFour.Geometry.intervalExtension_hasDerivAt line 18307

theorem OAI.PositiveEinsteinFour.Geometry.exists_endpointChartJets line 18318

Source documentation

Three globally continuous endpoint-jet functions agree with the actual chart transition on a common interval and have its genuine first and second parameter derivatives in the interior.

theorem exists_endpointChartJets (c d : M) (z : FourSpace)
    (y : JacobiCoordinateVector) (hz : z ∈ (chartAt FourSpace c).target)
    (hd : (chartAt FourSpace c).symm z ∈ (chartAt FourSpace d).source) :
    ∃ δ > 0, ∃ A A' A'' : ℝ → FourSpace,
      Continuous A ∧ Continuous A' ∧ Continuous A'' ∧
      (∀ s ∈ Ioo (-δ) δ, HasDerivAt A (A' s) s ∧ HasDerivAt A' (A'' s) s) ∧
      (∀ s ∈ Icc (-δ) δ,
        A s = endpointChartPosition c d z y s ∧
        A' s = endpointChartFirst c d z y s ∧ A'' s = endpointChartSecond c d z y s) ∧
      (∀ s ∈ Icc (-δ) δ,
        endpointChartLine z y s ∈ (chartAt FourSpace c).target ∧
        (chartAt FourSpace c).symm (endpointChartLine z y s) ∈ (chartAt FourSpace d).source) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.endpointChartPosition, OAI.PositiveEinsteinFour.Geometry.endpointChartFirst, OAI.PositiveEinsteinFour.Geometry.endpointChartSecond, OAI.PositiveEinsteinFour.Geometry.endpointChartLine

theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_timeField line 18379
theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_parameterField line 18384
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrected_jets_continuousOn line 18389
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrected_energy_continuousOnSegment line 18442
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_coordinateVector line 18479
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrected_energy_secondDerivOnSegment line 18485
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureMatrix_signed_trace line 18555
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureMatrix_signed_square_trace line 18567
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotentialMatrix_signed_square_trace line 18589
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotentialMatrix_signed_square line 18598
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldDerivative_add line 18627
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldDerivative_smul line 18641
def OAI.PositiveEinsteinFour.Geometry.twoCovariantAlternationLinear line 18652
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormExterior_apply line 18660
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormExterior_add line 18671
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormExterior_smul line 18691
def OAI.PositiveEinsteinFour.Geometry.smoothOneFormExteriorLinear line 18710
theorem OAI.PositiveEinsteinFour.Geometry.extend_parallelFrame_interval line 18734
theorem OAI.PositiveEinsteinFour.Geometry.exists_parallelFrame_arbitrary_interval line 18786
Source documentation
On a compact base, a genuine parallel-frame curve through any prescribed frame exists on every bounded open time interval.
```
theorem exists_parallelFrame_arbitrary_interval [CompactSpace M]
    (g : SmoothMetric M) (k : Fin 4) (e : FrameBundle g) (a : ℝ) :
    ∃ γ : ℝ → FrameBundle g, γ 0 = e ∧
      IsParallelFrameCurveOn g k γ (Ioo (-a) a) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.IsParallelFrameCurveOn
theorem OAI.PositiveEinsteinFour.Geometry.exists_global_intrinsic_parallelFrame line 18822
Source documentation
Compactness and uniqueness extend the actual horizontal ODE for all real times. Every derivative in the conclusion is still the original coordinate velocity/parallel equation, not an assumed tensor identity.
```
theorem exists_global_intrinsic_parallelFrame [CompactSpace M]
    (g : SmoothMetric M) (k : Fin 4) (e : FrameBundle g) :
    ∃ Γ : ℝ → FrameBundle g, Γ 0 = e ∧ Continuous Γ ∧
      ∀ t, ParallelFrameCurveAt g Γ k t := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.ParallelFrameCurveAt
theorem OAI.PositiveEinsteinFour.Geometry.twoFormDerivativeRows_pairing line 18874
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_weighted_rows_pairing line 18884
theorem OAI.PositiveEinsteinFour.Geometry.chartGramMatrix_mul_transpose_orthogonal line 18905
theorem OAI.PositiveEinsteinFour.Geometry.twoFormLocalNablaRows_pairing line 18915
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.covariantPairing_chart line 18926
def OAI.PositiveEinsteinFour.Geometry.twoFormH1Hodge line 18966
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1Hodge_smooth line 18969
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1Hodge_norm line 18973
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1Hodge_involutive line 18981
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1ToL2_hodge line 18990
def OAI.PositiveEinsteinFour.Geometry.twoFormInfinitesimalMatrix line 19018
theorem OAI.PositiveEinsteinFour.Geometry.twoFormInfinitesimalMatrix_action line 19026
theorem OAI.PositiveEinsteinFour.Geometry.twoFormInfinitesimalMatrix_square_trace line 19041
theorem OAI.PositiveEinsteinFour.Geometry.twoFormInfinitesimalMatrix_signed_square_trace line 19048
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMatrix_square_trace line 19056
theorem OAI.PositiveEinsteinFour.Geometry.twoFormInfinitesimalMatrix_euler_trace line 19063
def OAI.PositiveEinsteinFour.Geometry.twoFormSecondDeRham line 19085
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSecondDeRham_commutator line 19089
theorem OAI.PositiveEinsteinFour.Geometry.twoFormSecondDeRham_eq line 19106
theorem OAI.PositiveEinsteinFour.Geometry.exists_curve_second_jets line 19137
def OAI.PositiveEinsteinFour.Geometry.normalEndpointDirection line 19198
def OAI.PositiveEinsteinFour.Geometry.normalEndpointCurve line 19202
theorem OAI.PositiveEinsteinFour.Geometry.normalEndpoint_first_chart line 19207
theorem OAI.PositiveEinsteinFour.Geometry.normalEndpoint_position_zero line 19214
theorem OAI.PositiveEinsteinFour.Geometry.normalEndpoint_first_zero line 19222

theorem OAI.PositiveEinsteinFour.Geometry.exists_normalEndpointJets line 19231

Source documentation

The same endpoint curve can be represented in every adjacent chart, with actual continuous first and second jets and the required initial field.

theorem exists_normalEndpointJets (g : SmoothMetric M) (e : FrameBundle g)
    (c : M) (hc : e.base ∈ (chartAt FourSpace c).source) (a : Fin 3 → ℝ) :
    ∃ δ > 0, ∃ A A' A'' : ℝ → FourSpace,
      Continuous A ∧ Continuous A' ∧ Continuous A'' ∧
      A 0 = chartAt FourSpace c e.base ∧
      A' 0 = WithLp.toLp 2 (frameChartMatrix g c e *ᵥ Fin.cons 0 a) ∧
      A'' 0 = endpointChartSecond e.base c (chartAt FourSpace e.base e.base)
        (normalEndpointDirection g e a) 0 ∧
      (∀ ε ∈ Ioo (-δ) δ, HasDerivAt A (A' ε) ε ∧ HasDerivAt A' (A'' ε) ε) ∧
      (∀ ε ∈ Icc (-δ) δ,
        A ε ∈ (chartAt FourSpace c).target ∧
        (chartAt FourSpace c).symm (A ε) = normalEndpointCurve g e a ε) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix, OAI.PositiveEinsteinFour.Geometry.endpointChartSecond, OAI.PositiveEinsteinFour.Geometry.normalEndpointDirection, OAI.PositiveEinsteinFour.Geometry.normalEndpointCurve

def OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap line 19280
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_zero line 19284
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_curve_continuous line 19288
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_primitive line 19292
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_add line 19297
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_neg_left line 19317
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_neg_right line 19322
def OAI.PositiveEinsteinFour.Geometry.parallelFrameEquiv line 19328
Source documentation
The inverse at time t is the actual horizontal curve at time -t.
```
def parallelFrameEquiv (g : SmoothMetric M) (k : Fin 4) (t : ℝ) :
    FrameBundle g ≃ FrameBundle g where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle
structure OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData line 19355
def OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData.green line 19369
theorem OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData.opposite line 19373
theorem OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData.calculus line 19377
theorem OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData.norms line 19381
theorem OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData.folland line 19385
theorem OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData.volume line 19389
theorem OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData.compactFrames line 19394
def OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData.jacobi line 19399
theorem OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData.models line 19405
def OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureRow line 19434
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMatrix_curvatureRow line 19437
theorem OAI.PositiveEinsteinFour.Geometry.twoFormInfinitesimalMatrix_connection line 19444
def OAI.PositiveEinsteinFour.Geometry.ParallelMetricData.ofParallelFlows line 19489
Source documentation
Normalized Ricci curvature supplies the contraction field of the parallel-frame calculus.
```
def ParallelMetricData.ofParallelFlows (g : SmoothMetric M)
    (μ : Measure (FrameBundle g)) (flow : Fin 4 → FrameFlow g μ)
    (hcurve : ∀ k t e, ParallelFrameCurveAt g (fun s => (flow k).map s e) k t)
    (hRic : RicciThree g) : ParallelMetricData g μ where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.ParallelFrameCurveAt, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData
def OAI.PositiveEinsteinFour.Geometry.canonicalPublishedOrientedData line 19504
Source documentation
The canonical frame probability supplies the averaging and support fields, while the initial condition supplies orientation preservation.
```
def canonicalPublishedOrientedData (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o))
    (hzero : ∀ i e, (d.flow i).map 0 e = e)
    (hparallel : ParallelReflection d.toMetricGreenData)
    (poisson : PetersenPoissonInput g (canonicalFrameMeasure g o))
    (jacobi : JacobiRealizationData d.toMetricGreenData)
    (gap : GurskyLeBrunGapInput g o) (hodge : GurskyLeBrunHodgeInput g o)
    (model : DerdzinskiHitchinInput g o) : PublishedOrientedData g o where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.ParallelReflection, OAI.PositiveEinsteinFour.Geometry.PetersenPoissonInput, OAI.PositiveEinsteinFour.Geometry.JacobiRealizationData, OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunGapInput, OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunHodgeInput, OAI.PositiveEinsteinFour.Geometry.DerdzinskiHitchinInput, OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData
theorem OAI.PositiveEinsteinFour.Geometry.models_of_canonical_data line 19532
Source documentation
The oriented classification with the constructed frame probability. No independent spherical averaging, support, or orientation-preservation input remains in this specialization.
```
theorem models_of_canonical_data (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o))
    (hzero : ∀ i e, (d.flow i).map 0 e = e)
    (hparallel : ParallelReflection d.toMetricGreenData)
    (poisson : PetersenPoissonInput g (canonicalFrameMeasure g o))
    (jacobi : JacobiRealizationData d.toMetricGreenData)
    (gap : GurskyLeBrunGapInput g o) (hodge : GurskyLeBrunHodgeInput g o)
    (model : DerdzinskiHitchinInput g o)
    (hEinstein : IsEinstein g) (hpositive : HasPositiveSectionalCurvature g) :
    ∃ a : ℝ, 0 < a ∧ (ScaledIsometricTo g a roundDistance ∨
      ScaledIsometricTo g a fubiniStudyDistance) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.ParallelReflection, OAI.PositiveEinsteinFour.Geometry.PetersenPoissonInput, OAI.PositiveEinsteinFour.Geometry.JacobiRealizationData, OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunGapInput, OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunHodgeInput, OAI.PositiveEinsteinFour.Geometry.DerdzinskiHitchinInput
def OAI.PositiveEinsteinFour.Geometry.twoFormConnectionCurvatureMatrix line 19563
def OAI.PositiveEinsteinFour.Geometry.oneFormConnectionCurvatureMatrix line 19566
theorem OAI.PositiveEinsteinFour.Geometry.connectionCurvature_euler_trace line 19569
theorem OAI.PositiveEinsteinFour.Geometry.sum_four_components_connection line 19580
theorem OAI.PositiveEinsteinFour.Geometry.sum_pair_flip line 19586
theorem OAI.PositiveEinsteinFour.Geometry.curvatureRow_hodge_pairing line 19592
theorem OAI.PositiveEinsteinFour.Geometry.connectionCurvature_signature_trace line 19609
def OAI.PositiveEinsteinFour.Geometry.PetersenPositiveRicciInput line 19652
Source documentation
The one positive Ricci entry needed to show the Einstein constant is positive; it is the contraction of three strictly positive sectional terms.
```
def PetersenPositiveRicciInput (g : SmoothMetric M) : Prop :=
…
```
def OAI.PositiveEinsteinFour.Geometry.PetersenScalingInput line 19657
Source documentation
Constant metric rescaling, in actual chart tensors and actual distance. No Einstein normalization or model conclusion is included.
```
def PetersenScalingInput (g : SmoothMetric M) : Prop :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.einstein_of_ricciThree line 19666
theorem OAI.PositiveEinsteinFour.Geometry.normalized_oriented_metric line 19671
theorem OAI.PositiveEinsteinFour.Geometry.models_of_published_inputs line 19704
theorem OAI.PositiveEinsteinFour.Geometry.normalEndpoint_velocity_chart line 19748
def OAI.PositiveEinsteinFour.Geometry.normalEndpointBoundary line 19757
theorem OAI.PositiveEinsteinFour.Geometry.normalEndpoint_boundary_chart line 19761
theorem OAI.PositiveEinsteinFour.Geometry.normalEndpointBoundary_zero line 19782
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_eq_local line 19812
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_continuousAt_zero line 19831
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_uniform_continuous_time line 19847
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_continuous_slice line 19882
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_continuous line 19914
def OAI.PositiveEinsteinFour.Geometry.parallelFrameHomeomorph line 19934
Source documentation
The actual parallel flow gives homeomorphisms, with inverse at negative time.
```
def parallelFrameHomeomorph (g : SmoothMetric M) (k : Fin 4) (t : ℝ) :
    FrameBundle g ≃ₜ FrameBundle g where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_reflection line 19961
theorem OAI.PositiveEinsteinFour.Geometry.frameChartMatrix_rotate line 20007
theorem OAI.PositiveEinsteinFour.Geometry.rotated_column line 20017
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameCurveAt_rotate line 20023
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_rotate line 20070
theorem OAI.PositiveEinsteinFour.Geometry.coordinateVector_pair_independent line 20108
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.map_coordinateVector line 20119
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvature_plane_pos line 20124
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.ricci_eq_scalar line 20132
theorem OAI.PositiveEinsteinFour.Geometry.einstein_constant_positive line 20137
theorem OAI.PositiveEinsteinFour.Geometry.positiveRicciInput_of_einstein line 20160
Source documentation
The exact published positivity input is discharged for the Einstein metrics to which the classification proof applies.
```
theorem positiveRicciInput_of_einstein [Nonempty M] (hEinstein : IsEinstein g) :
    PetersenPositiveRicciInput g := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.PetersenPositiveRicciInput

theorem OAI.PositiveEinsteinFour.Geometry.models_of_scaling_and_normalized_data line 20175

Source documentation

The oriented application uses Ricci positivity derived from chart curvature.

theorem models_of_scaling_and_normalized_data (g : SmoothMetric M)
    (orientation : FrameOrientation g) (hscaling : PetersenScalingInput g)
    (hdata : ∀ (h : SmoothMetric M) (o : FrameOrientation h),
      RicciThree h → IsEinstein h → HasPositiveSectionalCurvature h →
        Nonempty (PublishedOrientedData h o))
    (hEinstein : IsEinstein g) (hpositive : HasPositiveSectionalCurvature g) :
    ∃ a : ℝ, 0 < a ∧ (ScaledIsometricTo g a roundDistance ∨
      ScaledIsometricTo g a fubiniStudyDistance) :=
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.PetersenScalingInput, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData

def OAI.PositiveEinsteinFour.Geometry.hodgeEulerTracePolynomial line 20204
def OAI.PositiveEinsteinFour.Geometry.hodgeSignatureTracePolynomial line 20211
theorem OAI.PositiveEinsteinFour.Geometry.actual_hodgeEulerTracePolynomial line 20219
theorem OAI.PositiveEinsteinFour.Geometry.actual_hodgeSignatureTracePolynomial line 20237
def OAI.PositiveEinsteinFour.Geometry.rescaleMetric line 20278
theorem OAI.PositiveEinsteinFour.Geometry.rescaleMetric_inner line 20301
theorem OAI.PositiveEinsteinFour.Geometry.metricInChart_rescaleMetric line 20305
theorem OAI.PositiveEinsteinFour.Geometry.partialDeriv_const_mul line 20311
theorem OAI.PositiveEinsteinFour.Geometry.matrix_inv_const_smul line 20317
theorem OAI.PositiveEinsteinFour.Geometry.inverse_scale_product line 20325
theorem OAI.PositiveEinsteinFour.Geometry.christoffel_rescaleMetric line 20329
theorem OAI.PositiveEinsteinFour.Geometry.curvatureComponent_rescaleMetric line 20340
theorem OAI.PositiveEinsteinFour.Geometry.chartMetric_rescaleMetric line 20346
theorem OAI.PositiveEinsteinFour.Geometry.chartRicci_rescaleMetric line 20350
theorem OAI.PositiveEinsteinFour.Geometry.sectionalNumerator_rescaleMetric line 20355
theorem OAI.PositiveEinsteinFour.Geometry.orientedDirection_one line 20381
def OAI.PositiveEinsteinFour.Geometry.normalRotationSubgroup line 20387
abbrev OAI.PositiveEinsteinFour.Geometry.NormalFrameRotation line 20400
theorem OAI.PositiveEinsteinFour.Geometry.isClosed_normalRotationSubgroup line 20402
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 20413) line 20413
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 20416) line 20416
def OAI.PositiveEinsteinFour.Geometry.normalFrameHaar line 20420
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 20422) line 20422
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 20426) line 20426
theorem OAI.PositiveEinsteinFour.Geometry.normalFrameHaar_left line 20429
theorem OAI.PositiveEinsteinFour.Geometry.normalFrameRotation_column line 20433
theorem OAI.PositiveEinsteinFour.Geometry.mem_normalRotationSubgroup_of_column line 20440
def OAI.PositiveEinsteinFour.Geometry.normalFrameRotate line 20451
def OAI.PositiveEinsteinFour.Geometry.normalFrameChange line 20455
theorem OAI.PositiveEinsteinFour.Geometry.normalFrameRotate_change line 20461
theorem OAI.PositiveEinsteinFour.Geometry.continuous_normalFrameRotate line 20468
theorem OAI.PositiveEinsteinFour.Geometry.normalFrameRotate_mul line 20473
theorem OAI.PositiveEinsteinFour.Geometry.normalFrameRotate_one line 20478
def OAI.PositiveEinsteinFour.Geometry.normalFrameHomeomorph line 20481
theorem OAI.PositiveEinsteinFour.Geometry.normalFrameRotate_first line 20496
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_normalFrameRotate line 20503

theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_same_first line 20513

Source documentation

The transported base point and first vector are independent of the chosen positive normal frame. This gives the descent of the constructed frame flow to geodesic data.

theorem parallelFrameFlowMap_same_first [T2Space M] [CompactSpace M]
    (g : SmoothMetric M) {c : M} (e f : OrthonormalFrame g c)
    (hdet : 0 < e.matrix.det * f.matrix.det) (hfirst : e.vector 0 = f.vector 0)
    (t : ℝ) :
    (parallelFrameFlowMap g 0 t ⟨c, e⟩).base =
        (parallelFrameFlowMap g 0 t ⟨c, f⟩).base ∧
      (parallelFrameFlowMap g 0 t ⟨c, e⟩).frame.vector 0 =
        (parallelFrameFlowMap g 0 t ⟨c, f⟩).frame.vector 0 := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap

theorem OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure_normalFrameRotate line 20538
def OAI.PositiveEinsteinFour.Geometry.normalEndpointAcceleration line 20560
def OAI.PositiveEinsteinFour.Geometry.normalEndpointQuadratic line 20565
def OAI.PositiveEinsteinFour.Geometry.normalQuadraticEndpointCurve line 20570
theorem OAI.PositiveEinsteinFour.Geometry.normalEndpointQuadratic_zero line 20574
theorem OAI.PositiveEinsteinFour.Geometry.normalEndpointQuadratic_hasDerivAt line 20578
theorem OAI.PositiveEinsteinFour.Geometry.normalEndpointQuadratic_contDiff line 20589
theorem OAI.PositiveEinsteinFour.Geometry.normal_quadratic_boundary_zero line 20594
structure OAI.PositiveEinsteinFour.Geometry.NormalQuadraticJetData line 20601
theorem OAI.PositiveEinsteinFour.Geometry.exists_normalQuadraticJetData line 20622
def OAI.PositiveEinsteinFour.Geometry.frameCotangentState line 20727
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameCurveAt_cotangent line 20732
theorem OAI.PositiveEinsteinFour.Geometry.frameCotangentState_energy line 20753
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_cotangent_derivative line 20763

theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_eq_kineticLocalFlow line 20775

Source documentation

Wherever a global frame trajectory remains in a fixed chart, its cotangent state is the actual local unit-Jacobian Hamiltonian flow.

theorem parallelFrameFlowMap_eq_kineticLocalFlow (g : SmoothMetric M) (c : M)
    (k : Fin 4) (e : FrameBundle g) (p : CotangentCoordinates)
    (F : KineticLocalFlow g c p)
    (hq : frameCotangentState g c k e ∈ Metric.ball p F.radius)
    (hchart : ∀ t ∈ Ioo (-F.time) F.time,
      (parallelFrameFlowMap g k t e).base ∈ (chartAt FourSpace c).source) :
    EqOn (fun t => F.map (frameCotangentState g c k e, t))
      (fun t => frameCotangentState g c k (parallelFrameFlowMap g k t e))
      (Ioo (-F.time) F.time) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow, OAI.PositiveEinsteinFour.Geometry.frameCotangentState, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap

theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameCurveAt_directionChange line 20810
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_directionChange line 20854
def OAI.PositiveEinsteinFour.Geometry.coordinateDirection line 20872
theorem OAI.PositiveEinsteinFour.Geometry.coordinateDirection_apply line 20875
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_preserves_of_first line 20882
def OAI.PositiveEinsteinFour.Geometry.actualFrameFlow line 20922
theorem OAI.PositiveEinsteinFour.Geometry.actualFrameFlow_apply line 20929
def OAI.PositiveEinsteinFour.Geometry.actualParallelMetricData line 20935
theorem OAI.PositiveEinsteinFour.Geometry.actualParallelMetricData_zero line 20941
theorem OAI.PositiveEinsteinFour.Geometry.actualParallelMetricData_reflection line 20948
def OAI.PositiveEinsteinFour.Geometry.actualCanonicalPublishedOrientedData line 20959
Source documentation
The complete flow preserves canonical base-volume times orthonormal-fiber probability under the measure-preservation hypothesis.
```
def actualCanonicalPublishedOrientedData (g : SmoothMetric M) (o : FrameOrientation g)
    (hpres : ∀ k t, MeasurePreserving (parallelFrameFlowMap g k t)
      (canonicalFrameMeasure g o) (canonicalFrameMeasure g o))
    (hRic : RicciThree g)
    (poisson : PetersenPoissonInput g (canonicalFrameMeasure g o))
    (jacobi : JacobiRealizationData
      (actualParallelMetricData g (canonicalFrameMeasure g o) hpres hRic).toMetricGreenData)
    (gap : GurskyLeBrunGapInput g o) (hodge : GurskyLeBrunHodgeInput g o)
    (model : DerdzinskiHitchinInput g o) : PublishedOrientedData g o :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.PetersenPoissonInput, OAI.PositiveEinsteinFour.Geometry.JacobiRealizationData, OAI.PositiveEinsteinFour.Geometry.actualParallelMetricData, OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunGapInput, OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunHodgeInput, OAI.PositiveEinsteinFour.Geometry.DerdzinskiHitchinInput, OAI.PositiveEinsteinFour.Geometry.PublishedOrientedData
def OAI.PositiveEinsteinFour.Geometry.actualFirstParallelMetricData line 20974
theorem OAI.PositiveEinsteinFour.Geometry.models_of_actual_parallel_data line 20983
theorem OAI.PositiveEinsteinFour.Geometry.models_of_actual_first_flow line 21000
Source documentation
Fixed oriented rotations reduce the Brin--Karcher measure-preservation hypothesis to the first frame flow.
```
theorem models_of_actual_first_flow (g : SmoothMetric M) (o : FrameOrientation g)
    (hfirst : ∀ t, MeasurePreserving (parallelFrameFlowMap g 0 t)
      (canonicalFrameMeasure g o) (canonicalFrameMeasure g o))
    (hRic : RicciThree g)
    (poisson : PetersenPoissonInput g (canonicalFrameMeasure g o))
    (jacobi : JacobiRealizationData (actualFirstParallelMetricData g o hfirst hRic).toMetricGreenData)
    (gap : GurskyLeBrunGapInput g o) (hodge : GurskyLeBrunHodgeInput g o)
    (model : DerdzinskiHitchinInput g o)
    (hEinstein : IsEinstein g) (hpositive : HasPositiveSectionalCurvature g) :
    ∃ a : ℝ, 0 < a ∧ (ScaledIsometricTo g a roundDistance ∨
      ScaledIsometricTo g a fubiniStudyDistance) :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.PetersenPoissonInput, OAI.PositiveEinsteinFour.Geometry.JacobiRealizationData, OAI.PositiveEinsteinFour.Geometry.actualFirstParallelMetricData, OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunGapInput, OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunHodgeInput, OAI.PositiveEinsteinFour.Geometry.DerdzinskiHitchinInput
theorem OAI.PositiveEinsteinFour.Geometry.metricTangentNorm_rescaleMetric line 21034
theorem OAI.PositiveEinsteinFour.Geometry.metricTangentENorm_rescaleMetric line 21041
theorem OAI.PositiveEinsteinFour.Geometry.metricEDistance_rescaleMetric line 21048
theorem OAI.PositiveEinsteinFour.Geometry.scaledEDistance_rescaleMetric line 21058
def OAI.PositiveEinsteinFour.Geometry.normalIntegralLinear line 21084
def OAI.PositiveEinsteinFour.Geometry.normalIntegralCLM line 21091
def OAI.PositiveEinsteinFour.Geometry.normalFrameAverage line 21100
theorem OAI.PositiveEinsteinFour.Geometry.normalFrameAverage_rotate line 21103
theorem OAI.PositiveEinsteinFour.Geometry.normalFrameAverage_same_first line 21113
Source documentation
The normal average depends only on the base point, first unit vector and orientation, not on the chosen three-vector normal frame.
```
theorem normalFrameAverage_same_first (F : FrameBundle g → ℝ) {c : M}
    (e f : OrthonormalFrame g c) (hdet : 0 < e.matrix.det * f.matrix.det)
    (hfirst : e.vector 0 = f.vector 0) :
    normalFrameAverage F (⟨c, e⟩ : FrameBundle g) =
      normalFrameAverage F (⟨c, f⟩ : FrameBundle g) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.normalFrameAverage
theorem OAI.PositiveEinsteinFour.Geometry.normalFrameAverage_parallel line 21123
theorem OAI.PositiveEinsteinFour.Geometry.continuous_normalFrameAverage line 21132
theorem OAI.PositiveEinsteinFour.Geometry.integral_normalFrameAverage line 21143
Source documentation
Normal-fiber averaging preserves the integral against the actual canonical oriented-frame probability.
```
theorem integral_normalFrameAverage (o : FrameOrientation g)
    (f : FrameBundle g → ℝ) (hf : Continuous f) :
    (∫ e, normalFrameAverage f e ∂canonicalFrameMeasure g o) =
      ∫ e, f e ∂canonicalFrameMeasure g o := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.normalFrameAverage, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure
theorem OAI.PositiveEinsteinFour.Geometry.integral_parallel_eq_normalAverage line 21165
Source documentation
A transported frame test function has the same integral as its normal-fiber average. Together with normalFrameAverage_same_first, this gives an integral on the unit tangent bundle.
```
theorem integral_parallel_eq_normalAverage (o : FrameOrientation g)
    (f : FrameBundle g → ℝ) (hf : Continuous f) (t : ℝ) :
    (∫ e, f (parallelFrameFlowMap g 0 t e) ∂canonicalFrameMeasure g o) =
      ∫ e, normalFrameAverage f (parallelFrameFlowMap g 0 t e)
        ∂canonicalFrameMeasure g o := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.normalFrameAverage
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadratic_boundary_chart_zero line 21194
theorem OAI.PositiveEinsteinFour.Geometry.frameCotangentState_continuousAt line 21236
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.time_subset line 21264
def OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.restrictTime line 21270
Source documentation
Restrict only the time interval of a constructed local flow.
```
def restrictTime (F : KineticLocalFlow g c p) (δ : ℝ)
    (hδ : 0 < δ) (hδF : δ ≤ F.time) : KineticLocalFlow g c p where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow

theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_chart_neighborhood line 21294

Source documentation

Nearby initial frames stay in one fixed chart for a common time.

theorem parallelFrameFlowMap_chart_neighborhood (g : SmoothMetric M) (c : M)
    (k : Fin 4) (e : FrameBundle g)
    (he : e.base ∈ (chartAt FourSpace c).source) :
    ∃ U : Set (FrameBundle g), IsOpen U ∧ e ∈ U ∧
      ∃ δ > (0 : ℝ), ∀ f ∈ U, ∀ t ∈ Ioo (-δ) δ,
        (parallelFrameFlowMap g k t f).base ∈ (chartAt FourSpace c).source := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap

theorem OAI.PositiveEinsteinFour.Geometry.exists_parallelFrame_localHamiltonian line 21319

Source documentation

Local Hamiltonian realization of the actual frame flow, simultaneously for an open set of nearby initial frames. Its Jacobian and volume properties are the already proved properties of KineticLocalFlow.

theorem exists_parallelFrame_localHamiltonian (g : SmoothMetric M) (c : M)
    (k : Fin 4) (e : FrameBundle g)
    (he : e.base ∈ (chartAt FourSpace c).source) :
    ∃ U : Set (FrameBundle g), IsOpen U ∧ e ∈ U ∧
      ∃ F : KineticLocalFlow g c (frameCotangentState g c k e),
        (∀ f ∈ U, frameCotangentState g c k f ∈
          Metric.ball (frameCotangentState g c k e) F.radius) ∧
        (∀ f ∈ U, ∀ t ∈ Ioo (-F.time) F.time,
          (parallelFrameFlowMap g k t f).base ∈ (chartAt FourSpace c).source) ∧
        (∀ f ∈ U, EqOn (fun t => F.map (frameCotangentState g c k f, t))
          (fun t => frameCotangentState g c k (parallelFrameFlowMap g k t f))
          (Ioo (-F.time) F.time)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow, OAI.PositiveEinsteinFour.Geometry.frameCotangentState, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap

theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.inner_map_self line 21377
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.inner_vector_self line 21388
structure OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle line 21394
theorem OAI.PositiveEinsteinFour.Geometry.unitTangent_ext line 21399
def OAI.PositiveEinsteinFour.Geometry.unitTangentRealization line 21410
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 21413) line 21413
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 21416) line 21416
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 21419) line 21419
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRealization_injective line 21421
def OAI.PositiveEinsteinFour.Geometry.unitTangentOfFrame line 21430
theorem OAI.PositiveEinsteinFour.Geometry.continuous_unitTangentOfFrame line 21433
theorem OAI.PositiveEinsteinFour.Geometry.unitTangent_metric_norm line 21438
theorem OAI.PositiveEinsteinFour.Geometry.exists_positive_unitTangent_frame line 21444
Source documentation
Every intrinsic unit tangent vector admits an oriented orthonormal completion, so the first-vector projection loses only the normal frame.
```
theorem exists_positive_unitTangent_frame (g : SmoothMetric M) (o : FrameOrientation g)
    (u : UnitTangentBundle g) :
    ∃ e : FrameBundle g, e ∈ o.positive ∧ unitTangentOfFrame e = u := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.unitTangentOfFrame
def OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure line 21465
instance OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure_probability line 21469
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentOfFrame_measurePreserving line 21474
def OAI.PositiveEinsteinFour.Geometry.jacobiZeroData line 21500
def OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvature line 21505
def OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvatureDerivative line 21509
theorem OAI.PositiveEinsteinFour.Geometry.actual_frameCurvature_continuous line 21513
theorem OAI.PositiveEinsteinFour.Geometry.actual_frameCurvatureDerivative_continuous line 21519
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvature_continuous line 21525
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvatureDerivative_continuous line 21531
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvature_hasDerivAt line 21538
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvature_symmetric line 21551
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvature_bounded line 21555
theorem OAI.PositiveEinsteinFour.Geometry.exists_actualJacobiSolution line 21564
def OAI.PositiveEinsteinFour.Geometry.actualJacobiSolution line 21569
theorem OAI.PositiveEinsteinFour.Geometry.exists_actualRegularJacobi line 21573
def OAI.PositiveEinsteinFour.Geometry.actualRegularJacobi line 21582
theorem OAI.PositiveEinsteinFour.Geometry.actualRegularJacobi_R line 21586
theorem OAI.PositiveEinsteinFour.Geometry.actualRegularJacobi_J line 21591
theorem OAI.PositiveEinsteinFour.Geometry.actualRegularJacobi_V line 21596
theorem OAI.PositiveEinsteinFour.Geometry.frame_scaling_identity line 21621
def OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.scaleBetween line 21626
Source documentation
Scale frame vectors when the metric matrices have the inverse square relation.
```
def OrthonormalFrame.scaleBetween {g h : SmoothMetric M} {x : M}
    (e : OrthonormalFrame g x) (a : ℝ)
    (ha : (a ^ 2) • chartMetric h x = chartMetric g x) : OrthonormalFrame h x where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.chartMetric
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.scaleBetween_vector line 21632
def OAI.PositiveEinsteinFour.Geometry.scaleFrameBundle line 21639
theorem OAI.PositiveEinsteinFour.Geometry.continuous_scaleFrameBundle line 21644
theorem OAI.PositiveEinsteinFour.Geometry.det_scale_product_pos_iff line 21654
def OAI.PositiveEinsteinFour.Geometry.rescaleFrameOrientation line 21663
theorem OAI.PositiveEinsteinFour.Geometry.petersenScalingInput line 21703
def OAI.PositiveEinsteinFour.Geometry.radialFrameCotangentState line 21732
theorem OAI.PositiveEinsteinFour.Geometry.radialFrameCotangentState_continuousAt line 21736
theorem OAI.PositiveEinsteinFour.Geometry.radialFrameFlowMap_cotangent_derivative line 21746
theorem OAI.PositiveEinsteinFour.Geometry.radialFrameFlowMap_chart_neighborhood line 21758

theorem OAI.PositiveEinsteinFour.Geometry.exists_radialFrame_localHamiltonian line 21787

Source documentation

Positive, zero and negative radii all give actual local Hamiltonian trajectories. Restricting to positive radii supplies the energy-shell chart.

theorem exists_radialFrame_localHamiltonian (g : SmoothMetric M) (c : M)
    (k : Fin 4) (r : ℝ) (e : FrameBundle g)
    (he : e.base ∈ (chartAt FourSpace c).source) :
    ∃ U : Set (ℝ × FrameBundle g), IsOpen U ∧ (r, e) ∈ U ∧
      ∃ F : KineticLocalFlow g c (radialFrameCotangentState g c k (r, e)),
        (∀ p ∈ U, radialFrameCotangentState g c k p ∈
          Metric.ball (radialFrameCotangentState g c k (r, e)) F.radius) ∧
        (∀ p ∈ U, EqOn (fun t => F.map (radialFrameCotangentState g c k p, t))
          (fun t => radialFrameCotangentState g c k
            (p.1, parallelFrameFlowMap g k (p.1 * t) p.2)) (Ioo (-F.time) F.time)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow, OAI.PositiveEinsteinFour.Geometry.radialFrameCotangentState, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap

theorem OAI.PositiveEinsteinFour.Geometry.orientedDirection_first_apply line 21839
theorem OAI.PositiveEinsteinFour.Geometry.orientedDirection_first_measurePreserving line 21845
def OAI.PositiveEinsteinFour.Geometry.unitTangentTurn line 21864
theorem OAI.PositiveEinsteinFour.Geometry.continuous_unitTangentTurn line 21867
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentTurn_first line 21873
theorem OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure_eq_section line 21891
Source documentation
Spherical disintegration is valid in any measurable positive frame section, including sections obtained by switching to a local Gram frame.
```
theorem canonicalUnitTangentMeasure_eq_section (g : SmoothMetric M) (o : FrameOrientation g)
    (s : M → FrameBundle g) (hs : Measurable s)
    (hbase : ∀ x, (s x).base = x) (hpos : ∀ x, s x ∈ o.positive) :
    canonicalUnitTangentMeasure g o =
      Measure.map (fun p : M × Directions => unitTangentTurn (s p.1) p.2)
        ((normalizedVolume g).prod sphereMeasure) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure, OAI.PositiveEinsteinFour.Geometry.unitTangentTurn, OAI.PositiveEinsteinFour.Geometry.normalizedVolume
theorem OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure_eq_spherical line 21915
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_positive line 21945
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentOfFrame_flow_eq line 21953
def OAI.PositiveEinsteinFour.Geometry.unitTangentFrame line 21970
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentFrame_positive line 21975
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentOfFrame_lift line 21980
def OAI.PositiveEinsteinFour.Geometry.unitTangentFlowMap line 21984
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentFlowMap_of_frame line 21988
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentFlowMap_zero line 21995
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentFlowMap_add line 21999
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.unique line 22031
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvature_joint_continuous line 22063
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvatureDerivative_joint_continuous line 22068
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiSolution_unique line 22074
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiState_joint_continuous line 22080
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiJ_joint_continuous line 22101
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiV_joint_continuous line 22105
def OAI.PositiveEinsteinFour.OrientedPublishedInputs line 22130
Source documentation
The classical hypotheses on a closed oriented metric, using its canonical Borel measurable structure.
```
def OrientedPublishedInputs (X : ClosedOrientedMetricFour.{u}) : Prop :=
…
```
theorem OAI.PositiveEinsteinFour.OrientedPublishedInputs.models line 22137
structure OAI.PositiveEinsteinFour.ClassificationPublishedInputs line 22152
Source documentation
Precisely the classical oriented metric identities and the classical orientation-cover/Euler inputs required by the full proof.
```
structure ClassificationPublishedInputs : Prop where
…
```
theorem OAI.PositiveEinsteinFour.classificationOn_of_published_inputs line 22160
Source documentation
Full conditional main result: every closed connected positively curved Einstein four-manifold is, up to positive scaling and isometry, S4, CP2 or RP4.
```
theorem classificationOn_of_published_inputs (h : ClassificationPublishedInputs M) :
    ClassificationOn M := by
…
```
Mentions: OAI.PositiveEinsteinFour.ClassificationPublishedInputs, OAI.PositiveEinsteinFour.ClassificationOn
def OAI.PositiveEinsteinFour.Jacobi.jacobiColumn line 22184
def OAI.PositiveEinsteinFour.Jacobi.jacobiColumnLinear line 22187
theorem OAI.PositiveEinsteinFour.Jacobi.mul_jacobiColumn line 22196
theorem OAI.PositiveEinsteinFour.Jacobi.hasDerivAt_jacobiColumn line 22205

theorem OAI.PositiveEinsteinFour.Jacobi.normal_jacobi_eq_mulVec line 22212

Source documentation

A normal vector solution with initial position zero and velocity w is the action of the matrix solution on w.

theorem normal_jacobi_eq_mulVec {R : ℝ → NormalMatrix}
    (d : MatrixJacobiSolution R) (K : ℝ≥0) (hK : ∀ s, ‖R s‖ ≤ K)
    (y z : ℝ → Fin 3 → ℝ) (w : Fin 3 → ℝ) (a b : ℝ)
    (hzero : (0 : ℝ) ∈ Ioo a b) (hy0 : y 0 = 0) (hz0 : z 0 = w)
    (hy : ∀ s ∈ Ioo a b, HasDerivAt y (z s) s)
    (hz : ∀ s ∈ Ioo a b, HasDerivAt z (-(R s *ᵥ y s)) s) :
    ∀ s ∈ Ioo a b, y s = d.J s *ᵥ w ∧ z s = d.V s *ᵥ w := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution

theorem OAI.PositiveEinsteinFour.Geometry.actual_normal_jacobi_eq_mulVec line 22274

Source documentation

The Jacobi coefficient is the curvature along the parallel-frame flow.

theorem actual_normal_jacobi_eq_mulVec (g : SmoothMetric M) (hRic : RicciThree g)
    (e : FrameBundle g) (y z : ℝ → Fin 3 → ℝ) (w : Fin 3 → ℝ) (a b : ℝ)
    (hzero : (0 : ℝ) ∈ Ioo a b) (hy0 : y 0 = 0) (hz0 : z 0 = w)
    (hy : ∀ s ∈ Ioo a b, HasDerivAt y (z s) s)
    (hz : ∀ s ∈ Ioo a b, HasDerivAt z
      (-((1 + frameCurvatureField g (parallelFrameFlowMap g 0 s e)) *ᵥ y s)) s) :
    ∀ s ∈ Ioo a b,
      y s = (actualJacobiSolution g hRic e).J s *ᵥ w ∧
      z s = (actualJacobiSolution g hRic e).V s *ᵥ w := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameCurvatureField, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap, OAI.PositiveEinsteinFour.Geometry.actualJacobiSolution

theorem OAI.PositiveEinsteinFour.Geometry.actual_geodesic_normal_identification line 22290

Source documentation

The coordinate first variation of an actual geodesic is identified with actualJacobiSolution, after taking inverse parallel-frame components. The differential equations are the geodesic and variational equations.

theorem actual_geodesic_normal_identification (g : SmoothMetric M)
    (hRic : RicciThree g) (c : M) (e : FrameBundle g)
    (γ Z : ℝ → FourSpace × FourSpace) (w : Fin 3 → ℝ) (a b : ℝ)
    (hzero : (0 : ℝ) ∈ Ioo a b)
    (hc : ∀ s ∈ Ioo a b,
      (parallelFrameFlowMap g 0 s e).base ∈ (chartAt FourSpace c).source)
    (hposition : ∀ s ∈ Ioo a b, (γ s).1 =
      chartAt FourSpace c (parallelFrameFlowMap g 0 s e).base)
    (hvelocity : ∀ s ∈ Ioo a b, WithLp.ofLp (γ s).2 =
      fun i => frameChartMatrix g c (parallelFrameFlowMap g 0 s e) i 0)
    (hγ : ∀ s ∈ Ioo a b, HasDerivAt γ (geodesicCoordinateField g c (γ s)) s)
    (hZ : ∀ s ∈ Ioo a b, HasDerivAt Z
…

Mentions: OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix, OAI.PositiveEinsteinFour.Geometry.geodesicCoordinateField

def OAI.PositiveEinsteinFour.Geometry.unitTangentFiberMeasure line 22348
theorem OAI.PositiveEinsteinFour.Geometry.orthogonalDirection_value line 22351
theorem OAI.PositiveEinsteinFour.Geometry.frame_map_change line 22355
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentTurn_vector line 22362
Distinct definitions of this name: OAI/Geometry/EinsteinFour/GeodesicGeometry04.lean:12295 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.unitTangentTurn_vector@path.
theorem OAI.PositiveEinsteinFour.Geometry.continuous_unitTangentTurn_fixed line 22366
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentTurn_change_matrix line 22374
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentTurn_change line 22387
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentFiberMeasure_eq line 22394
theorem OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure_eq_any_section line 22418
Source documentation
Orientation is irrelevant for the projected spherical measure, so any measurable orthonormal frame section computes this same probability.
```
theorem canonicalUnitTangentMeasure_eq_any_section (g : SmoothMetric M)
    (o : FrameOrientation g) (s : M → FrameBundle g) (hs : Measurable s)
    (hbase : ∀ x, (s x).base = x) :
    canonicalUnitTangentMeasure g o =
      Measure.map (fun p : M × Directions => unitTangentTurn (s p.1) p.2)
        ((normalizedVolume g).prod sphereMeasure) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure, OAI.PositiveEinsteinFour.Geometry.unitTangentTurn, OAI.PositiveEinsteinFour.Geometry.normalizedVolume
theorem OAI.PositiveEinsteinFour.Geometry.tangentBundle_t2 line 22469
theorem OAI.PositiveEinsteinFour.Geometry.isEmbedding_unitTangentRealization line 22487
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 22492) line 22492
def OAI.PositiveEinsteinFour.Geometry.positiveFirstProjection line 22498
theorem OAI.PositiveEinsteinFour.Geometry.positiveFirstProjection_surjective line 22502
theorem OAI.PositiveEinsteinFour.Geometry.positiveFirstProjection_quotient line 22508
theorem OAI.PositiveEinsteinFour.Geometry.compact_unitTangentBundle line 22517
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentFlowMap_continuous line 22525
def OAI.PositiveEinsteinFour.Geometry.unitTangentHomeomorph line 22536
instance OAI.PositiveEinsteinFour.Geometry.tangentBundle_secondCountable line 22570
instance OAI.PositiveEinsteinFour.Geometry.frameBundle_secondCountable line 22587
instance OAI.PositiveEinsteinFour.Geometry.unitTangentBundle_secondCountable line 22593
instance OAI.PositiveEinsteinFour.Geometry.frameBundle_pseudoMetrizable line 22599
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentBundle_pseudoMetrizable line 22604

theorem OAI.PositiveEinsteinFour.Jacobi.full_jacobi_eq_mulVec line 22627

Source documentation

The radial and normal initial-value equations determine the full frame variation.

theorem full_jacobi_eq_mulVec {R : ℝ → NormalMatrix}
    (d : MatrixJacobiSolution R) (K : ℝ≥0) (hK : ∀ s, ‖R s‖ ≤ K)
    (y z : ℝ → Fin 4 → ℝ) (w : Fin 4 → ℝ) (a b : ℝ)
    (hzero : (0 : ℝ) ∈ Ioo a b) (hy0 : y 0 = 0) (hz0 : z 0 = w)
    (hy : ∀ s ∈ Ioo a b, HasDerivAt y (z s) s)
    (hz : ∀ s ∈ Ioo a b,
      HasDerivAt z (-(Fin.cons 0 (R s *ᵥ fun i => y s i.succ))) s) :
    ∀ s ∈ Ioo a b,
      y s = jacobiBlockMatrix s (d.J s) *ᵥ w ∧
      z s = jacobiBlockMatrix 1 (d.V s) *ᵥ w := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution

theorem OAI.PositiveEinsteinFour.Geometry.continuous_unitTangentBase line 22701
theorem OAI.PositiveEinsteinFour.Geometry.exists_measurable_gram_extension line 22713
Source documentation
Extend the Gram frame measurably outside its chart while retaining its exact base point everywhere. The extension only computes measures.
```
theorem exists_measurable_gram_extension (g : SmoothMetric M) (o : FrameOrientation g)
    (c : M) : ∃ s : M → FrameBundle g, Measurable s ∧
      (∀ x, (s x).base = x) ∧
      EqOn s (localGramSection g c 1 (by simp)) (chartAt FourSpace c).source := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.localGramSection
theorem OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure_restrict_chart line 22739
Source documentation
The restriction to a base chart has normalized base volume times spherical probability, expressed using the actual smooth Gram frame.
```
theorem canonicalUnitTangentMeasure_restrict_chart (g : SmoothMetric M)
    (o : FrameOrientation g) (c : M) :
    (canonicalUnitTangentMeasure g o).restrict
      {u | u.base ∈ (chartAt FourSpace c).source} =
      Measure.map (fun p : M × Directions =>
        unitTangentTurn (localGramSection g c 1 (by simp) p.1) p.2)
        (((normalizedVolume g).restrict (chartAt FourSpace c).source).prod sphereMeasure) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure, OAI.PositiveEinsteinFour.Geometry.unitTangentTurn, OAI.PositiveEinsteinFour.Geometry.localGramSection, OAI.PositiveEinsteinFour.Geometry.normalizedVolume
abbrev OAI.PositiveEinsteinFour.Geometry.ChartUnitTangent line 22794
abbrev OAI.PositiveEinsteinFour.Geometry.NonzeroCotangentChart line 22797
def OAI.PositiveEinsteinFour.Geometry.tangentInnerForm line 22800
def OAI.PositiveEinsteinFour.Geometry.unitTangentVector line 22803
theorem OAI.PositiveEinsteinFour.Geometry.tangentInnerForm_pos line 22805
theorem OAI.PositiveEinsteinFour.Geometry.tangentInnerForm_unit line 22808
def OAI.PositiveEinsteinFour.Geometry.chartForwardOperator line 22811
def OAI.PositiveEinsteinFour.Geometry.chartBackwardOperator line 22814
theorem OAI.PositiveEinsteinFour.Geometry.chartBackward_forward line 22817
theorem OAI.PositiveEinsteinFour.Geometry.chartForward_backward line 22822
def OAI.PositiveEinsteinFour.Geometry.unitChartVelocity line 22828
theorem OAI.PositiveEinsteinFour.Geometry.unitChartVelocity_eq_derivative line 22833
theorem OAI.PositiveEinsteinFour.Geometry.unitChartVelocity_continuousAt line 22845
theorem OAI.PositiveEinsteinFour.Geometry.unitChartVelocity_inner line 22856
def OAI.PositiveEinsteinFour.Geometry.unitCotangentState line 22875
theorem OAI.PositiveEinsteinFour.Geometry.unitCotangentState_frame line 22880
theorem OAI.PositiveEinsteinFour.Geometry.unitCotangentState_continuousAt line 22885
def OAI.PositiveEinsteinFour.Geometry.raisedChartVelocity line 22924
def OAI.PositiveEinsteinFour.Geometry.raisedChartVector line 22928
def OAI.PositiveEinsteinFour.Geometry.momentumRadius line 22932
theorem OAI.PositiveEinsteinFour.Geometry.raisedChartVelocity_lower line 22936
theorem OAI.PositiveEinsteinFour.Geometry.momentumRadius_pos line 22943
theorem OAI.PositiveEinsteinFour.Geometry.momentumRadius_sq line 22959
def OAI.PositiveEinsteinFour.Geometry.unitTangentFromMomentum line 22976
theorem OAI.PositiveEinsteinFour.Geometry.unitChartVelocity_fromMomentum line 22989
theorem OAI.PositiveEinsteinFour.Geometry.unitCotangentState_fromMomentum line 23002
Source documentation
The normalized inverse recovers every nonzero cotangent momentum.
```
theorem unitCotangentState_fromMomentum (g : SmoothMetric M) (c : M)
    (p : NonzeroCotangentChart c) :
    unitCotangentState g c (momentumRadius g c p) (unitTangentFromMomentum g c p).val = p.val := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.NonzeroCotangentChart, OAI.PositiveEinsteinFour.Geometry.unitCotangentState, OAI.PositiveEinsteinFour.Geometry.momentumRadius, OAI.PositiveEinsteinFour.Geometry.unitTangentFromMomentum
theorem OAI.PositiveEinsteinFour.Geometry.raisedChartVelocity_unitCotangentState line 23016
theorem OAI.PositiveEinsteinFour.Geometry.raisedChartVector_unitCotangentState line 23029
theorem OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian_unitCotangentState line 23042
theorem OAI.PositiveEinsteinFour.Geometry.momentumRadius_unitCotangentState line 23056
theorem OAI.PositiveEinsteinFour.Geometry.unitCotangentState_momentum_ne_zero line 23068
def OAI.PositiveEinsteinFour.Geometry.unitTangentCotangentTo line 23082
def OAI.PositiveEinsteinFour.Geometry.unitTangentCotangentFrom line 23088
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentCotangentTo_from line 23092
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentCotangentFrom_to line 23098
def OAI.PositiveEinsteinFour.Geometry.unitTangentCotangentEquiv line 23116
Source documentation
Actual radial unit tangent coordinates and nonzero cotangent coordinates in a fixed manifold chart are mutually inverse.
```
def unitTangentCotangentEquiv (g : SmoothMetric M) (c : M) :
    (PositiveRadius × ChartUnitTangent g c) ≃ NonzeroCotangentChart c where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.ChartUnitTangent, OAI.PositiveEinsteinFour.Geometry.NonzeroCotangentChart
def OAI.PositiveEinsteinFour.Geometry.frameGeodesic line 23147
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_continuous line 23150
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_chart_derivative line 23154
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_chart_contDiffOn line 23164
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_contMDiff line 23191
theorem OAI.PositiveEinsteinFour.Geometry.frameChart_column_eq_derivative line 23210
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_mfderiv line 23219
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_metric_speed line 23249
theorem OAI.PositiveEinsteinFour.Geometry.normalFrameAverage_eq_of_unitTangent line 23288
def OAI.PositiveEinsteinFour.Geometry.unitTangentAverage line 23303
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentAverage_of_frame line 23306
theorem OAI.PositiveEinsteinFour.Geometry.continuous_unitTangentAverage line 23314
theorem OAI.PositiveEinsteinFour.Geometry.integral_unitTangentAverage line 23325
theorem OAI.PositiveEinsteinFour.Geometry.integral_frameFlow_eq_unitTangentFlow line 23340
theorem OAI.PositiveEinsteinFour.Geometry.frameFlow_preserves_of_unitTangent line 23359
theorem OAI.PositiveEinsteinFour.Geometry.allFrameFlows_preserve_of_unitTangent line 23373
theorem OAI.PositiveEinsteinFour.Geometry.continuous_raisedChartVelocity line 23401
theorem OAI.PositiveEinsteinFour.Geometry.momentumRadius_eq_sqrt line 23421
theorem OAI.PositiveEinsteinFour.Geometry.continuous_momentumRadius line 23427
theorem OAI.PositiveEinsteinFour.Geometry.continuous_unitTangentFromMomentum line 23447
theorem OAI.PositiveEinsteinFour.Geometry.continuous_unitTangentCotangentTo line 23484
theorem OAI.PositiveEinsteinFour.Geometry.continuous_unitTangentCotangentFrom line 23494
def OAI.PositiveEinsteinFour.Geometry.unitTangentCotangentHomeomorph line 23499