GeodesicGeometry04.lean`

876 declarations, 0 contain sorry, 0 declared as axioms

Exact unit-speed length and endpoint distance bounds for the actual complete geodesics, including their intrinsic unit-tangent formulation.

theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_pathELength line 68
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_distance_le line 79
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_distance_from_start line 99
def OAI.PositiveEinsteinFour.Geometry.unitGeodesic line 105
theorem OAI.PositiveEinsteinFour.Geometry.unitGeodesic_eq_frameGeodesic line 108
theorem OAI.PositiveEinsteinFour.Geometry.unitGeodesic_contMDiff line 112
theorem OAI.PositiveEinsteinFour.Geometry.unitGeodesic_distance_le line 116
theorem OAI.PositiveEinsteinFour.Geometry.unitGeodesic_distance_from_start line 122
def OAI.PositiveEinsteinFour.Geometry.affinePartitionTime line 147
theorem OAI.PositiveEinsteinFour.Geometry.affinePartitionTime_zero line 149
theorem OAI.PositiveEinsteinFour.Geometry.affinePartitionTime_last line 152
theorem OAI.PositiveEinsteinFour.Geometry.exists_finite_curve_chart_partition line 159
theorem OAI.PositiveEinsteinFour.Geometry.frameChart_map line 224
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticEndpointCurve_zero line 244
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticEndpointCurve_continuousAt line 249
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticEndpointCurve_eq line 257
def OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow line 303
Source documentation
Radius is constant and multiplies the time of the unit-speed flow.
```
def unitTangentRadialFlow (g : SmoothMetric M) (o : FrameOrientation g) (t : ℝ)
    (p : PositiveRadius × UnitTangentBundle g) : PositiveRadius × UnitTangentBundle g :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow_continuous line 307
def OAI.PositiveEinsteinFour.Geometry.unitTangentRadialHomeomorph line 312
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentFlow_preserves_of_radial line 333
theorem OAI.PositiveEinsteinFour.Geometry.allFrameFlows_preserve_of_radial line 347
def OAI.PositiveEinsteinFour.Geometry.frameExponentialNonzero line 377
def OAI.PositiveEinsteinFour.Geometry.frameExponential line 382
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_nonzero line 387
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_zero line 392
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_radial line 398
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_distance line 406
theorem OAI.PositiveEinsteinFour.Geometry.frameExponentialNonzero_continuous line 424
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_continuous line 437
def OAI.PositiveEinsteinFour.Geometry.joinedPartitionTime line 479
theorem OAI.PositiveEinsteinFour.Geometry.affinePartitionTime_step_lt line 482
theorem OAI.PositiveEinsteinFour.Geometry.joinedPartitionTime_left line 492
theorem OAI.PositiveEinsteinFour.Geometry.joinedPartitionTime_right line 496
theorem OAI.PositiveEinsteinFour.Geometry.joinedPartitionTime_zero line 505
theorem OAI.PositiveEinsteinFour.Geometry.joinedPartitionTime_last line 509
theorem OAI.PositiveEinsteinFour.Geometry.joinedPartitionTime_step_lt line 513
theorem OAI.PositiveEinsteinFour.Geometry.joinedPartition_chart_cover line 527
theorem OAI.PositiveEinsteinFour.Geometry.sum_intervalIntegral_partition line 549
theorem OAI.PositiveEinsteinFour.Geometry.joinedPartition_sum_integral line 557
theorem OAI.PositiveEinsteinFour.Geometry.measure_eq_of_local_restrict line 612

theorem OAI.PositiveEinsteinFour.Geometry.measure_le_of_local_restrict line 622

Source documentation

Pointwise local domination suffices for domination of the measures. This applies the same countable-cover argument to their lattice infimum.

theorem measure_le_of_local_restrict {X : Type*} [TopologicalSpace X]
    [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] (μ ν : Measure X)
    (hlocal : ∀ x, ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ μ.restrict U ≤ ν.restrict U) :
    μ ≤ ν := by
…

theorem OAI.PositiveEinsteinFour.Geometry.measure_le_of_sharp_local_comparison line 639

Source documentation

Arbitrarily sharp local lower comparisons give exact global domination, with no differentiation theorem for measures required.

theorem measure_le_of_sharp_local_comparison {X : Type*} [TopologicalSpace X]
    [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] (μ ν : Measure X)
    (hlocal : ∀ a : ℝ≥0∞, a < 1 → ∀ x, ∃ U : Set X, IsOpen U ∧ x ∈ U ∧
      (a • μ).restrict U ≤ ν.restrict U) : μ ≤ ν := by
…

theorem OAI.PositiveEinsteinFour.Geometry.measurePreserving_of_local_image line 652

Source documentation

Local image-measure identities for a homeomorphism determine its pushforward on the whole second-countable space.

theorem measurePreserving_of_local_image {X : Type*} [TopologicalSpace X]
    [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X]
    (f : X ≃ₜ X) (μ : Measure X)
    (hlocal : ∀ x, ∃ U : Set X, IsOpen U ∧ x ∈ U ∧
      Measure.map f (μ.restrict U) = μ.restrict (f '' U)) :
    MeasurePreserving f μ μ := by
…

theorem OAI.PositiveEinsteinFour.Geometry.unitTangentFlow_preserves_of_near_zero line 675
Source documentation
It suffices to preserve the actual unit tangent probability for a fixed nonempty time interval around zero. Completeness and the group law then give preservation for every real time.
```
theorem unitTangentFlow_preserves_of_near_zero (g : SmoothMetric M) (o : FrameOrientation g)
    (ε : ℝ) (hε : 0 < ε)
    (hnear : ∀ t ∈ Ioo (-ε) ε, MeasurePreserving (unitTangentFlowMap g o t)
      (canonicalUnitTangentMeasure g o) (canonicalUnitTangentMeasure g o)) (t : ℝ) :
    MeasurePreserving (unitTangentFlowMap g o t)
      (canonicalUnitTangentMeasure g o) (canonicalUnitTangentMeasure g o) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.unitTangentFlowMap, OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure
def OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState line 729
theorem OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState_continuousAt line 734
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_unitTangentRadial_cotangent line 744
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow_joint_continuous line 770
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow_chart_neighborhood line 780

theorem OAI.PositiveEinsteinFour.Geometry.exists_unitTangent_localHamiltonian line 811

Source documentation

A common open intrinsic neighborhood is conjugate to the actual local Hamiltonian flow. This is the local input for transporting its volume law.

theorem exists_unitTangent_localHamiltonian (g : SmoothMetric M) (o : FrameOrientation g)
    (c : M) (p : PositiveRadius × UnitTangentBundle g)
    (hp : p.2.base ∈ (chartAt FourSpace c).source) :
    ∃ U : Set (PositiveRadius × UnitTangentBundle g), IsOpen U ∧ p ∈ U ∧
      ∃ F : KineticLocalFlow g c (unitRadialCotangentState g c p),
        (∀ q ∈ U, unitRadialCotangentState g c q ∈
          Metric.ball (unitRadialCotangentState g c p) F.radius) ∧
        (∀ q ∈ U, EqOn (fun t => F.map (unitRadialCotangentState g c q, t))
          (fun t => unitRadialCotangentState g c (unitTangentRadialFlow g o t q))
          (Ioo (-F.time) F.time)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow, OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState, OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow

def OAI.PositiveEinsteinFour.Geometry.frameMomentumMap line 867
Source documentation
Lowering the initial frame vector in a fixed coordinate chart.
```
def frameMomentumMap (g : SmoothMetric M) (c : M) (e : FrameBundle g) :
    FourSpace →L[ℝ] FourSpace :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle
theorem OAI.PositiveEinsteinFour.Geometry.unitCotangentState_turn line 873
theorem OAI.PositiveEinsteinFour.Geometry.unitGeodesic_turn_zero line 888
theorem OAI.PositiveEinsteinFour.Geometry.unitGeodesic_turn_joint_continuous line 894
theorem OAI.PositiveEinsteinFour.Geometry.direction_uniform_neighborhood line 901
theorem OAI.PositiveEinsteinFour.Geometry.unitGeodesic_uniform_chart line 919
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.radial_endpoint_uniform line 933
Source documentation
Every sufficiently short radial geodesic starting at a fixed frame satisfies the same constructed local Hamiltonian flow, uniformly in direction.
```
theorem KineticLocalFlow.radial_endpoint_uniform (g : SmoothMetric M)
    (o : FrameOrientation g) (c : M) (e : FrameBundle g)
    (he : e.base ∈ (chartAt FourSpace c).source)
    (F : KineticLocalFlow g c (chartAt FourSpace c e.base, 0)) :
    ∃ ε > (0 : ℝ), ∀ q : Directions, ∀ r : ℝ, 0 < r → r < ε →
      ∀ t ∈ Ioo (-F.time) F.time,
        F.map ((chartAt FourSpace c e.base, frameMomentumMap g c e (r • q.val)), t) =
          unitCotangentState g c r (unitTangentFlowMap g o (r * t) (unitTangentTurn e q)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow, OAI.PositiveEinsteinFour.Geometry.frameMomentumMap, OAI.PositiveEinsteinFour.Geometry.unitCotangentState, OAI.PositiveEinsteinFour.Geometry.unitTangentFlowMap, OAI.PositiveEinsteinFour.Geometry.unitTangentTurn
theorem OAI.PositiveEinsteinFour.Geometry.measure_restrict_eq_of_local line 995
theorem OAI.PositiveEinsteinFour.Geometry.measure_restrict_le_of_local line 1010
theorem OAI.PositiveEinsteinFour.Geometry.measure_restrict_le_of_sharp_local_comparison line 1031

theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.map_volume_restrict line 1069

Source documentation

The proved unit Jacobian applies to any measurable part of the initial ball. This is the form used after shrinking an intrinsic neighborhood.

theorem map_volume_restrict {g : SmoothMetric M} {c : M} {p : CotangentCoordinates}
    (F : KineticLocalFlow g c p) (t : ℝ) (ht : t ∈ Ioo (-F.time) F.time)
    (s : Set CotangentCoordinates) (hs : MeasurableSet s)
    (hsub : s ⊆ Metric.ball p F.radius) :
    Measure.map (fun q => F.map (q, t)) (volume.restrict s) =
      volume.restrict ((fun q => F.map (q, t)) '' s) := by
…

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

theorem OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState_injOn line 1082
theorem OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState_continuousOn line 1092
theorem OAI.PositiveEinsteinFour.Geometry.isOpen_unitRadialCotangentState_image line 1097
theorem OAI.PositiveEinsteinFour.Geometry.radial_chart_neighborhood line 1125

theorem OAI.PositiveEinsteinFour.Geometry.exists_unitTangent_cotangentNeighborhood line 1157

Source documentation

An intrinsic neighborhood has an open cotangent image lying in the initial Hamiltonian ball. Every trajectory stays in the chosen base chart, and its cotangent image agrees with the constructed Hamiltonian flow.

theorem exists_unitTangent_cotangentNeighborhood (g : SmoothMetric M)
    (o : FrameOrientation g) (c : M) (p : PositiveRadius × UnitTangentBundle g)
    (hp : p.2.base ∈ (chartAt FourSpace c).source) :
    ∃ U : Set (PositiveRadius × UnitTangentBundle g),
      ∃ V : Set CotangentCoordinates,
      ∃ F : KineticLocalFlow g c (unitRadialCotangentState g c p),
        IsOpen U ∧ p ∈ U ∧ IsOpen V ∧ unitRadialCotangentState g c p ∈ V ∧
        V = unitRadialCotangentState g c '' U ∧
        V ⊆ Metric.ball (unitRadialCotangentState g c p) F.radius ∧
        (∀ z ∈ V, z.1 ∈ (chartAt FourSpace c).target ∧ z.2 ≠ 0) ∧
        (∀ q ∈ U, ∀ t ∈ Ioo (-F.time) F.time,
          (unitTangentRadialFlow g o t q).2.base ∈ (chartAt FourSpace c).source) ∧
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow, OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState, OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow

theorem OAI.PositiveEinsteinFour.Geometry.kinetic_radial_image line 1204
Source documentation
Transporting the intrinsic neighborhood and transporting its cotangent image give the same set.
```
theorem kinetic_radial_image (g : SmoothMetric M) (o : FrameOrientation g) (c : M)
    {p : CotangentCoordinates} (F : KineticLocalFlow g c p) (t : ℝ)
    (U : Set (PositiveRadius × UnitTangentBundle g))
    (heq : ∀ q ∈ U, F.map (unitRadialCotangentState g c q, t) =
      unitRadialCotangentState g c (unitTangentRadialFlow g o t q)) :
    (fun z => F.map (z, t)) '' (unitRadialCotangentState g c '' U) =
      unitRadialCotangentState g c '' (unitTangentRadialFlow g o t '' U) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow, OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState, OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow
theorem OAI.PositiveEinsteinFour.Geometry.isOpen_kinetic_radial_image line 1214
theorem OAI.PositiveEinsteinFour.Geometry.kinetic_radial_image_subset_nonzero_chart line 1228
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_chart_eventually_kinetic line 1264
theorem OAI.PositiveEinsteinFour.Geometry.raise_frameMomentumMap line 1300
Source documentation
Raising the lowered initial vector cancels the metric.
```
theorem raise_frameMomentumMap (g : SmoothMetric M) (c : M) (e : FrameBundle g)
    (he : e.base ∈ (chartAt FourSpace c).source) :
    (Matrix.toEuclideanCLM (n := Fin 4) (𝕜 := ℝ)
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_chart_strictDerivative_rescaled line 1317
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_chart_strictDerivative_zero line 1341
Source documentation
The actual radial exponential has at zero exactly the initial frame map in any fixed chart.
```
theorem frameExponential_chart_strictDerivative_zero (g : SmoothMetric M)
    (o : FrameOrientation g) (c : M) (e : FrameBundle g)
    (he : e.base ∈ (chartAt FourSpace c).source) :
    HasStrictFDerivAt (fun v : FourSpace => chartAt FourSpace c (frameExponential g o e v))
      ((chartForwardOperator c e.base).comp e.frame.map.toContinuousLinearMap) 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameExponential, OAI.PositiveEinsteinFour.Geometry.chartForwardOperator
theorem OAI.PositiveEinsteinFour.Geometry.ofReal_sqrt_four line 1393
theorem OAI.PositiveEinsteinFour.Geometry.ofReal_inv_sqrt_four line 1402
theorem OAI.PositiveEinsteinFour.Geometry.exists_chartHausdorff_constant_bounds line 1413
def OAI.PositiveEinsteinFour.Geometry.chartBaseDensity line 1467
instance OAI.PositiveEinsteinFour.Geometry.chartBaseDensity_sfinite line 1471
def OAI.PositiveEinsteinFour.Geometry.gramChartUnitTangent line 1476
theorem OAI.PositiveEinsteinFour.Geometry.continuous_gramChartUnitTangent line 1480
theorem OAI.PositiveEinsteinFour.Geometry.localGramSection_chart_inverse line 1485
theorem OAI.PositiveEinsteinFour.Geometry.chartGramFrame_map line 1494
theorem OAI.PositiveEinsteinFour.Geometry.gramChartUnitTangent_velocity line 1527
def OAI.PositiveEinsteinFour.Geometry.gramRadialLift line 1545
theorem OAI.PositiveEinsteinFour.Geometry.continuous_gramRadialLift line 1550
theorem OAI.PositiveEinsteinFour.Geometry.gramRadialLift_cotangent line 1556
theorem OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure_chartDensity line 1580
theorem OAI.PositiveEinsteinFour.Geometry.gramRadialLift_map line 1628
def OAI.PositiveEinsteinFour.Geometry.measurableRadialState line 1645
theorem OAI.PositiveEinsteinFour.Geometry.measurable_measurableRadialState line 1652
theorem OAI.PositiveEinsteinFour.Geometry.cotangentCoordinateInclusion_map line 1661
theorem OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState_map line 1681
Source documentation
The normalization factor is the base density factor divided by the actual Euclidean angular mass. No flow preservation is assumed.
```
theorem unitRadialCotangentState_map (g : SmoothMetric M) (o : FrameOrientation g)
    (c : M) (K : ℝ≥0∞)
    (hbase : (normalizedVolume g).restrict (chartAt FourSpace c).source =
      K • Measure.map (fun z : ChartTarget c => (chartAt FourSpace c).symm z.val)
        (chartBaseDensity g c)) :
    Measure.map (unitRadialCotangentState g c)
      (((Measure.volumeIoiPow 3).prod (canonicalUnitTangentMeasure g o)).restrict
        {p | p.2.base ∈ (chartAt FourSpace c).source}) =
      (K / polarAngularMass) • (volume : Measure CotangentCoordinates).restrict
        {p | p.1 ∈ (chartAt FourSpace c).target} := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.normalizedVolume, OAI.PositiveEinsteinFour.Geometry.ChartTarget, OAI.PositiveEinsteinFour.Geometry.chartBaseDensity, OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState, OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure, OAI.PositiveEinsteinFour.Geometry.polarAngularMass, OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates
def OAI.PositiveEinsteinFour.Geometry.radialSlab line 1762
theorem OAI.PositiveEinsteinFour.Geometry.isCompact_radialSlab line 1766
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow_mem_slab line 1784
def OAI.PositiveEinsteinFour.Geometry.unitTangentRadialSlabHomeomorph line 1789
Source documentation
The restriction is the actual radial flow, with inverse negative time.
```
def unitTangentRadialSlabHomeomorph (g : SmoothMetric M) (o : FrameOrientation g)
    (a b t : ℝ) : radialSlab g a b ≃ₜ radialSlab g a b where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.radialSlab
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadialSlabHomeomorph_zero line 1800
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadialSlabHomeomorph_add line 1809
structure OAI.PositiveEinsteinFour.Geometry.RadialHamiltonianChart line 1824
Source documentation
Data produced by the local Hamiltonian theorem, retaining the actual coordinate map and the common interval of agreement with radial motion.
```
structure RadialHamiltonianChart (g : SmoothMetric M) (o : FrameOrientation g) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation
theorem OAI.PositiveEinsteinFour.Geometry.exists_radialHamiltonianChart line 1843
theorem OAI.PositiveEinsteinFour.Geometry.finite_positive_lower_bound line 1864
Distinct definitions of this name: OAI/Geometry/EinsteinFour/HeatKernels10.lean:4683 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.finite_positive_lower_bound@path.
theorem OAI.PositiveEinsteinFour.Geometry.radialSlab_uniform_hamiltonian_time line 1883
Source documentation
A single positive time works in actual Hamiltonian charts around all points of a compact radius slab. The centers and charts may vary pointwise.
```
theorem radialSlab_uniform_hamiltonian_time (g : SmoothMetric M) (o : FrameOrientation g)
    {a b : ℝ} (ha : 0 < a) :
    ∃ ε > (0 : ℝ), ∀ p ∈ radialSlab g a b,
      ∃ C : RadialHamiltonianChart g o, p ∈ C.domain ∧ ε ≤ C.flow.time := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.radialSlab, OAI.PositiveEinsteinFour.Geometry.RadialHamiltonianChart
theorem OAI.PositiveEinsteinFour.Geometry.density_comparison_parameter line 1915
theorem OAI.PositiveEinsteinFour.Geometry.chartHausdorffMeasure_eq_density line 1931
theorem OAI.PositiveEinsteinFour.Geometry.chartForwardOperator_center line 2035
theorem OAI.PositiveEinsteinFour.Geometry.frameMap_isUnit line 2046
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_localChart line 2063
Source documentation
The actual exponential agrees on a neighborhood of zero with a local homeomorphism onto a neighborhood of its base point.
```
theorem frameExponential_localChart (g : SmoothMetric M) (o : FrameOrientation g)
    (e : FrameBundle g) :
    ∃ C : OpenPartialHomeomorph FourSpace M,
      0 ∈ C.source ∧ EqOn C (frameExponential g o e) C.source := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameExponential
def OAI.PositiveEinsteinFour.Geometry.radialCotangentStateExtension line 2120
theorem OAI.PositiveEinsteinFour.Geometry.radialCotangentStateExtension_eq line 2126
def OAI.PositiveEinsteinFour.Geometry.cotangentRadialInverseOn line 2133
theorem OAI.PositiveEinsteinFour.Geometry.continuous_cotangentRadialInverseOn line 2138
def OAI.PositiveEinsteinFour.Geometry.cotangentRadialRetraction line 2144
theorem OAI.PositiveEinsteinFour.Geometry.cotangentRadialRetraction_on line 2150
theorem OAI.PositiveEinsteinFour.Geometry.cotangentRadialRetraction_source line 2155
theorem OAI.PositiveEinsteinFour.Geometry.cotangentRadialRetraction_state line 2164
Source documentation
The measurable inverse recovers the original intrinsic radial state.
```
theorem cotangentRadialRetraction_state (g : SmoothMetric M) (c : M)
    (p : PositiveRadius × UnitTangentBundle g)
    (hp : p.2.base ∈ (chartAt FourSpace c).source) :
    cotangentRadialRetraction g c (unitRadialCotangentState g c p) = p := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.cotangentRadialRetraction, OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState
theorem OAI.PositiveEinsteinFour.Geometry.cotangentRadialRetraction_extension line 2178
theorem OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState_retraction line 2186
Source documentation
On the nonzero cotangent chart, the extension's inverse is also a right inverse.
```
theorem unitRadialCotangentState_retraction (g : SmoothMetric M) (c : M)
    (z : CotangentCoordinates)
    (hz : z.1 ∈ (chartAt FourSpace c).target ∧ z.2 ≠ 0) :
    unitRadialCotangentState g c (cotangentRadialRetraction g c z) = z := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CotangentCoordinates, OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState, OAI.PositiveEinsteinFour.Geometry.cotangentRadialRetraction
theorem OAI.PositiveEinsteinFour.Geometry.radialCotangentStateExtension_retraction line 2195
theorem OAI.PositiveEinsteinFour.Geometry.measurable_radialCotangentStateExtension line 2204
theorem OAI.PositiveEinsteinFour.Geometry.measurable_cotangentRadialRetraction line 2211
theorem OAI.PositiveEinsteinFour.Geometry.isClosed_radialSlab line 2242
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow_preimage_slab line 2246
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow_image_slab line 2250
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow_zero line 2257
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow_add line 2264

theorem OAI.PositiveEinsteinFour.Geometry.radialSlab_restrict_local_image line 2276

Source documentation

A local ambient image identity restricts to the invariant slab.

theorem radialSlab_restrict_local_image (g : SmoothMetric M) (o : FrameOrientation g)
    (μ : Measure (PositiveRadius × UnitTangentBundle g)) (a b t : ℝ)
    (U : Set (PositiveRadius × UnitTangentBundle g))
    (hlocal : Measure.map (unitTangentRadialFlow g o t) (μ.restrict U) =
      μ.restrict (unitTangentRadialFlow g o t '' U)) :
    Measure.map (unitTangentRadialFlow g o t) ((μ.restrict (radialSlab g a b)).restrict U) =
      (μ.restrict (radialSlab g a b)).restrict (unitTangentRadialFlow g o t '' U) := by
…

theorem OAI.PositiveEinsteinFour.Geometry.radialSlab_preserves_of_local_image line 2298

Source documentation

It suffices to supply ambient local image identities at points of the slab. Outside it, both restricted measures vanish.

theorem radialSlab_preserves_of_local_image (g : SmoothMetric M) (o : FrameOrientation g)
    (μ : Measure (PositiveRadius × UnitTangentBundle g)) (a b t : ℝ)
    (hlocal : ∀ p ∈ radialSlab g a b,
      ∃ U : Set (PositiveRadius × UnitTangentBundle g), IsOpen U ∧ p ∈ U ∧
        Measure.map (unitTangentRadialFlow g o t) (μ.restrict U) =
          μ.restrict (unitTangentRadialFlow g o t '' U)) :
    MeasurePreserving (unitTangentRadialFlow g o t)
      (μ.restrict (radialSlab g a b)) (μ.restrict (radialSlab g a b)) := by
…

theorem OAI.PositiveEinsteinFour.Geometry.radialSlab_preserves_of_near_zero line 2328
Source documentation
The group law turns a neighborhood of preserving times into all times, for the measure restricted to one invariant slab.
```
theorem radialSlab_preserves_of_near_zero (g : SmoothMetric M) (o : FrameOrientation g)
    (μ : Measure (PositiveRadius × UnitTangentBundle g)) (a b ε : ℝ) (hε : 0 < ε)
    (hnear : ∀ t ∈ Ioo (-ε) ε, MeasurePreserving (unitTangentRadialFlow g o t)
      (μ.restrict (radialSlab g a b)) (μ.restrict (radialSlab g a b))) (t : ℝ) :
    MeasurePreserving (unitTangentRadialFlow g o t)
      (μ.restrict (radialSlab g a b)) (μ.restrict (radialSlab g a b)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow, OAI.PositiveEinsteinFour.Geometry.radialSlab
def OAI.PositiveEinsteinFour.Geometry.exhaustingRadialSlab line 2362
theorem OAI.PositiveEinsteinFour.Geometry.iUnion_exhaustingRadialSlab line 2367
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadial_preserves_of_slabs line 2388
Source documentation
Preservation on the countable family of slabs determines preservation of the whole radial measure, without a finiteness hypothesis.
```
theorem unitTangentRadial_preserves_of_slabs (g : SmoothMetric M) (o : FrameOrientation g)
    (μ : Measure (PositiveRadius × UnitTangentBundle g)) (t : ℝ)
    (hslabs : ∀ n, MeasurePreserving (unitTangentRadialFlow g o t)
      (μ.restrict (exhaustingRadialSlab g n)) (μ.restrict (exhaustingRadialSlab g n))) :
    MeasurePreserving (unitTangentRadialFlow g o t) μ μ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow, OAI.PositiveEinsteinFour.Geometry.exhaustingRadialSlab

theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadial_preserves_of_slab_local_images line 2405

Source documentation

Final technical reduction: uniform small-time local image identities on each compact slab suffice for ambient radial preservation at every time.

theorem unitTangentRadial_preserves_of_slab_local_images
    (g : SmoothMetric M) (o : FrameOrientation g)
    (μ : Measure (PositiveRadius × UnitTangentBundle g))
    (hlocal : ∀ n, ∃ ε > (0 : ℝ), ∀ t ∈ Ioo (-ε) ε,
      ∀ p ∈ exhaustingRadialSlab g n,
        ∃ U : Set (PositiveRadius × UnitTangentBundle g), IsOpen U ∧ p ∈ U ∧
          Measure.map (unitTangentRadialFlow g o t) (μ.restrict U) =
            μ.restrict (unitTangentRadialFlow g o t '' U)) (t : ℝ) :
    MeasurePreserving (unitTangentRadialFlow g o t) μ μ := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.exhaustingRadialSlab, OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow

theorem OAI.PositiveEinsteinFour.Geometry.continuous_chartInverse_restrict line 2442
theorem OAI.PositiveEinsteinFour.Geometry.metricHausdorffMeasure_restrict_chart line 2449
def OAI.PositiveEinsteinFour.Geometry.riemannianChartFactor line 2490
theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_restrict_chart line 2493
def OAI.PositiveEinsteinFour.Geometry.normalizedChartFactor line 2503
theorem OAI.PositiveEinsteinFour.Geometry.normalizedVolume_restrict_chart line 2506
def OAI.PositiveEinsteinFour.Geometry.cotangentChartTransition line 2535
theorem OAI.PositiveEinsteinFour.Geometry.cotangentChartTransition_contDiffAt line 2542
theorem OAI.PositiveEinsteinFour.Geometry.unitChartVelocity_change line 2580
theorem OAI.PositiveEinsteinFour.Geometry.cotangentChartTransition_unitState line 2599
theorem OAI.PositiveEinsteinFour.Geometry.cotangentChartTransition_radialState line 2620
theorem OAI.PositiveEinsteinFour.Geometry.cotangentChartTransition_retraction line 2628
theorem OAI.PositiveEinsteinFour.Geometry.actual_unitRadialCotangentState_map line 2659
theorem OAI.PositiveEinsteinFour.Geometry.chart_image_measurable line 2691
theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_chart_image line 2708
theorem OAI.PositiveEinsteinFour.Geometry.fourSpace_volume_ball line 2750
theorem OAI.PositiveEinsteinFour.Geometry.fourSpace_volume_closedBall line 2755
theorem OAI.PositiveEinsteinFour.Geometry.ball_normalization_product line 2761
theorem OAI.PositiveEinsteinFour.Geometry.fourSpace_ediam_closedBall_le line 2769
theorem OAI.PositiveEinsteinFour.Geometry.fourSpace_ball_cost line 2774
theorem OAI.PositiveEinsteinFour.Geometry.euclideanHausdorff_unitBall_le line 2786
theorem OAI.PositiveEinsteinFour.Geometry.euclideanHausdorffFactor_le line 2840
theorem OAI.PositiveEinsteinFour.Geometry.riemannianChartFactor_le_one line 2848
theorem OAI.PositiveEinsteinFour.Geometry.polarAngularMass_eq line 2859
theorem OAI.PositiveEinsteinFour.Geometry.cotangentRadialRetraction_continuousAt line 2886
def OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow line 2903
theorem OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow_at_state line 2907
theorem OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow_continuousAt line 2914
theorem OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow_add_eventually line 2935
Source documentation
The intrinsic group law becomes coordinate composition on a genuine neighborhood of the starting cotangent state.
```
theorem radialCoordinateFlow_add_eventually (g : SmoothMetric M) (o : FrameOrientation g)
    (c m d : M) (s t : ℝ) (p : PositiveRadius × UnitTangentBundle g)
    (hc : p.2.base ∈ (chartAt FourSpace c).source)
    (hm : (unitTangentRadialFlow g o t p).2.base ∈ (chartAt FourSpace m).source) :
    radialCoordinateFlow g o c d (s + t) =ᶠ[𝓝 (unitRadialCotangentState g c p)]
      (radialCoordinateFlow g o m d s ∘ radialCoordinateFlow g o c m t) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow, OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow, OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState

theorem OAI.PositiveEinsteinFour.Geometry.scalar_chart_representative_ae line 2985

Source documentation

Lebesgue almost-everywhere equality in a chart transfers to actual normalized volume. No measurability assumption on the representatives is needed, and the open set need not be contained in the chart target.

theorem scalar_chart_representative_ae (g : SmoothMetric M) (c : M)
    (U : Set FourSpace) (hU : IsOpen U) (b : M → ℝ) (F : FourSpace → ℝ)
    (h : (fun z => b ((chartAt FourSpace c).symm z)) =ᵐ[volume.restrict U] F) :
    b =ᵐ[(normalizedVolume g).restrict
      ((chartAt FourSpace c).source ∩ (chartAt FourSpace c) ⁻¹' U)]
      (fun x => F (chartAt FourSpace c x)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.normalizedVolume

def OAI.PositiveEinsteinFour.Geometry.RadialFlowContDiffAt line 3043
theorem OAI.PositiveEinsteinFour.Geometry.radial_state_domain_nhds line 3050
theorem OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow_zero_eventually line 3060
theorem OAI.PositiveEinsteinFour.Geometry.radialFlowContDiffAt_zero line 3079
theorem OAI.PositiveEinsteinFour.Geometry.radialFlowContDiffAt_of_chart line 3093
Source documentation
A derivative in one pair of actual charts gives the derivative in every pair of charts at the same source and target.
```
theorem radialFlowContDiffAt_of_chart (g : SmoothMetric M) (o : FrameOrientation g)
    (t : ℝ) (p : PositiveRadius × UnitTangentBundle g) (c₀ d₀ : M)
    (hc₀ : p.2.base ∈ (chartAt FourSpace c₀).source)
    (hd₀ : (unitTangentRadialFlow g o t p).2.base ∈ (chartAt FourSpace d₀).source)
    (hcore : ContDiffAt ℝ 1 (radialCoordinateFlow g o c₀ d₀ t)
      (unitRadialCotangentState g c₀ p)) : RadialFlowContDiffAt g o t p := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow, OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow, OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState, OAI.PositiveEinsteinFour.Geometry.RadialFlowContDiffAt
theorem OAI.PositiveEinsteinFour.Geometry.RadialFlowContDiffAt.add line 3119
theorem OAI.PositiveEinsteinFour.Geometry.RadialHamiltonianChart.contDiffAt line 3135
theorem OAI.PositiveEinsteinFour.Geometry.radialFlowContDiffAt_uniform_time line 3166
Source documentation
Compact radius slabs give one interval of continuously differentiable flow times.
```
theorem radialFlowContDiffAt_uniform_time (g : SmoothMetric M) (o : FrameOrientation g)
    (a b : ℝ) (ha : 0 < a) :
    ∃ ε > (0 : ℝ), ∀ p ∈ radialSlab g a b, ∀ t : ℝ, |t| < ε →
      RadialFlowContDiffAt g o t p := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.radialSlab, OAI.PositiveEinsteinFour.Geometry.RadialFlowContDiffAt
theorem OAI.PositiveEinsteinFour.Geometry.radialFlowContDiffAt_all_time line 3180
Source documentation
The constructed complete radial flow is continuously differentiable in its initial cotangent state at every time. No differentiability of a chosen global ODE solution is assumed.
```
theorem radialFlowContDiffAt_all_time (g : SmoothMetric M) (o : FrameOrientation g)
    (t : ℝ) (p : PositiveRadius × UnitTangentBundle g) :
    RadialFlowContDiffAt g o t p := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.RadialFlowContDiffAt
def OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.measurableSlice line 3241
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.measurableSlice_eq line 3246
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.measurable_measurableSlice line 3252
theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.measurableSlice_map_volume line 3261
theorem OAI.PositiveEinsteinFour.Geometry.actual_radialCotangentStateExtension_map line 3282
theorem OAI.PositiveEinsteinFour.Geometry.RadialHamiltonianChart.map_radialMeasure line 3301
Source documentation
Every actual Hamiltonian chart preserves the actual radial measure on its open domain for the full interval provided by that chart.
```
theorem RadialHamiltonianChart.map_radialMeasure (g : SmoothMetric M)
    (o : FrameOrientation g) (C : RadialHamiltonianChart g o)
    (t : ℝ) (ht : t ∈ Ioo (-C.flow.time) C.flow.time) :
    Measure.map (unitTangentRadialFlow g o t)
      (((Measure.volumeIoiPow 3).prod (canonicalUnitTangentMeasure g o)).restrict C.domain) =
      ((Measure.volumeIoiPow 3).prod (canonicalUnitTangentMeasure g o)).restrict
        (unitTangentRadialFlow g o t '' C.domain) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RadialHamiltonianChart, OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow, OAI.PositiveEinsteinFour.Geometry.canonicalUnitTangentMeasure
theorem OAI.PositiveEinsteinFour.Geometry.scalar_chart_ae_predicate line 3384
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow_measurePreserving line 3429
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentFlow_measurePreserving line 3445
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_measurePreserving line 3453
Source documentation
The actual parallel-frame flow preserves base Riemannian volume times orthonormal-fiber Haar probability, in every distinguished frame direction.
```
theorem parallelFrameFlowMap_measurePreserving (g : SmoothMetric M)
    (o : FrameOrientation g) (k : Fin 4) (t : ℝ) :
    MeasurePreserving (parallelFrameFlowMap g k t)
      (canonicalFrameMeasure g o) (canonicalFrameMeasure g o) :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure
theorem OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow_frame_endpoint line 3479
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_chart_contDiffAt_zero line 3499
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_chart_contDiffAt_nonzero line 3540
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_chart_contDiffAt line 3571
Source documentation
Every coordinate representation of the constructed exponential is C1 where its value belongs to that coordinate chart.
```
theorem frameExponential_chart_contDiffAt (g : SmoothMetric M)
    (o : FrameOrientation g) (d : M) (e : FrameBundle g) (v : FourSpace)
    (hd : frameExponential g o e v ∈ (chartAt FourSpace d).source) :
    ContDiffAt ℝ 1 (fun w : FourSpace => chartAt FourSpace d (frameExponential g o e w)) v := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameExponential
theorem OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow_local_factor line 3603
Source documentation
A local kinetic flow at the endpoint factors the complete coordinate flow on a neighborhood of its initial state.
```
theorem radialCoordinateFlow_local_factor (g : SmoothMetric M) (o : FrameOrientation g)
    (c d : M) (p : PositiveRadius × UnitTangentBundle g) (t : ℝ)
    (hc : p.2.base ∈ (chartAt FourSpace c).source)
    (hd : (unitTangentRadialFlow g o t p).2.base ∈ (chartAt FourSpace d).source) :
    ∃ F : KineticLocalFlow g d (unitRadialCotangentState g d (unitTangentRadialFlow g o t p)),
      ∀ s ∈ Ioo (-F.time) F.time,
        radialCoordinateFlow g o c d (s + t) =ᶠ[𝓝 (unitRadialCotangentState g c p)]
          (fun z => F.map (radialCoordinateFlow g o c d t z, s)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow, OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow, OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState, OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow
theorem OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow_fderiv_hasDerivAt line 3630
Source documentation
The true spatial derivative, rather than a separately chosen solution, satisfies the linearized Hamiltonian equation at every valid chart time.
```
theorem radialCoordinateFlow_fderiv_hasDerivAt (g : SmoothMetric M)
    (o : FrameOrientation g) (c d : M) (p : PositiveRadius × UnitTangentBundle g)
    (t : ℝ) (hc : p.2.base ∈ (chartAt FourSpace c).source)
    (hd : (unitTangentRadialFlow g o t p).2.base ∈ (chartAt FourSpace d).source) :
    HasDerivAt
      (fun s => fderiv ℝ (radialCoordinateFlow g o c d s) (unitRadialCotangentState g c p))
      ((fderiv ℝ (cotangentHamiltonianField (kineticHamiltonian g d))
          (unitRadialCotangentState g d (unitTangentRadialFlow g o t p))).comp
        (fderiv ℝ (radialCoordinateFlow g o c d t) (unitRadialCotangentState g c p))) t := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.PositiveRadius, OAI.PositiveEinsteinFour.Geometry.UnitTangentBundle, OAI.PositiveEinsteinFour.Geometry.unitTangentRadialFlow, OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow, OAI.PositiveEinsteinFour.Geometry.unitRadialCotangentState, OAI.PositiveEinsteinFour.Geometry.cotangentHamiltonianField, OAI.PositiveEinsteinFour.Geometry.kineticHamiltonian
def OAI.PositiveEinsteinFour.Geometry.canonicalParallelMetricData line 3695
def OAI.PositiveEinsteinFour.Geometry.actualCanonicalData line 3700
theorem OAI.PositiveEinsteinFour.Geometry.models_of_actual_canonical_data line 3713
Source documentation
Analytic, polar, topological and rigidity hypotheses imply the two-model oriented classification.
```
theorem models_of_actual_canonical_data (g : SmoothMetric M) (o : FrameOrientation g)
    (hRic : RicciThree g)
    (poisson : PetersenPoissonInput g (canonicalFrameMeasure g o))
    (jacobi : JacobiRealizationData (canonicalParallelMetricData g o 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.RicciThree, OAI.PositiveEinsteinFour.Geometry.PetersenPoissonInput, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.JacobiRealizationData, OAI.PositiveEinsteinFour.Geometry.canonicalParallelMetricData, OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunGapInput, OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunHodgeInput, OAI.PositiveEinsteinFour.Geometry.DerdzinskiHitchinInput
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_chart_contDiffAt_zero_order line 3746
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_chart_smoothAt_zero line 3784
theorem OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow_position_change_eventually line 3810
theorem OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow_position_fderiv_change line 3833
def OAI.PositiveEinsteinFour.Geometry.radialVariationInFrame line 3871
theorem OAI.PositiveEinsteinFour.Geometry.radialVariationInFrame_chart_independent line 3877
def OAI.PositiveEinsteinFour.Geometry.actualJacobiMatrix line 3925
theorem OAI.PositiveEinsteinFour.Geometry.actualRegularJacobi_truncatedDensity_eq line 3929
theorem OAI.PositiveEinsteinFour.Geometry.actualRegularJacobi_truncatedDensity_scaled line 3938
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiDensity_integrable_of_continuous line 3948
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiDensity_intervalIntegrable_of_continuous line 3960
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiDensity_integrable line 3983
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiDensity_intervalIntegrable line 3990
def OAI.PositiveEinsteinFour.Geometry.frameUnitRadialState line 4018
def OAI.PositiveEinsteinFour.Geometry.frameKineticCurve line 4021
def OAI.PositiveEinsteinFour.Geometry.frameKineticVariation line 4025
def OAI.PositiveEinsteinFour.Geometry.frameGeodesicCoordinateCurve line 4030
def OAI.PositiveEinsteinFour.Geometry.frameGeodesicCoordinateVariation line 4034
theorem OAI.PositiveEinsteinFour.Geometry.frameUnitRadialState_flow line 4039
theorem OAI.PositiveEinsteinFour.Geometry.frameKineticCurve_eq line 4046
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesicCoordinateCurve_position line 4054
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesicCoordinateCurve_velocity line 4062
theorem OAI.PositiveEinsteinFour.Geometry.frameKineticCurve_hasDerivAt line 4072
theorem OAI.PositiveEinsteinFour.Geometry.frameKineticVariation_hasDerivAt line 4080
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesicCoordinateCurve_hasDerivAt line 4091
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesicCoordinateVariation_hasDerivAt line 4101
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesicCoordinateVariation_fst line 4116
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_normal_variation line 4129
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormExterior_covariant line 4176
def OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Pairing line 4230
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneForm_pairing_integrable line 4234
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Pairing_comm line 4243
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Pairing_add line 4252
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Pairing_smul line 4260
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Pairing_self line 4266
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Pairing_sub line 4272
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Pairing_nonneg line 4279
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormL2Pairing_definite line 4285
def OAI.PositiveEinsteinFour.Geometry.smoothScalarModule line 4312
Source documentation
Smooth real scalar functions, with their pointwise vector-space structure.
```
def smoothScalarModule (M : Type*) [TopologicalSpace M] [ChartedSpace FourSpace M] :
    Submodule ℝ (M → ℝ) where
…
```
abbrev OAI.PositiveEinsteinFour.Geometry.SmoothScalar line 4321
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarData line 4323
def OAI.PositiveEinsteinFour.Geometry.smoothScalarValue line 4329
Source documentation
Viewing a smooth scalar on the orthonormal frame bundle.
```
def smoothScalarValue (g : SmoothMetric M) :
    SmoothScalar (M := M) →ₗ[ℝ] C(FrameBundle g, ℝ) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.SmoothScalar, OAI.PositiveEinsteinFour.Geometry.FrameBundle
def OAI.PositiveEinsteinFour.Geometry.smoothScalarGradient line 4336
Source documentation
Each actual frame component of the scalar differential is linear.
```
def smoothScalarGradient {μ : Measure (FrameBundle g)}
    (d : ParallelMetricData g μ) (i : Fin 4) :
    SmoothScalar (M := M) →ₗ[ℝ] C(FrameBundle g, ℝ) where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.SmoothScalar
abbrev OAI.PositiveEinsteinFour.Geometry.ScalarL2 line 4359
def OAI.PositiveEinsteinFour.Geometry.smoothScalarValueL2 line 4361
def OAI.PositiveEinsteinFour.Geometry.smoothScalarGradientL2 line 4366
def OAI.PositiveEinsteinFour.Geometry.smoothScalarDirichlet line 4371
Source documentation
The actual scalar Dirichlet pairing in the frame measure.
```
def smoothScalarDirichlet (d : ParallelMetricData g μ)
    (a b : SmoothScalar (M := M)) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.SmoothScalar
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDirichlet_eq_integral line 4375
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDirichlet_green line 4393
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDirichlet_nonneg line 4399
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDirichlet_symm line 4403
abbrev OAI.PositiveEinsteinFour.Geometry.ScalarJetL2 line 4410
Source documentation
The value and four derivative coordinates, in a genuine Hilbert product.
```
abbrev ScalarJetL2 (g : SmoothMetric M) (μ : Measure (FrameBundle g)) :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle
def OAI.PositiveEinsteinFour.Geometry.smoothScalarFirstJet line 4413
def OAI.PositiveEinsteinFour.Geometry.scalarH1 line 4421
Source documentation
Intrinsic first-order Sobolev space generated by actual smooth scalars.
```
def scalarH1 (d : ParallelMetricData g μ) : Submodule ℝ (ScalarJetL2 g μ) :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.ScalarJetL2
instance OAI.PositiveEinsteinFour.Geometry.scalarH1_complete line 4424
def OAI.PositiveEinsteinFour.Geometry.scalarH1Value line 4428
def OAI.PositiveEinsteinFour.Geometry.scalarH1Gradient line 4431
def OAI.PositiveEinsteinFour.Geometry.smoothScalarToH1 line 4435
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_inner line 4439
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Value_smooth line 4446
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Gradient_smooth line 4450
def OAI.PositiveEinsteinFour.Geometry.scalarShiftedSolution line 4456
Source documentation
The weak solution of the shifted scalar equation. Its construction is the Hilbert adjoint of value evaluation, so needs no elliptic premise.
```
def scalarShiftedSolution (d : ParallelMetricData g μ) : ScalarL2 g μ →L[ℝ] scalarH1 d :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.ScalarL2, OAI.PositiveEinsteinFour.Geometry.scalarH1
theorem OAI.PositiveEinsteinFour.Geometry.scalarShiftedSolution_weak line 4459
theorem OAI.PositiveEinsteinFour.Geometry.scalarShiftedSolution_unique line 4467
def OAI.PositiveEinsteinFour.Geometry.scalarWeakResolvent line 4485
Source documentation
The value of the weak shifted solution, as an operator on scalar L².
```
def scalarWeakResolvent (d : ParallelMetricData g μ) : ScalarL2 g μ →L[ℝ] ScalarL2 g μ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.ScalarL2
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeakResolvent_symmetric line 4488
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeakResolvent_nonneg line 4496
theorem OAI.PositiveEinsteinFour.Geometry.frameTensorPairing_three line 4518
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameValue_inner line 4528
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner_eq_frame line 4535
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCurvatureInner_eq_frame line 4545
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCovariantEnergy_eq_frame line 4556
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_direction_green line 4590
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_rough_green line 4614
def OAI.PositiveEinsteinFour.Geometry.ActualJacobiPolarInput line 4679
def OAI.PositiveEinsteinFour.Geometry.actualJacobiRealizationData line 4689
def OAI.PositiveEinsteinFour.Geometry.actualCanonicalData_of_polar line 4701
theorem OAI.PositiveEinsteinFour.Geometry.models_of_actual_polar_data line 4712
theorem OAI.PositiveEinsteinFour.Jacobi.positive_of_continuousOn_nonzero line 4742
theorem OAI.PositiveEinsteinFour.Jacobi.jacobi_det_pos_of_preconjugate line 4750
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.det_pos_of_preconjugate line 4768
theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.det_pos_of_preconjugate line 4777
theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.truncatedDensity_nonneg line 4786
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_det_pos_of_preconjugate line 4810
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_abs_det_eq_truncatedDensity line 4816
def OAI.PositiveEinsteinFour.Geometry.actualNormalVariationPosition line 4848
def OAI.PositiveEinsteinFour.Geometry.actualNormalVariationVelocity line 4853
theorem OAI.PositiveEinsteinFour.Geometry.actualNormalVariationPosition_eq_chart line 4857
theorem OAI.PositiveEinsteinFour.Geometry.actualNormalVariationPosition_eventually_chart line 4879
theorem OAI.PositiveEinsteinFour.Geometry.actualNormalVariationPosition_hasDerivAt line 4892
theorem OAI.PositiveEinsteinFour.Geometry.actualNormalVariationVelocity_eq_chart line 4904
theorem OAI.PositiveEinsteinFour.Geometry.actualNormalVariationVelocity_hasDerivAt line 4914
structure OAI.PositiveEinsteinFour.Geometry.SmoothL2OneForm line 4956
def OAI.PositiveEinsteinFour.Geometry.smoothL2OneFormEquiv line 4959
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 4966) line 4966
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 4968) line 4968
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 4969) line 4969
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 4970) line 4970
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 4971) line 4971
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 4972) line 4972
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 4973) line 4973
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 4974) line 4974
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 4976) line 4976
def OAI.PositiveEinsteinFour.Geometry.smoothL2OneFormAddHom line 4980
instance OAI.PositiveEinsteinFour.Geometry.(instance at line 4985) line 4985
instance OAI.PositiveEinsteinFour.Geometry.smoothOneFormInnerCore line 4989
instance OAI.PositiveEinsteinFour.Geometry.smoothOneFormNormedAddCommGroup line 5003
instance OAI.PositiveEinsteinFour.Geometry.smoothOneFormInnerProductSpace line 5006
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneForm_inner_eq line 5009
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneForm_norm_sq line 5012
def OAI.PositiveEinsteinFour.Geometry.OneFormL2 line 5018
def OAI.PositiveEinsteinFour.Geometry.smoothOneFormToL2 line 5021
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormToL2_dense line 5024
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormToL2_injective line 5027
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormToL2_inner line 5030
def OAI.PositiveEinsteinFour.Geometry.regularizedPlusWeylScalar line 5057
Source documentation
Positive regularization makes the Weyl cube root smooth even on its zero set.
```
def regularizedPlusWeylScalar (o : FrameOrientation g) (ε : ℝ) (hε : 0 < ε) :
    SmoothScalar (M := M) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.SmoothScalar
theorem OAI.PositiveEinsteinFour.Geometry.regularizedPlusWeylScalar_frame line 5067
theorem OAI.PositiveEinsteinFour.Geometry.regularizedPlusWeylScalar_gradient line 5074
theorem OAI.PositiveEinsteinFour.Geometry.regularizedPlusWeylScalar_moment line 5096
theorem OAI.PositiveEinsteinFour.Geometry.regularizedPlusWeylScalar_dirichlet line 5115
def OAI.PositiveEinsteinFour.Geometry.SharpScalarSobolev line 5132
Source documentation
The sharp scalar inequality in normalized base volume, with the actual Dirichlet pairing. Its geometric proof is independent of this transfer.
```
def SharpScalarSobolev (o : FrameOrientation g)
    (p : ParallelMetricData g (canonicalFrameMeasure g o)) : Prop :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure
theorem OAI.PositiveEinsteinFour.Geometry.sharpScalarSobolev_regularized line 5138
theorem OAI.PositiveEinsteinFour.Geometry.canonicalParallelMetricData_orientation line 5153
theorem OAI.PositiveEinsteinFour.Geometry.plus_gap_of_sharpScalarSobolev line 5163
Source documentation
Actual smooth scalar Sobolev suffices for the Weyl gap. No special Sobolev premise on frame fields or their derivatives is needed.
```
theorem plus_gap_of_sharpScalarSobolev (o : FrameOrientation g) (hRic : RicciThree g)
    (hsharp : SharpScalarSobolev o (canonicalParallelMetricData g o hRic))
    (hnonzero : ∃ x, plusNorm o x ≠ 0) :
    1 ≤ ∫ x, plusNorm o x ^ 2 ∂normalizedVolume g := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.SharpScalarSobolev, OAI.PositiveEinsteinFour.Geometry.canonicalParallelMetricData, OAI.PositiveEinsteinFour.Geometry.plusNorm, OAI.PositiveEinsteinFour.Geometry.normalizedVolume

theorem OAI.PositiveEinsteinFour.Geometry.scalar_C1_representative_of_local line 5196

Source documentation

The gluing uses only the actual full-support volume and local smooth representatives. No global C1 regularity or elliptic premise is assumed.

theorem scalar_C1_representative_of_local (g : SmoothMetric M)
    (b : Lp ℝ 2 (normalizedVolume g))
    (hlocal : ∀ x : M, ∃ U : Set M, ∃ f : M → ℝ,
      IsOpen U ∧ x ∈ U ∧ ContMDiffOn I4 𝓘(ℝ, ℝ) 1 f U ∧
        (b : M → ℝ) =ᵐ[(normalizedVolume g).restrict U] f) :
    ∃ F : M → ℝ, ContMDiff I4 𝓘(ℝ, ℝ) 1 F ∧ F =ᵐ[normalizedVolume g] b := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.normalizedVolume

def OAI.PositiveEinsteinFour.Geometry.scalarChartLift line 5256
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartLift_on_source line 5261
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartLift_symm line 5267
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartLift_support line 5274
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartLift_smooth line 5283
def OAI.PositiveEinsteinFour.Geometry.scalarChartTest line 5304

theorem OAI.PositiveEinsteinFour.Geometry.scalar_continuous_representative_of_local line 5332

Source documentation

The gluing uses only the actual full-support volume and local smooth representatives. No global continuity or elliptic premise is assumed.

theorem scalar_continuous_representative_of_local (g : SmoothMetric M)
    (b : Lp ℝ 2 (normalizedVolume g))
    (hlocal : ∀ x : M, ∃ U : Set M, ∃ f : M → ℝ,
      IsOpen U ∧ x ∈ U ∧ ContinuousOn f U ∧
        (b : M → ℝ) =ᵐ[(normalizedVolume g).restrict U] f) :
    ∃ F : M → ℝ, Continuous F ∧ F =ᵐ[normalizedVolume g] b := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.normalizedVolume

def OAI.PositiveEinsteinFour.Geometry.smoothScalarCompose line 5394
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarCompose_gradient line 5398
theorem OAI.PositiveEinsteinFour.Geometry.scalarValueL2_coe line 5421
theorem OAI.PositiveEinsteinFour.Geometry.scalarGradientL2_coe line 5425
theorem OAI.PositiveEinsteinFour.Geometry.scalarCompose_value line 5430
theorem OAI.PositiveEinsteinFour.Geometry.scalarCompose_gradient line 5443

theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_compose_exists line 5463

Source documentation

Composition by a smooth function with bounded derivative preserves the actual scalar H¹ closure and has the expected four weak derivatives.

theorem scalarH1_compose_exists (d : ParallelMetricData g μ)
    (φ : ℝ → ℝ) (hφ : ContDiff ℝ ∞ φ) {C : ℝ≥0}
    (hLip : LipschitzWith C φ) (hzero : φ 0 = 0)
    {D : ℝ} (hD : 0 ≤ D) (hbound : ∀ r, |deriv φ r| ≤ D)
    (u : scalarH1 d) :
    ∃ v : scalarH1 d, scalarH1Value d v = hLip.compLp hzero (scalarH1Value d u) ∧
      ∀ i : Fin 4, scalarH1Gradient d i v =ᵐ[μ]
        fun e => deriv φ (scalarH1Value d u e) * scalarH1Gradient d i u e := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.scalarH1Value, OAI.PositiveEinsteinFour.Geometry.scalarH1Gradient

theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_compose_exists_of_deriv_bound line 5533

Source documentation

A bound on the ordinary derivative supplies the Lipschitz hypothesis.

theorem scalarH1_compose_exists_of_deriv_bound (d : ParallelMetricData g μ)
    (φ : ℝ → ℝ) (hφ : ContDiff ℝ ∞ φ) (hzero : φ 0 = 0)
    {D : ℝ≥0} (hbound : ∀ r, |deriv φ r| ≤ D) (u : scalarH1 d) :
    ∃ v : scalarH1 d,
      (scalarH1Value d v : FrameBundle g → ℝ) =ᵐ[μ]
        (fun e => φ (scalarH1Value d u e)) ∧
      ∀ i : Fin 4, scalarH1Gradient d i v =ᵐ[μ]
        fun e => deriv φ (scalarH1Value d u e) * scalarH1Gradient d i u e := by
…

def OAI.PositiveEinsteinFour.Geometry.scalarBasePullback line 5578
theorem OAI.PositiveEinsteinFour.Geometry.scalarBasePullback_closed line 5582
def OAI.PositiveEinsteinFour.Geometry.smoothScalarBaseL2 line 5586
theorem OAI.PositiveEinsteinFour.Geometry.scalarBasePullback_smooth line 5590
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_base_representative line 5606
Source documentation
No extra dependence on the orthonormal frame appears in the value coordinate when completing smooth scalar first jets.
```
theorem scalarH1_base_representative (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) (u : scalarH1 d) :
    ∃ f : Lp ℝ 2 (normalizedVolume g), scalarBasePullback g o f = scalarH1Value d u := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.normalizedVolume, OAI.PositiveEinsteinFour.Geometry.scalarBasePullback, OAI.PositiveEinsteinFour.Geometry.scalarH1Value
theorem OAI.PositiveEinsteinFour.Geometry.continuous_pairwise_square_integral line 5647
Source documentation
Pairwise square oscillation is twice the variance for a probability measure. Both integrals are ordinary real Bochner integrals.
```
theorem continuous_pairwise_square_integral (a : C(X, ℝ)) :
    (∫ x, ∫ y, (a x - a y) ^ 2 ∂μ ∂μ) =
      2 * ((∫ x, (a x) ^ 2 ∂μ) - (∫ x, a x ∂μ) ^ 2) := by
…
```
theorem OAI.PositiveEinsteinFour.Geometry.continuous_pairwise_square_integral_of_mean_zero line 5680
def OAI.PositiveEinsteinFour.Geometry.smoothScalarConst line 5694
Source documentation
A constant as an actual smooth scalar function.
```
def smoothScalarConst (c : ℝ) : SmoothScalar (M := M) :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.SmoothScalar
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarGradient_const line 5697
def OAI.PositiveEinsteinFour.Geometry.scalarL2One line 5710
Source documentation
The constant one in scalar L².
```
def scalarL2One (g : SmoothMetric M) (μ : Measure (FrameBundle g))
    [CompactSpace (FrameBundle g)] [IsFiniteMeasure μ] : ScalarL2 g μ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.ScalarL2
def OAI.PositiveEinsteinFour.Geometry.scalarH1One line 5715
Source documentation
The genuine constant first jet, with zero derivative coordinates.
```
def scalarH1One (d : ParallelMetricData g μ) : scalarH1 d :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Value_one line 5718
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Gradient_one line 5721
def OAI.PositiveEinsteinFour.Geometry.scalarH1Mean line 5729
Source documentation
Integration of the value coordinate, represented by inner product with the constant one and hence continuous on the actual H¹ completion.
```
def scalarH1Mean (d : ParallelMetricData g μ) : scalarH1 d →L[ℝ] ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Mean_apply line 5732
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Mean_smooth line 5735
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Mean_eq_inner_one line 5745
def OAI.PositiveEinsteinFour.Geometry.scalarH1MeanZero line 5752
Source documentation
The closed subspace on which the actual value coordinate has mean zero.
```
def scalarH1MeanZero (d : ParallelMetricData g μ) : Submodule ℝ (scalarH1 d) :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1MeanZero_closed line 5755
theorem OAI.PositiveEinsteinFour.Geometry.mem_scalarH1MeanZero line 5759
instance OAI.PositiveEinsteinFour.Geometry.scalarH1MeanZero_complete line 5762
def OAI.PositiveEinsteinFour.Geometry.scalarH1SubtractMean line 5767
Source documentation
Subtract the constant jet with coefficient equal to the scalar mean.
```
def scalarH1SubtractMean (d : ParallelMetricData g μ) : scalarH1 d →L[ℝ] scalarH1 d :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1SubtractMean_apply line 5770
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Gradient_subtractMean line 5773
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Value_subtractMean line 5779
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Mean_one line 5786
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Mean_subtractMean line 5791
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1SubtractMean_eq_self line 5797
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1SubtractMean_idempotent line 5802
def OAI.PositiveEinsteinFour.Geometry.scalarH1MeanZeroProjection line 5808
Source documentation
The mean-subtraction projection with its closed mean-zero codomain.
```
def scalarH1MeanZeroProjection (d : ParallelMetricData g μ) :
    scalarH1 d →L[ℝ] scalarH1MeanZero d :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.scalarH1MeanZero
def OAI.PositiveEinsteinFour.Geometry.smoothScalarSubtractMean line 5814
Source documentation
Subtracting the actual integral preserves smoothness.
```
def smoothScalarSubtractMean (a : SmoothScalar (M := M)) : SmoothScalar (M := M) :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.SmoothScalar
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarSubtractMean_toH1 line 5818
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarGradient_subtractMean line 5829
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarGradientL2_subtractMean line 5837
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarSubtractMean_mean_zero line 5844

theorem OAI.PositiveEinsteinFour.Geometry.scalar_smooth_representative_of_local line 5875

Source documentation

The gluing uses only the actual full-support volume and local smooth representatives. No global smoothness or elliptic premise is assumed.

theorem scalar_smooth_representative_of_local (g : SmoothMetric M)
    (b : Lp ℝ 2 (normalizedVolume g))
    (hlocal : ∀ x : M, ∃ U : Set M, ∃ f : M → ℝ,
      IsOpen U ∧ x ∈ U ∧ ContMDiffOn I4 𝓘(ℝ, ℝ) ∞ f U ∧
        (b : M → ℝ) =ᵐ[(normalizedVolume g).restrict U] f) :
    ∃ F : SmoothScalar (M := M), F.val =ᵐ[normalizedVolume g] b := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.normalizedVolume, OAI.PositiveEinsteinFour.Geometry.SmoothScalar

def OAI.PositiveEinsteinFour.Geometry.smoothScalarLaplacianField line 5936
def OAI.PositiveEinsteinFour.Geometry.smoothScalarLaplacianL2 line 5941
def OAI.PositiveEinsteinFour.Geometry.smoothScalarShiftedRhs line 5944
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarShiftedRhs_pairing line 5947
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_eq_of_smooth_tests line 5960
theorem OAI.PositiveEinsteinFour.Geometry.scalarShiftedSolution_smooth line 5976
Source documentation
The Hilbert construction inverts 1 - Δ on every actual smooth scalar. This identifies the weak resolvent with the geometric operator.
```
theorem scalarShiftedSolution_smooth (d : ParallelMetricData g μ)
    (a : SmoothScalar (M := M)) :
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.SmoothScalar
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeakResolvent_smooth line 5987
def OAI.PositiveEinsteinFour.Geometry.smoothScalarCovariantField line 6014
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarCovariantField_coordinates line 6020
def OAI.PositiveEinsteinFour.Geometry.covariantScalarFunction line 6025
theorem OAI.PositiveEinsteinFour.Geometry.covariantScalarFunction_smooth line 6027
def OAI.PositiveEinsteinFour.Geometry.smoothCovariantScalar line 6040
def OAI.PositiveEinsteinFour.Geometry.smoothScalarDifferential line 6043
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDifferential_framed line 6046
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDifferential_derivative line 6057
def OAI.PositiveEinsteinFour.Geometry.twoFormExteriorTensor line 6082
theorem OAI.PositiveEinsteinFour.Geometry.twoFormExteriorTensor_apply line 6086
theorem OAI.PositiveEinsteinFour.Geometry.twoFormExteriorTensor_frame line 6098
def OAI.PositiveEinsteinFour.Geometry.twoFormCodiffTensor line 6104
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodiffTensor_apply line 6107
theorem OAI.PositiveEinsteinFour.Geometry.trace_three_frame line 6110
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCodiffTensor_frame line 6127
theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamQuadratic_tensor line 6153
theorem OAI.PositiveEinsteinFour.Geometry.twoFormDeRhamQuadratic_frame line 6171
abbrev OAI.PositiveEinsteinFour.Geometry.TwoTensorEuclidean line 6196
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormEuclideanValue line 6204
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormEuclideanTrace line 6208
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormTensorValueL2 line 6212
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormTensorTraceL2 line 6215
theorem OAI.PositiveEinsteinFour.Geometry.continuousTwoTensor_inner_toLp line 6218
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormTensorValueL2_norm_sq line 6228
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormTensorValueL2_norm_le line 6246
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormTensorValueTrace_inner line 6255
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCovariantEnergy_L2_bound line 6267
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_mixed_green line 6304
def OAI.PositiveEinsteinFour.Geometry.covariantMetricTraceThree line 6344
theorem OAI.PositiveEinsteinFour.Geometry.covariantMetricTraceThree_frame line 6347
def OAI.PositiveEinsteinFour.Geometry.covariantMetricTraceField line 6391
theorem OAI.PositiveEinsteinFour.Geometry.covariantMetricTraceField_framed line 6395
theorem OAI.PositiveEinsteinFour.Geometry.covariantFieldFramed_chart line 6402
theorem OAI.PositiveEinsteinFour.Jacobi.firstEigenvalue_eventually_neg line 6428
theorem OAI.PositiveEinsteinFour.Jacobi.trace_first_mode_curvatureDirichlet line 6439
Source documentation
On the first sine mode a trace-free curvature defect has zero trace.
```
theorem trace_first_mode_curvatureDirichlet {N : ℕ} (hN : 0 < N)
    (t : ℝ) (A : Fin N → NormalMatrix) (hA : ∀ i, (A i).trace = 0) :
    ((modeEmbedding (unitFirstSineVector N))ᵀ * curvatureDirichlet t A *
      modeEmbedding (unitFirstSineVector N)).trace = 3 * firstEigenvalue t N := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.modeEmbedding, OAI.PositiveEinsteinFour.Jacobi.unitFirstSineVector, OAI.PositiveEinsteinFour.Jacobi.curvatureDirichlet, OAI.PositiveEinsteinFour.Jacobi.firstEigenvalue
theorem OAI.PositiveEinsteinFour.Jacobi.firstEigenvalue_nonneg_of_curvatureDirichlet line 6460
theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.le_pi_of_preconjugate line 6471
Source documentation
The Einstein trace condition forces a conjugate point by any time strictly greater than π.
```
theorem RegularJacobi.le_pi_of_preconjugate {t : ℝ} (d : RegularJacobi t)
    (htrace : ∀ s, (d.R s).trace = 3)
    (hpre : ∀ s, 0 < s → s ≤ t → IsUnit (d.J s)) : t ≤ Real.pi := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.RegularJacobi
theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.exists_singular_of_pi_lt line 6489
theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.truncatedDensity_eq_zero_of_pi_lt line 6496
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvature_trace line 6517
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_le_pi_of_preconjugate line 6522
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_exists_singular_of_pi_lt line 6530
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_truncatedDensity_eq_zero_of_pi_lt line 6537
theorem OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow_self_zero_fderiv line 6565
def OAI.PositiveEinsteinFour.Geometry.frameNormalInitialVariation line 6583
theorem OAI.PositiveEinsteinFour.Geometry.actualNormalVariation_initial line 6589
theorem OAI.PositiveEinsteinFour.Geometry.actualNormalVariation_eq_jacobi line 6626
theorem OAI.PositiveEinsteinFour.Geometry.frameReflectionMatrix_det line 6663
theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.reflect_det line 6669
def OAI.PositiveEinsteinFour.Geometry.FrameOrientation.reversed line 6676
Source documentation
The opposite orientation is the pullback of the original orientation through the concrete single-axis reflection.
```
def FrameOrientation.reversed (o : FrameOrientation g) : FrameOrientation g where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation
theorem OAI.PositiveEinsteinFour.Geometry.FrameOrientation.mem_reversed_iff line 6690
theorem OAI.PositiveEinsteinFour.Geometry.FrameOrientation.reversed_positive_iff_not line 6693
theorem OAI.PositiveEinsteinFour.Geometry.plusNorm_reversed line 6709
theorem OAI.PositiveEinsteinFour.Geometry.minusNorm_reversed line 6718
theorem OAI.PositiveEinsteinFour.Geometry.minus_gap_of_sharpScalarSobolev line 6735
Source documentation
The same sharp scalar inequality, used with the opposite orientation, gives the minus-block gap.
```
theorem minus_gap_of_sharpScalarSobolev (o : FrameOrientation g) (hRic : RicciThree g)
    (hsharp : SharpScalarSobolev o.reversed (canonicalParallelMetricData g o.reversed hRic))
    (hnonzero : ∃ x, minusNorm o x ≠ 0) :
    1 ≤ ∫ x, minusNorm o x ^ 2 ∂normalizedVolume g := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.SharpScalarSobolev, OAI.PositiveEinsteinFour.Geometry.canonicalParallelMetricData, OAI.PositiveEinsteinFour.Geometry.minusNorm, OAI.PositiveEinsteinFour.Geometry.normalizedVolume
theorem OAI.PositiveEinsteinFour.Geometry.gurskyLeBrunGap_of_sharpScalarSobolev line 6746
Source documentation
Both scalar Sobolev instances suffice for the original geometric gap input. The sharp scalar premise remains explicit.
```
theorem gurskyLeBrunGap_of_sharpScalarSobolev (o : FrameOrientation g) (hRic : RicciThree g)
    (hplus : SharpScalarSobolev o (canonicalParallelMetricData g o hRic))
    (hminus : SharpScalarSobolev o.reversed (canonicalParallelMetricData g o.reversed hRic)) :
    GurskyLeBrunGapInput g o :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.SharpScalarSobolev, OAI.PositiveEinsteinFour.Geometry.canonicalParallelMetricData, OAI.PositiveEinsteinFour.Geometry.GurskyLeBrunGapInput
structure OAI.PositiveEinsteinFour.RemainingOrientedData line 6772
def OAI.PositiveEinsteinFour.RemainingOrientedInputs line 6782
theorem OAI.PositiveEinsteinFour.RemainingOrientedInputs.toPublished line 6788
structure OAI.PositiveEinsteinFour.RemainingClassificationInputs line 6799
theorem OAI.PositiveEinsteinFour.classificationOn_of_remaining_inputs line 6807
Source documentation
The S4/CP2/RP4 classification under the Poisson, polar comparison, Weyl gap, Hodge and half-flat model hypotheses.
```
theorem classificationOn_of_remaining_inputs (h : RemainingClassificationInputs M) :
    ClassificationOn M :=
…
```
Mentions: OAI.PositiveEinsteinFour.RemainingClassificationInputs, OAI.PositiveEinsteinFour.ClassificationOn
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDifferential_closed line 6831
def OAI.PositiveEinsteinFour.Geometry.smoothScalarCovariantLinear line 6866
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDifferential_add line 6871
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDifferential_smul line 6880
def OAI.PositiveEinsteinFour.Geometry.smoothScalarDifferentialLinear line 6887
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDifferential_const line 6893
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_value_derivative line 6923
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_gradient_derivative line 6938
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_pairing_green line 6947
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_laplacian_symmetric line 6977
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_laplacian_continuous line 6998
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_laplacian_base_symmetric line 7011
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_jet_limit line 7047
def OAI.PositiveEinsteinFour.Geometry.scalarKatoTest line 7088
def OAI.PositiveEinsteinFour.Geometry.scalarKatoSquare line 7090
def OAI.PositiveEinsteinFour.Geometry.scalarKatoTestRate line 7092
def OAI.PositiveEinsteinFour.Geometry.scalarKatoSquareRate line 7095
theorem OAI.PositiveEinsteinFour.Geometry.scalarKato_den_pos line 7098
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoTest_smooth line 7101
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoSquare_smooth line 7106
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoTest_hasDerivAt line 7112
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoSquare_hasDerivAt line 7123
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoTest_deriv line 7145
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoSquare_deriv line 7149
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoTest_zero line 7153
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoSquare_zero line 7156
theorem OAI.PositiveEinsteinFour.Geometry.scalarKato_test_square line 7159
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoTest_abs_le line 7165
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoSquare_sq_le line 7175
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoTestRate_nonneg line 7183
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoTestRate_le line 7188
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoSquareRate_sq_le line 7195
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoSquareRate_abs_le line 7213
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoSquare_tendsto line 7226

theorem OAI.PositiveEinsteinFour.Geometry.scalarKato_memLp_eight_of_bound line 7239

Source documentation

A uniform fourth-moment bound for the rational square tests gives the eighth moment of the original function by Fatou's lemma.

theorem scalarKato_memLp_eight_of_bound {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {f : X → ℝ} (hf : AEStronglyMeasurable f μ)
    {C : ℝ≥0∞} (hC : C ≠ (∞ : ℝ≥0∞))
    (hbound : ∀ lam : ℝ, 0 < lam →
      eLpNorm (fun x => scalarKatoSquare lam (f x)) 4 μ ≤ C) : MemLp f 8 μ := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarKatoSquare

theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_katoTest_exists line 7266
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_katoSquare_exists line 7283
def OAI.PositiveEinsteinFour.Geometry.scalarNegativeTest line 7316
theorem OAI.PositiveEinsteinFour.Geometry.scalarNegativeTest_smooth line 7318
theorem OAI.PositiveEinsteinFour.Geometry.scalarNegativeTest_zero line 7321
theorem OAI.PositiveEinsteinFour.Geometry.scalarNegativeTest_nonpos line 7324
theorem OAI.PositiveEinsteinFour.Geometry.scalarNegativeTest_eq_zero line 7327
theorem OAI.PositiveEinsteinFour.Geometry.scalarNegativeTest_neg line 7330
theorem OAI.PositiveEinsteinFour.Geometry.scalarNegativeTest_monotone line 7333
theorem OAI.PositiveEinsteinFour.Geometry.scalarNegativeTest_deriv_nonneg line 7337
theorem OAI.PositiveEinsteinFour.Geometry.scalarNegativeTest_deriv_bound line 7340
theorem OAI.PositiveEinsteinFour.Geometry.scalarNegativeTest_product_nonneg line 7365
def OAI.PositiveEinsteinFour.Geometry.scalarNonlinearTruncation line 7387
def OAI.PositiveEinsteinFour.Geometry.scalarNonlinearTruncationDerivative line 7390
theorem OAI.PositiveEinsteinFour.Geometry.scalarNonlinearTruncation_smooth line 7394
theorem OAI.PositiveEinsteinFour.Geometry.scalarNonlinearTruncation_hasDeriv line 7401
theorem OAI.PositiveEinsteinFour.Geometry.scalarNonlinearTruncation_deriv line 7417
theorem OAI.PositiveEinsteinFour.Geometry.scalarNonlinearTruncation_zero line 7421
theorem OAI.PositiveEinsteinFour.Geometry.scalarNonlinearTruncation_power_bound line 7425
theorem OAI.PositiveEinsteinFour.Geometry.scalarNonlinearTruncation_bracket_bound line 7436
theorem OAI.PositiveEinsteinFour.Geometry.scalarNonlinearTruncation_deriv_growth line 7449
theorem OAI.PositiveEinsteinFour.Geometry.scalarNonlinearTruncation_deriv_bounded line 7462
def OAI.PositiveEinsteinFour.Geometry.fourGradientDirichlet line 7497
theorem OAI.PositiveEinsteinFour.Geometry.fourGradientDirichlet_apply line 7502
def OAI.PositiveEinsteinFour.Geometry.fourGradientSolution line 7514
theorem OAI.PositiveEinsteinFour.Geometry.fourGradientSolution_weak line 7518
theorem OAI.PositiveEinsteinFour.Geometry.fourGradientSolution_unique line 7528
def OAI.PositiveEinsteinFour.Geometry.SmoothScalarPoincare line 7560
Source documentation
The estimate needed here, stated solely for actual smooth mean-zero scalars. The geometric Poincaré theorem supplies this hypothesis.
```
def SmoothScalarPoincare (d : ParallelMetricData g μ) (K : ℝ) : Prop :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_centered_poincare line 7567
Source documentation
Center the value coordinate before taking closure. This avoids needing an independently chosen smooth mean-zero approximation.
```
theorem scalarH1_centered_poincare (d : ParallelMetricData g μ) {K : ℝ}
    (hP : SmoothScalarPoincare d K) (u : scalarH1 d) :
    ‖scalarH1Value d u - scalarH1Mean d u • scalarL2One g μ‖ ^ 2 ≤
      K * ∑ i : Fin 4, ‖scalarH1Gradient d i u‖ ^ 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.SmoothScalarPoincare, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.scalarH1Value, OAI.PositiveEinsteinFour.Geometry.scalarH1Mean, OAI.PositiveEinsteinFour.Geometry.scalarL2One, OAI.PositiveEinsteinFour.Geometry.scalarH1Gradient
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_poincare line 7592
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_norm_sq line 7598
def OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroValue line 7606
Source documentation
Restrict the scalar value map to the mean-zero Hilbert subspace.
```
def scalarMeanZeroValue (d : ParallelMetricData g μ) :
    scalarH1MeanZero d →L[ℝ] ScalarL2 g μ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1MeanZero, OAI.PositiveEinsteinFour.Geometry.ScalarL2
def OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroGradient line 7611
Source documentation
Restrict each of the four actual scalar derivatives to that subspace.
```
def scalarMeanZeroGradient (d : ParallelMetricData g μ) (i : Fin 4) :
    scalarH1MeanZero d →L[ℝ] ScalarL2 g μ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1MeanZero, OAI.PositiveEinsteinFour.Geometry.ScalarL2
def OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroDirichlet line 7616
Source documentation
The bounded Dirichlet bilinear form on the actual mean-zero space.
```
def scalarMeanZeroDirichlet (d : ParallelMetricData g μ) :
    scalarH1MeanZero d →L[ℝ] scalarH1MeanZero d →L[ℝ] ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1MeanZero
theorem OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroDirichlet_apply line 7621
theorem OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroDirichlet_self line 7628
theorem OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroDirichlet_coercive line 7636
Source documentation
The Poincaré estimate controls the full first-jet norm on the mean-zero subspace; the coercivity constant is exactly 1 / (K + 1).
```
theorem scalarMeanZeroDirichlet_coercive (d : ParallelMetricData g μ)
    {K : ℝ} (hK : 0 < K) (hP : SmoothScalarPoincare d K) :
    @IsCoercive (scalarH1MeanZero d) _ (scalarCoercive_meanZeroSpace d)
      (scalarMeanZeroDirichlet d) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.SmoothScalarPoincare, OAI.PositiveEinsteinFour.Geometry.scalarH1MeanZero, OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroDirichlet
def OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroWeakPoisson line 7656
Source documentation
The unique mean-zero weak solution, as a continuous operator on L². Its sign convention is the positive Dirichlet operator -Δ.
```
def scalarMeanZeroWeakPoisson (d : ParallelMetricData g μ) {K : ℝ}
    (hK : 0 < K) (hP : SmoothScalarPoincare d K) :
    ScalarL2 g μ →L[ℝ] scalarH1MeanZero d :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.SmoothScalarPoincare, OAI.PositiveEinsteinFour.Geometry.ScalarL2, OAI.PositiveEinsteinFour.Geometry.scalarH1MeanZero
theorem OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroWeakPoisson_weak line 7664
theorem OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroWeakPoisson_unique line 7675
theorem OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroWeakPoisson_existsUnique line 7687
def OAI.PositiveEinsteinFour.Geometry.positivePowerInner line 7712
def OAI.PositiveEinsteinFour.Geometry.positivePowerOuter line 7718
def OAI.PositiveEinsteinFour.Geometry.positivePowerExtension line 7724
theorem OAI.PositiveEinsteinFour.Geometry.positivePowerExtension_smooth line 7727
theorem OAI.PositiveEinsteinFour.Geometry.positivePowerExtension_compact line 7741
theorem OAI.PositiveEinsteinFour.Geometry.positivePowerExtension_eq line 7745
theorem OAI.PositiveEinsteinFour.Geometry.positivePowerExtension_deriv line 7761

theorem OAI.PositiveEinsteinFour.Geometry.scalar_positive_power_extension line 7784

Source documentation

The extension is smooth on all of R, vanishes at zero, and has bounded first derivative. On the positive interval it is exactly the desired power.

theorem scalar_positive_power_extension (a B q : ℝ) (ha : 0 < a) (hB : 0 ≤ B) :
    ∃ φ : ℝ → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧ φ 0 = 0 ∧
      (∃ D : ℝ≥0, ∀ t, |deriv φ t| ≤ D) ∧
      ∀ t ∈ Icc a B, φ t = t ^ q ∧ deriv φ t = q * t ^ (q - 1) := by
…

theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarDirichlet_laplacian_pairing line 7826
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_green line 7837
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Value_injective line 7858
Source documentation
The first-jet completion has no nonzero element with zero scalar value: Green's identity determines every derivative coordinate.
```
theorem scalarH1Value_injective (d : ParallelMetricData g μ) :
    Function.Injective (scalarH1Value d) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1Value
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_eq_smooth_of_value line 7867
def OAI.PositiveEinsteinFour.Geometry.scalarJetWeight line 7890
theorem OAI.PositiveEinsteinFour.Geometry.scalarJetWeight_ne_zero line 7894
def OAI.PositiveEinsteinFour.Geometry.scalarWeightEquiv line 7899
def OAI.PositiveEinsteinFour.Geometry.scalarWeightedJetEquiv line 7915
Source documentation
Invertible diagonal rescaling of the actual scalar first jet.
```
def scalarWeightedJetEquiv (g : SmoothMetric M) (μ : Measure (FrameBundle g)) :
    ScalarJetL2 g μ ≃L[ℝ] ScalarJetL2 g μ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.ScalarJetL2
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedJetEquiv_none line 7923
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedJetEquiv_some line 7929
def OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1 line 7933
Source documentation
The closed image of actual smooth first jets, with the Sobolev energy norm.
```
def scalarWeightedH1 (d : ParallelMetricData g μ) : Submodule ℝ (ScalarJetL2 g μ) :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.ScalarJetL2
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1_closed line 7936
instance OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1_complete line 7942
def OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1Equiv line 7947
Source documentation
The weighted energy space is continuously linearly equivalent to actual H¹.
```
def scalarWeightedH1Equiv (d : ParallelMetricData g μ) :
    scalarH1 d ≃L[ℝ] scalarWeightedH1 d :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1
def OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1ToH1 line 7952
Source documentation
Continuous recovery of the original first jet, including its value.
```
def scalarWeightedH1ToH1 (d : ParallelMetricData g μ) :
    scalarWeightedH1 d →L[ℝ] scalarH1 d :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1, OAI.PositiveEinsteinFour.Geometry.scalarH1
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1ToH1_equiv line 7956
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1_inner line 7961
Source documentation
The exact weighted inner product, on arbitrary completed scalar jets.
```
theorem scalarWeightedH1_inner (d : ParallelMetricData g μ) (u v : scalarH1 d) :
    inner ℝ (scalarWeightedH1Equiv d u) (scalarWeightedH1Equiv d v) =
      inner ℝ (scalarH1Value d u) (scalarH1Value d v) +
        (1 / 2 : ℝ) * ∑ i : Fin 4,
          inner ℝ (scalarH1Gradient d i u) (scalarH1Gradient d i v) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1Equiv, OAI.PositiveEinsteinFour.Geometry.scalarH1Value, OAI.PositiveEinsteinFour.Geometry.scalarH1Gradient
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1_norm_sq line 7980
def OAI.PositiveEinsteinFour.Geometry.smoothScalarToWeightedH1 line 7987
Source documentation
A smooth function, regarded as an element of the weighted Hilbert space.
```
def smoothScalarToWeightedH1 (d : ParallelMetricData g μ) :
    SmoothScalar (M := M) →ₗ[ℝ] scalarWeightedH1 d where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.SmoothScalar, OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1ToH1_smooth line 7999
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarToWeightedH1_dense line 8004
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarToWeightedH1_norm_sq line 8025
Source documentation
On smooth scalars the Hilbert norm is exactly the Sobolev quotient denominator.
```
theorem smoothScalarToWeightedH1_norm_sq (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) (a : SmoothScalar (M := M)) :
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.SmoothScalar
def OAI.PositiveEinsteinFour.Geometry.tensorTransportWeight line 8065
theorem OAI.PositiveEinsteinFour.Geometry.tensorTransportWeight_nonneg line 8068
theorem OAI.PositiveEinsteinFour.Geometry.tensorTransportWeight_continuous line 8072
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_abs_le_weight line 8080
theorem OAI.PositiveEinsteinFour.Geometry.tensor_component_sq_le line 8101
def OAI.PositiveEinsteinFour.Geometry.twoFormChartTransport line 8110
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartTransport_continuousOn line 8113
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoordinates_abs_le line 8125
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.gramCovariantCoordinates line 8147
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.covariantCoordinates_abs_le line 8161
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFramedValue_skew line 8219
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.framedCovariant_skew line 8224
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_cross_curvature line 8271
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormGreenLinear line 8352
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormGreenLinear_bound line 8366
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormGreenDual line 8383
def OAI.PositiveEinsteinFour.Geometry.twoFormGreenDual line 8389
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGreenDual_smooth line 8393
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1_inner_smooth line 8400
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormTensorLinear line 8438
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormTensorL2 line 8468
def OAI.PositiveEinsteinFour.Geometry.twoFormTensorL2 line 8473
theorem OAI.PositiveEinsteinFour.Geometry.twoFormTensorL2_smooth line 8477
theorem OAI.PositiveEinsteinFour.Geometry.twoFormTensorL2_norm_sq line 8481
theorem OAI.PositiveEinsteinFour.Geometry.twoFormTensorL2_inner line 8496
def OAI.PositiveEinsteinFour.Geometry.twoFormFromTensorL2 line 8503
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFromTensorL2_pairing line 8506
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFromTensorL2_left_inverse line 8512
def OAI.PositiveEinsteinFour.Geometry.weylGapEpsilon line 8533
theorem OAI.PositiveEinsteinFour.Geometry.weylGapEpsilon_pos line 8535
theorem OAI.PositiveEinsteinFour.Geometry.weylGapEpsilon_le_one line 8539
theorem OAI.PositiveEinsteinFour.Geometry.weylGapEpsilon_tendsto line 8543
theorem OAI.PositiveEinsteinFour.Geometry.integral_weyl_regularized_power_tendsto line 8550
theorem OAI.PositiveEinsteinFour.Geometry.radialCoordinateFlow_frame_endpoint_time line 8595
theorem OAI.PositiveEinsteinFour.Geometry.frameMomentumMap_apply line 8617
theorem OAI.PositiveEinsteinFour.Geometry.frameUnitRadialState_cotangent line 8642
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_rescaled_hasFDerivAt line 8655

theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_rescaled_normal_differential line 8694

Source documentation

Varying the initial unit velocity in a normal frame direction gives exactly the matrix Jacobi solution at time t.

theorem frameExponential_rescaled_normal_differential (g : SmoothMetric M)
    (o : FrameOrientation g) (hRic : RicciThree g) (d : M)
    (e : FrameBundle g) (he : e ∈ o.positive) (t : ℝ) (ht : 0 < t)
    (hd : (parallelFrameFlowMap g 0 t e).base ∈ (chartAt FourSpace d).source)
    (w : Fin 3 → ℝ) :
    (fun i : Fin 3 => ((frameChartMatrix g d (parallelFrameFlowMap g 0 t e))⁻¹ *ᵥ
      WithLp.ofLp (fderiv ℝ (fun v : FourSpace => chartAt FourSpace d
        (frameExponential g o e (t • v))) (coordinateVector 0)
          (WithLp.toLp 2 (Fin.cons 0 w)))) i.succ) =
      (actualJacobiSolution g hRic e).J t *ᵥ w := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix, OAI.PositiveEinsteinFour.Geometry.frameExponential, OAI.PositiveEinsteinFour.Geometry.actualJacobiSolution

theorem OAI.PositiveEinsteinFour.Geometry.actual_normalizedJacobi_continuous line 8741
theorem OAI.PositiveEinsteinFour.Geometry.exists_actualFirstConjugateTime line 8753
def OAI.PositiveEinsteinFour.Geometry.actualFirstConjugateTime line 8813
theorem OAI.PositiveEinsteinFour.Geometry.actualFirstConjugateTime_pos line 8817
theorem OAI.PositiveEinsteinFour.Geometry.actualFirstConjugateTime_le_pi line 8821
theorem OAI.PositiveEinsteinFour.Geometry.actualFirstConjugateTime_singular line 8825
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_isUnit_before_firstConjugate line 8830
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_preconjugate_iff_lt line 8836
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_det_pos_before_firstConjugate line 8848
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_full_variation line 8875
def OAI.PositiveEinsteinFour.Geometry.actualFullVariationPosition line 8902
def OAI.PositiveEinsteinFour.Geometry.actualFullVariationVelocity line 8907
theorem OAI.PositiveEinsteinFour.Geometry.actualFullVariationPosition_eq_chart line 8911
theorem OAI.PositiveEinsteinFour.Geometry.actualFullVariationPosition_eventually_chart line 8931
theorem OAI.PositiveEinsteinFour.Geometry.actualFullVariationPosition_hasDerivAt line 8944
theorem OAI.PositiveEinsteinFour.Geometry.actualFullVariationVelocity_eq_chart line 8956
theorem OAI.PositiveEinsteinFour.Geometry.actualFullVariationVelocity_hasDerivAt line 8966
def OAI.PositiveEinsteinFour.Geometry.frameFullInitialVariation line 8987
theorem OAI.PositiveEinsteinFour.Geometry.actualFullVariation_initial line 8993
theorem OAI.PositiveEinsteinFour.Geometry.actualFullVariation_eq_jacobi line 9030
def OAI.PositiveEinsteinFour.Geometry.oneFormDivergence line 9069
theorem OAI.PositiveEinsteinFour.Geometry.oneFormDivergence_eq_frame line 9072
theorem OAI.PositiveEinsteinFour.Geometry.oneFormDivergence_coordinates line 9078
theorem OAI.PositiveEinsteinFour.Geometry.oneFormDivergence_smooth line 9088
def OAI.PositiveEinsteinFour.Geometry.smoothOneFormDivergence line 9112
theorem OAI.PositiveEinsteinFour.Geometry.oneFormDivergence_differential line 9133
theorem OAI.PositiveEinsteinFour.Geometry.twoCovariantAlternation_pairing line 9156
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormExterior_framed_tensor line 9181
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneFormExterior_frame_pairing line 9191
theorem OAI.PositiveEinsteinFour.Geometry.smoothOneForm_direction_green line 9205
def OAI.PositiveEinsteinFour.Geometry.smoothScalarAbsRegularized line 9249
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarAbsRegularized_pos line 9259
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarAbsRegularized_sq line 9265
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarAbsRegularized_error line 9271
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarAbsRegularized_gradient line 9284
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarAbsRegularized_gradient_sq_le line 9316
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarAbsRegularized_dirichlet_le line 9339
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarAbsRegularized_energy_le line 9359
def OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValueFun line 9400
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValueFun_spec line 9405
def OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue line 9410
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue_spec line 9430
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue_eq line 9435
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue_smooth line 9442
def OAI.PositiveEinsteinFour.Geometry.scalarKatoTail line 9470
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoTail_memLp line 9472
theorem OAI.PositiveEinsteinFour.Geometry.scalarKatoTail_small line 9480
theorem OAI.PositiveEinsteinFour.Geometry.scalarLp_four_norm_sq line 9505
theorem OAI.PositiveEinsteinFour.Geometry.scalarKato_square_memLp line 9518

theorem OAI.PositiveEinsteinFour.Geometry.scalarKato_tail_pairing line 9528

Source documentation

The multiplication estimate used for the tail, in ordinary real integrals.

theorem scalarKato_tail_pairing {V W : X → ℝ} (hV : MemLp V 2 μ)
    (hW : MemLp W 4 μ) (n : ℕ) :
    (∫ x, scalarKatoTail V n x * W x ^ 2 ∂μ) ≤
      Real.sqrt (∫ x, scalarKatoTail V n x ^ 2 ∂μ) *
        Real.sqrt (∫ x, W x ^ 4 ∂μ) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarKatoTail

theorem OAI.PositiveEinsteinFour.Geometry.scalarKato_memLp_eight_of_energy line 9548

Source documentation

A fixed Sobolev estimate and the tested energy bound imply the eighth moment. The potential only needs its genuine L² integrability.

theorem scalarKato_memLp_eight_of_energy [IsFiniteMeasure μ] {f V : X → ℝ}
    (hf : MemLp f 4 μ) (hV : MemLp V 2 μ) {C : ℝ} (hC : 0 < C)
    (hW : ∀ lam : ℝ, 0 < lam → MemLp (fun x => scalarKatoSquare lam (f x)) 4 μ)
    (henergy : ∀ lam : ℝ, 0 < lam →
      Real.sqrt (∫ x, scalarKatoSquare lam (f x) ^ 4 ∂μ) ≤ C *
        ((∫ x, f x ^ 4 ∂μ) +
          4 * ∫ x, V x * scalarKatoSquare lam (f x) ^ 2 ∂μ)) :
    MemLp f 8 μ := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarKatoSquare

theorem OAI.PositiveEinsteinFour.Geometry.scalarWeakMinimum_inner line 9642
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_nonneg_of_negative_source line 9649
Source documentation
Strict negativity of the weak Laplacian wherever the scalar value is negative forces nonnegativity almost everywhere.
```
theorem scalarH1_nonneg_of_negative_source (d : ParallelMetricData g μ)
    (u : scalarH1 d) (F : ScalarL2 g μ)
    (heq : ∀ v : scalarH1 d,
      (∑ i : Fin 4, inner ℝ (scalarH1Gradient d i u) (scalarH1Gradient d i v)) =
        -(inner ℝ F (scalarH1Value d v)))
    (hneg : ∀ᵐ e ∂μ, scalarH1Value d u e < 0 → F e < 0) :
    ∀ᵐ e ∂μ, 0 ≤ scalarH1Value d u e := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.ScalarL2, OAI.PositiveEinsteinFour.Geometry.scalarH1Gradient, OAI.PositiveEinsteinFour.Geometry.scalarH1Value
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_sub_smooth_weak_equation line 9692
Source documentation
Subtracting a smooth barrier preserves the weak equation, with its actual geometric Laplacian subtracted from the source.
```
theorem scalarH1_sub_smooth_weak_equation (d : ParallelMetricData g μ)
    (u : scalarH1 d) (F : ScalarL2 g μ)
    (heq : ∀ v : scalarH1 d,
      (∑ i : Fin 4, inner ℝ (scalarH1Gradient d i u) (scalarH1Gradient d i v)) =
        -(inner ℝ F (scalarH1Value d v)))
    (b : SmoothScalar (M := M)) (ε : ℝ) (v : scalarH1 d) :
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.ScalarL2, OAI.PositiveEinsteinFour.Geometry.scalarH1Gradient, OAI.PositiveEinsteinFour.Geometry.scalarH1Value, OAI.PositiveEinsteinFour.Geometry.SmoothScalar
theorem OAI.PositiveEinsteinFour.Geometry.scalar_continuous_base_nonneg_of_frame_ae line 9717
Source documentation
A continuous base representative which is nonnegative almost everywhere on the canonical frames is nonnegative at every base point.
```
theorem scalar_continuous_base_nonneg_of_frame_ae (g : SmoothMetric M)
    (o : FrameOrientation g) (u : M → ℝ) (hu : Continuous u)
    (hae : ∀ᵐ e ∂canonicalFrameMeasure g o, 0 ≤ u e.base) : ∀ x, 0 ≤ u x := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure
theorem OAI.PositiveEinsteinFour.Geometry.covariantMetricTraceField_coordinates line 9751
theorem OAI.PositiveEinsteinFour.Geometry.CovariantFieldSmooth.metricTrace line 9764
def OAI.PositiveEinsteinFour.Geometry.smoothCovariantMetricTrace line 9781
def OAI.PositiveEinsteinFour.Geometry.tensorSlotWeight line 9802
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotWeight_nonneg line 9805
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotWeight_continuous line 9809
theorem OAI.PositiveEinsteinFour.Geometry.tensorSlotAction_abs_le_weight line 9818
def OAI.PositiveEinsteinFour.Geometry.twoFormChartConnectionWeight line 9845
def OAI.PositiveEinsteinFour.Geometry.twoFormChartControl line 9848
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartControl_nonneg line 9853
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartControl_continuousOn line 9862
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.coordinate_partial_control line 9881
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChart_compact_control line 9936
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_norm_le_tensor_sum line 9978
theorem OAI.PositiveEinsteinFour.Geometry.frameTensor_sum_abs_le line 9988
def OAI.PositiveEinsteinFour.Geometry.twoFormChartReverseControl line 10003
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartReverseControl_continuousOn line 10006
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_chart_reverse_value line 10016
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_chart_reverse_bound line 10029
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFromTensorL2_norm_le line 10065
def OAI.PositiveEinsteinFour.Geometry.twoFormFromContinuousTensor line 10084
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFromContinuousTensor_pairing line 10087
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFromContinuousTensor_smooth line 10104
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFromContinuousTensor_norm_le line 10111
theorem OAI.PositiveEinsteinFour.Geometry.integral_frame_sum_three line 10147
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDeRhamEnergy line 10160
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDeRhamEnergy_nonneg line 10164
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_derivative_product_integrable line 10168
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormDeRhamEnergy_cross line 10176
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1_eq_zero_of_value_eq_zero line 10234
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1ToL2_injective line 10246
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.framedSecond_skew line 10273
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.roughTrace_skew line 10296
theorem OAI.PositiveEinsteinFour.Geometry.weyl_gap_equality_constant line 10321
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_rescaled_full_differential line 10427
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_rescaled_fderiv line 10452
theorem OAI.PositiveEinsteinFour.Geometry.jacobiBlockMatrix_rescale line 10474
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_hasFDerivAt line 10483
Source documentation
The actual exponential differential at t e₀, written using the parallel frame at its endpoint.
```
theorem frameExponential_hasFDerivAt (g : SmoothMetric M)
    (o : FrameOrientation g) (hRic : RicciThree g) (d : M)
    (e : FrameBundle g) (he : e ∈ o.positive) (t : ℝ) (ht : 0 < t)
    (hd : (parallelFrameFlowMap g 0 t e).base ∈ (chartAt FourSpace d).source) :
    HasFDerivAt (fun v : FourSpace => chartAt FourSpace d (frameExponential g o e v))
      (Matrix.toEuclideanCLM (n := Fin 4) (𝕜 := ℝ) (frameChartMatrix g d (parallelFrameFlowMap g 0 t e) *
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap, OAI.PositiveEinsteinFour.Geometry.frameExponential, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_metric_jacobian line 10521
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_metric_jacobian_preconjugate line 10533
theorem OAI.PositiveEinsteinFour.Geometry.actualFirstConjugateTime_measurable line 10567
Source documentation
Measurability of the preconjugate set implies measurability of the first conjugate time.
```
theorem actualFirstConjugateTime_measurable (g : SmoothMetric M) (hRic : RicciThree g) :
    Measurable (actualFirstConjugateTime g hRic) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.actualFirstConjugateTime
def OAI.PositiveEinsteinFour.Geometry.actualNormalizedJacobiMatrix line 10579
theorem OAI.PositiveEinsteinFour.Geometry.actualNormalizedJacobiMatrix_zero line 10583
theorem OAI.PositiveEinsteinFour.Geometry.actualNormalizedJacobiMatrix_eq_average line 10589
theorem OAI.PositiveEinsteinFour.Geometry.actualNormalizedJacobiMatrix_continuous line 10614
theorem OAI.PositiveEinsteinFour.Geometry.actualNormalizedJacobiMatrix_isUnit_iff line 10630
theorem OAI.PositiveEinsteinFour.Geometry.actualFirstConjugateTime_lowerSemicontinuous line 10640
theorem OAI.PositiveEinsteinFour.Geometry.actual_preconjugate_radial_isOpen line 10679
Source documentation
Positive times strictly before the first conjugate time form an open subset of the actual radial parameter space.
```
theorem actual_preconjugate_radial_isOpen (g : SmoothMetric M) (hRic : RicciThree g) :
    IsOpen {p : ℝ × FrameBundle g |
      0 < p.1 ∧ p.1 < actualFirstConjugateTime g hRic p.2} := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.actualFirstConjugateTime
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.kernel_intersection_eq_zero line 10707
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.velocity_ne_zero_of_kernel line 10747
theorem OAI.PositiveEinsteinFour.Geometry.exists_actualJacobi_conjugate_vector line 10767
theorem OAI.PositiveEinsteinFour.Geometry.exists_actualFirstConjugate_vector line 10780

theorem OAI.PositiveEinsteinFour.Geometry.exists_actualConjugateNormalVariation line 10789

Source documentation

The conjugate vector is realized by the derivative of the geodesic flow.

theorem exists_actualConjugateNormalVariation (g : SmoothMetric M)
    (o : FrameOrientation g) (hRic : RicciThree g) (e : FrameBundle g)
    (he : e ∈ o.positive) (c : ℝ)
    (hc : ¬ IsUnit ((actualJacobiSolution g hRic e).J c)) :
    ∃ w : Fin 3 → ℝ, w ≠ 0 ∧
      actualNormalVariationPosition g o e (frameNormalInitialVariation g e w) 0 = 0 ∧
      actualNormalVariationVelocity g o e (frameNormalInitialVariation g e w) 0 = w ∧
      actualNormalVariationPosition g o e (frameNormalInitialVariation g e w) c = 0 ∧
      actualNormalVariationVelocity g o e (frameNormalInitialVariation g e w) c ≠ 0 := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.actualJacobiSolution, OAI.PositiveEinsteinFour.Geometry.actualNormalVariationPosition, OAI.PositiveEinsteinFour.Geometry.frameNormalInitialVariation, OAI.PositiveEinsteinFour.Geometry.actualNormalVariationVelocity

theorem OAI.PositiveEinsteinFour.Geometry.exists_actualFirstConjugateNormalVariation line 10803
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_det_firstConjugate_eq_zero line 10837
theorem OAI.PositiveEinsteinFour.Geometry.actualRegularJacobi_truncatedDensity_firstConjugate line 10844
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_cutoff_le_truncatedDensity line 10853
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_cutoff_le_truncatedIndicator line 10870
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_cutoff_lintegral_le line 10885
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_truncatedDensity_integrableOn line 10910
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_cutoff_lintegral_le_integral line 10928
theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.kinetic_eq line 10964
theorem OAI.PositiveEinsteinFour.Geometry.heatRadialCotangentState_frame line 10982
theorem OAI.PositiveEinsteinFour.Geometry.heatRadialFrameEndpoint_exponential line 10989
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_power_of_positive_range line 11051
theorem OAI.PositiveEinsteinFour.Geometry.scalar_positive_continuous_range line 11071
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_power_of_positive_continuous line 11083
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_barrier_comparison line 11127
def OAI.PositiveEinsteinFour.Geometry.twoFormTraceLinear line 11206
def OAI.PositiveEinsteinFour.Geometry.twoFormTraceExtract line 11211
def OAI.PositiveEinsteinFour.Geometry.twoFormRoughTraceField line 11217
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.secondGram_contDiffAt line 11220
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.framedSecond_chart line 11231
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.roughTraceField_frame line 11243
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.roughTrace line 11257
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormRoughTrace line 11272
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.framedValue_roughTrace line 11275
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_frame_inner_integrable line 11305
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_Weitzenbock line 11324
theorem OAI.PositiveEinsteinFour.Geometry.heatRadialCotangentState_contDiffAt line 11383
def OAI.PositiveEinsteinFour.Geometry.exponentialFamilyCoordinates line 11405
theorem OAI.PositiveEinsteinFour.Geometry.exponentialFamilyCoordinates_frame line 11409
theorem OAI.PositiveEinsteinFour.Geometry.exponentialFamilyCoordinates_contDiffAt line 11418
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_contMDiff line 11463
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_first_ray line 11481
theorem OAI.PositiveEinsteinFour.Geometry.normalized_frame_pairing line 11493

theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_chart_gauss line 11500

Source documentation

In output coordinates, the exponential differential has radial inner product exactly equal to the initial radial component.

theorem frameExponential_chart_gauss (g : SmoothMetric M) (o : FrameOrientation g)
    (hRic : RicciThree g) (d : M) (e : FrameBundle g) (he : e ∈ o.positive)
    (t : ℝ) (ht : 0 < t)
    (hd : (parallelFrameFlowMap g 0 t e).base ∈ (chartAt FourSpace d).source)
    (w : FourSpace) :
    (fun i => frameChartMatrix g d (parallelFrameFlowMap g 0 t e) i 0) ⬝ᵥ
      (metricInChart g d (chartAt FourSpace d (parallelFrameFlowMap g 0 t e).base) *ᵥ
        WithLp.ofLp (fderiv ℝ (fun v : FourSpace => chartAt FourSpace d
          (frameExponential g o e v)) (t • coordinateVector 0) w)) = w 0 := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.normal_conjugate_mul line 11539
theorem OAI.PositiveEinsteinFour.Jacobi.matrixJacobi_conjugate line 11545
theorem OAI.PositiveEinsteinFour.Jacobi.normal_conjugate_det line 11573
theorem OAI.PositiveEinsteinFour.Geometry.orthogonal_first_row line 11595
theorem OAI.PositiveEinsteinFour.Geometry.frameJacobi_normalRestriction line 11602
theorem OAI.PositiveEinsteinFour.Geometry.frameJacobi_rotate_normal line 11611
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_rotate_normal line 11629
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_det_rotate_normal line 11647
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_truncatedDensity_rotate_normal line 11656
theorem OAI.PositiveEinsteinFour.Geometry.frame_eq_of_matrix_eq line 11666
Distinct definitions of this name: OAI/Geometry/EinsteinFour/CurvatureTensors02.lean:11802 (different declaration text), OAI/Geometry/EinsteinFour/WeylEstimates03.lean:951 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.frame_eq_of_matrix_eq@path.
theorem OAI.PositiveEinsteinFour.Geometry.frame_rotate_change line 11677
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_truncatedDensity_directionInvariant line 11684
def OAI.PositiveEinsteinFour.Jacobi.normalIndexDensity line 11714
theorem OAI.PositiveEinsteinFour.Jacobi.normalIndexDensity_eq_euclidean line 11717
def OAI.PositiveEinsteinFour.Jacobi.mulVecRightLinear line 11722
theorem OAI.PositiveEinsteinFour.Jacobi.hasDerivAt_mulVec_right line 11726
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.field_position_hasDerivAt line 11731
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.field_velocity_hasDerivAt line 11736
theorem OAI.PositiveEinsteinFour.Jacobi.normalJacobi_pairing_hasDerivAt line 11742
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.index_integral_eq_boundary line 11758
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.index_integral_zero_of_kernel line 11779
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_index_integral_eq_boundary line 11799
theorem OAI.PositiveEinsteinFour.Geometry.exists_actualFirstConjugate_zero_index line 11811
theorem OAI.PositiveEinsteinFour.Geometry.unitGeodesic_common_chart line 11844
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_common_source line 11875
def OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.recenter line 11920
def OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.restrictTime line 11963
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatRadialNormalFrame_flow line 11982
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatRadialNormalFrame line 12023
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_roughTrace_green line 12055
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_roughTrace_green_left line 12071
theorem OAI.PositiveEinsteinFour.Geometry.chartBackwardOperator_center line 12101
theorem OAI.PositiveEinsteinFour.Geometry.metricInChart_center_pairing line 12107
theorem OAI.PositiveEinsteinFour.Geometry.metric_inner_abs_le line 12119
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_center_fderiv line 12126
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_gauss_first line 12141
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_radial_differential_first line 12164
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_preconjugate_isUnit line 12209
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_preconjugate_localChart line 12228
Source documentation
A local exponential chart centered at any positive preconjugate time.
```
theorem frameExponential_preconjugate_localChart (g : SmoothMetric M)
    (o : FrameOrientation g) (hRic : RicciThree g) (e : FrameBundle g)
    (he : e ∈ o.positive) (t : ℝ) (ht : 0 < t)
    (htc : t < actualFirstConjugateTime g hRic e) :
    ∃ C : OpenPartialHomeomorph FourSpace M,
      t • coordinateVector 0 ∈ C.source ∧ EqOn C (frameExponential g o e) C.source := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.actualFirstConjugateTime, OAI.PositiveEinsteinFour.Geometry.frameExponential
theorem OAI.PositiveEinsteinFour.Geometry.frameRotate_map line 12286
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentTurn_vector line 12295
Distinct definitions of this name: OAI/Geometry/EinsteinFour/WeylEstimates03.lean:22362 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.unitTangentTurn_vector@path.
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentTurn_base line 12298
theorem OAI.PositiveEinsteinFour.Geometry.frameRotate_base line 12301
theorem OAI.PositiveEinsteinFour.Geometry.orthogonalDirection_val line 12304
theorem OAI.PositiveEinsteinFour.Geometry.orientedDirection_val line 12308
theorem OAI.PositiveEinsteinFour.Geometry.unitTangentTurn_rotate line 12313
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_rotate line 12329
def OAI.PositiveEinsteinFour.Jacobi.normalIndexPairing line 12373
theorem OAI.PositiveEinsteinFour.Jacobi.normalIndexDensity_sub_smul line 12376
theorem OAI.PositiveEinsteinFour.Jacobi.normalIndexDensity_smul line 12390
theorem OAI.PositiveEinsteinFour.Jacobi.continuous_normalIndexDensity line 12396
theorem OAI.PositiveEinsteinFour.Jacobi.continuous_normalIndexPairing line 12401
theorem OAI.PositiveEinsteinFour.Jacobi.normalJacobi_mixed_pairing_hasDerivAt line 12407
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.index_pairing_integral line 12424
theorem OAI.PositiveEinsteinFour.Jacobi.index_integral_sub_smul line 12446
def OAI.PositiveEinsteinFour.Jacobi.indexEndpointBump line 12465
def OAI.PositiveEinsteinFour.Jacobi.indexEndpointBumpDerivative line 12468
theorem OAI.PositiveEinsteinFour.Jacobi.indexEndpointBump_hasDerivAt line 12471
theorem OAI.PositiveEinsteinFour.Jacobi.indexEndpointBump_continuous line 12483
theorem OAI.PositiveEinsteinFour.Jacobi.indexEndpointBumpDerivative_continuous line 12487
theorem OAI.PositiveEinsteinFour.Jacobi.indexEndpointBump_values line 12492
def OAI.PositiveEinsteinFour.Jacobi.conjugateIndexAction line 12500
Source documentation
The action on the two smooth pieces of the zero-extended conjugate field minus the explicit endpoint bump.
```
def conjugateIndexAction {R : ℝ → NormalMatrix} (d : MatrixJacobiSolution R)
    (w : Fin 3 → ℝ) (c b ε : ℝ) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.conjugateIndexAction_eq line 12508
theorem OAI.PositiveEinsteinFour.Jacobi.exists_positive_quadratic_negative line 12547
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.exists_negative_conjugate_index line 12560
def OAI.PositiveEinsteinFour.Jacobi.conjugateIndexVariation line 12579
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.conjugateIndexVariation_continuous line 12583
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.conjugateIndexVariation_endpoints line 12592
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.conjugateIndexVariation_left_derivative line 12600
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.conjugateIndexVariation_right_derivative line 12609
theorem OAI.PositiveEinsteinFour.Geometry.exists_actualFirstConjugate_negative_index line 12631
theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair_frame line 12661
theorem OAI.PositiveEinsteinFour.Geometry.normal_lift_dotProduct line 12667
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_normal_lift line 12672
theorem OAI.PositiveEinsteinFour.Geometry.frameChart_normal_curvature_vector line 12684

theorem OAI.PositiveEinsteinFour.Geometry.actual_coordinateIndexDensity_normal line 12701

Source documentation

Only the ordinary-to-covariant derivative relation is needed in addition to the actual frame and curvature.

theorem actual_coordinateIndexDensity_normal (g : SmoothMetric M) (c : M)
    (e : FrameBundle g) (he : e.base ∈ (chartAt FourSpace c).source)
    (a b : Fin 3 → ℝ) (w : JacobiCoordinateVector)
    (hw : w + jacobiConnection
        (fun i => connectionMatrix g c i (chartAt FourSpace c e.base))
        (fun i => frameChartMatrix g c e i 0) *ᵥ
          (frameChartMatrix g c e *ᵥ Fin.cons 0 a) =
      frameChartMatrix g c e *ᵥ Fin.cons 0 b) :
    coordinateIndexDensity (metricInChart g c (chartAt FourSpace c e.base))
        (fun i => connectionMatrix g c i (chartAt FourSpace c e.base))
        (fun i j => matrixPartial (connectionMatrix g c j) i (chartAt FourSpace c e.base))
        (fun i => frameChartMatrix g c e i 0) (frameChartMatrix g c e *ᵥ Fin.cons 0 a) w =
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.jacobiConnection, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix, OAI.PositiveEinsteinFour.Geometry.coordinateIndexDensity, OAI.PositiveEinsteinFour.Geometry.matrixPartial

theorem OAI.PositiveEinsteinFour.Geometry.actual_parallel_normal_index line 12723

Source documentation

Parallel-frame differentiation supplies the preceding derivative relation from ordinary derivatives of the actual field.

theorem actual_parallel_normal_index (g : SmoothMetric M) (c : M)
    (e : ℝ → FrameBundle g) (a : ℝ → Fin 3 → ℝ) (b : Fin 3 → ℝ)
    (w : JacobiCoordinateVector) (t : ℝ)
    (he : (e t).base ∈ (chartAt FourSpace c).source)
    (hE : ∀ i j, HasDerivAt (fun s => frameChartMatrix g c (e s) i j)
      (-(jacobiConnection
        (fun k => connectionMatrix g c k (chartAt FourSpace c (e t).base))
        (fun k => frameChartMatrix g c (e t) k 0) * frameChartMatrix g c (e t)) i j) t)
    (ha : HasDerivAt a b t)
    (hY : HasDerivAt (fun s => frameChartMatrix g c (e s) *ᵥ Fin.cons 0 (a s)) w t) :
    coordinateIndexDensity (metricInChart g c (chartAt FourSpace c (e t).base))
        (fun i => connectionMatrix g c i (chartAt FourSpace c (e t).base))
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix, OAI.PositiveEinsteinFour.Geometry.jacobiConnection, OAI.PositiveEinsteinFour.Geometry.connectionMatrix, OAI.PositiveEinsteinFour.Geometry.coordinateIndexDensity

theorem OAI.PositiveEinsteinFour.Geometry.KineticLocalFlow.common_exponential_endpoint line 12764
def OAI.PositiveEinsteinFour.Geometry.heatRadialDirectionScale line 12853
theorem OAI.PositiveEinsteinFour.Geometry.heatRadialFrameField_scale line 12859
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_heatRadialDirectionScale line 12885
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatRadialNormalFamily line 12927
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_rotate_mfderiv line 13004
theorem OAI.PositiveEinsteinFour.Geometry.directionRotation_first line 13027
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_gauss line 13037
Source documentation
Gauss' lemma for every unit radial direction, derived from the actual Jacobi differential and the proved orthogonal change of initial frame.
```
theorem frameExponential_gauss (g : SmoothMetric M) (o : FrameOrientation g)
    (hRic : RicciThree g) (e : FrameBundle g) (he : e ∈ o.positive)
    (q : Directions) (t : ℝ) (ht : 0 < t) (w : FourSpace) :
    g.inner (frameExponential g o e (t • q.val))
      (mfderiv I4 I4 (frameExponential g o e) (t • q.val) q.val)
      (mfderiv I4 I4 (frameExponential g o e) (t • q.val) w) = ⟪q.val, w⟫_ℝ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameExponential
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_radial_norm line 13081
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_radial_pairing_le line 13089
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_chart_local_inverse_contMDiffAt line 13121
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_local_inverse_contMDiffAt line 13157
theorem OAI.PositiveEinsteinFour.Geometry.exists_exponential_log_first_variation line 13183
def OAI.PositiveEinsteinFour.Jacobi.conjugateLeftField line 13256
def OAI.PositiveEinsteinFour.Jacobi.conjugateLeftRate line 13260
def OAI.PositiveEinsteinFour.Jacobi.conjugateRightField line 13264
def OAI.PositiveEinsteinFour.Jacobi.conjugateRightRate line 13268
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateLeftField_hasDerivAt line 13272
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateRightField_hasDerivAt line 13278
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateLeftRate_continuous line 13283
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateRightRate_continuous line 13290
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateLeftField_continuous line 13295
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateRightField_continuous line 13301
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateLeftField_contDiff line 13307
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateRightField_contDiff line 13317
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateBranches_agree line 13327
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateBranches_endpoints line 13333
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateLeftField_eq_variation line 13338
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateRightField_eq_variation line 13343
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateBranches_integrals line 13352
theorem OAI.PositiveEinsteinFour.Jacobi.conjugateBranches_index_integrable line 13360
def OAI.PositiveEinsteinFour.Geometry.normalChartField line 13395
def OAI.PositiveEinsteinFour.Geometry.normalChartFrameRate line 13399
def OAI.PositiveEinsteinFour.Geometry.normalChartFieldRate line 13404
theorem OAI.PositiveEinsteinFour.Geometry.normalChartFrame_hasDerivAt line 13409
theorem OAI.PositiveEinsteinFour.Geometry.normalChartFieldRate_eq line 13419
theorem OAI.PositiveEinsteinFour.Geometry.normalChartField_hasDerivAt line 13432
theorem OAI.PositiveEinsteinFour.Geometry.normalChartField_toLp_hasDerivAt line 13449
theorem OAI.PositiveEinsteinFour.Geometry.normalChartField_change line 13459
theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_normal_lift line 13469
theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_matrixVector line 13478
theorem OAI.PositiveEinsteinFour.Geometry.normalChartFrame_continuousOn line 13488
theorem OAI.PositiveEinsteinFour.Geometry.normalChartFrameRate_continuousOn line 13495
theorem OAI.PositiveEinsteinFour.Geometry.normalChartField_continuousOn line 13513
theorem OAI.PositiveEinsteinFour.Geometry.normalChartFieldRate_continuousOn line 13520
theorem OAI.PositiveEinsteinFour.Geometry.normalChartField_index line 13532
Source documentation
The actual coordinate index is the matrix index for every prescribed normal value and normal derivative; the ordinary derivative is constructed.
```
theorem normalChartField_index (g : SmoothMetric M) (c : M) (e : FrameBundle g)
    (a b : ℝ → Fin 3 → ℝ) (t : ℝ)
    (hc : (parallelFrameFlowMap g 0 t e).base ∈ (chartAt FourSpace c).source) :
    chartEnergyIndexDensity g c (chartAt FourSpace c (parallelFrameFlowMap g 0 t e).base)
      (fun i => frameChartMatrix g c (parallelFrameFlowMap g 0 t e) i 0)
      (normalChartField g c e a t) (normalChartFieldRate g c e a b t) =
    normalIndexDensity (1 + frameCurvatureField g (parallelFrameFlowMap g 0 t e)) (a t) (b t) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap, OAI.PositiveEinsteinFour.Geometry.chartEnergyIndexDensity, OAI.PositiveEinsteinFour.Geometry.frameChartMatrix, OAI.PositiveEinsteinFour.Geometry.normalChartField, OAI.PositiveEinsteinFour.Geometry.normalChartFieldRate, OAI.PositiveEinsteinFour.Geometry.frameCurvatureField
theorem OAI.PositiveEinsteinFour.Geometry.normalChartField_index_continuousOn line 13543
theorem OAI.PositiveEinsteinFour.Geometry.normalChartField_index_intervalIntegrable line 13564
theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.kinetic_eq_from line 13597
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatRadialFrameCommonDomain line 13612
theorem OAI.PositiveEinsteinFour.Geometry.HeatRadialFrameFlow.scaling_eventually line 13694
theorem OAI.PositiveEinsteinFour.Geometry.heatRadialFrameEndpoint_radial_derivative line 13735
theorem OAI.PositiveEinsteinFour.Geometry.metric_curve_speed_continuous line 13808
theorem OAI.PositiveEinsteinFour.Geometry.actual_normal_curvature_positive line 13843
theorem OAI.PositiveEinsteinFour.Geometry.parallel_normal_index_negative line 13875
theorem OAI.PositiveEinsteinFour.Geometry.frameChart_center_inner line 13912
theorem OAI.PositiveEinsteinFour.Geometry.exists_exponential_log_center line 13931
def OAI.PositiveEinsteinFour.Geometry.framePolarDomain line 13970
theorem OAI.PositiveEinsteinFour.Geometry.framePolarDomain_isOpen line 13975
theorem OAI.PositiveEinsteinFour.Geometry.framePolarDomain_time_le_pi line 13985
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_polar_localChart line 13990
def OAI.PositiveEinsteinFour.Geometry.smoothRadialNorm line 14037
theorem OAI.PositiveEinsteinFour.Geometry.smoothRadialNorm_pos line 14039
theorem OAI.PositiveEinsteinFour.Geometry.smoothRadialNorm_bounds line 14044
theorem OAI.PositiveEinsteinFour.Geometry.smoothRadialNorm_hasFDerivAt line 14051
theorem OAI.PositiveEinsteinFour.Geometry.smoothRadialNorm_exponential_bound line 14073
def OAI.PositiveEinsteinFour.Geometry.geodesicChartVelocity line 14128
theorem OAI.PositiveEinsteinFour.Geometry.geodesicChartVelocity_hasDerivAt line 14132
theorem OAI.PositiveEinsteinFour.Geometry.geodesicChartPosition_hasDerivAt line 14147
theorem OAI.PositiveEinsteinFour.Geometry.geodesicChart_derivatives line 14154
theorem OAI.PositiveEinsteinFour.Geometry.geodesicChartPosition_continuousOn line 14165
theorem OAI.PositiveEinsteinFour.Geometry.geodesicChartVelocity_continuousOn line 14171
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalFrame_transport line 14198
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_curve_derivative line 14261
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_radial_displacement_le_length line 14273
theorem OAI.PositiveEinsteinFour.Geometry.normalChartField_second_integral line 14340
def OAI.PositiveEinsteinFour.Geometry.heatNormalFrameConnection line 14410
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalFrameConnection_radial line 14416
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalFrame_radial_connection line 14467