GeodesicGeometry05.lean`

367 declarations, 0 contain sorry, 0 declared as axioms

The radial length bound for lifts defined only on a compact interval. Endpoint differentiability is unnecessary.

theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_radial_interval_le line 45
theorem OAI.PositiveEinsteinFour.Geometry.heatMatrixDeterminant_contDiffAt line 99
theorem OAI.PositiveEinsteinFour.Geometry.heatMatrixInverse_contDiffAt line 107
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_normal_ball line 145
theorem OAI.PositiveEinsteinFour.Geometry.heatCompatibleMetric_inverse line 215
theorem OAI.PositiveEinsteinFour.Geometry.heatCompatibleMetric_density line 251
def OAI.PositiveEinsteinFour.Geometry.heatFamilyPartial line 305
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyPartial_slice line 309
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyPartial_contDiffAt line 323
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyMatrixDeterminant_contDiffAt line 329
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyMatrixInverse_contDiffAt line 338
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalFrameConnection_contDiffAt line 376
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_radial_le_lintegral line 437
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_inverse_path_length line 489
def OAI.PositiveEinsteinFour.Geometry.heatFamilyConnection line 564
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyConnection_slice line 571
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyConnection_contDiffAt line 579
def OAI.PositiveEinsteinFour.Geometry.heatFamilyBaseAugment line 630
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyBaseAugment_local_inverse line 633
def OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarPartial line 706
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarPartial_contDiffAt line 709
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarPartial_slice line 715
structure OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData line 747
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalFrameData line 765
theorem OAI.PositiveEinsteinFour.Geometry.heat_normal_inverse_four line 810
theorem OAI.PositiveEinsteinFour.Geometry.exists_heat_normal_chart_four line 845
theorem OAI.PositiveEinsteinFour.Geometry.exponentialFamily_local_inverse line 906
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_short_path_stays line 982
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_normal_ball_distance_lower line 1029
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_locally_minimizing line 1062
Source documentation
The constructed radial geodesics minimize distance near their initial point.
```
theorem frameExponential_locally_minimizing (g : SmoothMetric M)
    (o : FrameOrientation g) (hRic : RicciThree g) (e : FrameBundle g)
    (he : e ∈ o.positive) :
    ∃ r > (0 : ℝ), ∀ v : FourSpace, ‖v‖ < r →
      metricEDistance g e.base (frameExponential g o e v) = ENNReal.ofReal ‖v‖ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.metricEDistance, OAI.PositiveEinsteinFour.Geometry.frameExponential

theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_metric_ball_surj line 1075

Source documentation

The metric ball is covered by the actual radial normal coordinates.

theorem frameExponential_metric_ball_surj (g : SmoothMetric M)
    (o : FrameOrientation g) (hRic : RicciThree g) (e : FrameBundle g)
    (he : e ∈ o.positive) (C : OpenPartialHomeomorph FourSpace M)
    (hC : EqOn C (frameExponential g o e) C.source)
    (hI : ContMDiffOn I4 I4 1 C.symm C.target) (r : ℝ) (hr : 0 < r)
    (hball : closedBall 0 r ⊆ C.source) (y : M)
    (hy : metricEDistance g e.base y < ENNReal.ofReal r) :
    ∃ v : FourSpace, ‖v‖ < r ∧ frameExponential g o e v = y ∧
      metricEDistance g e.base y = ENNReal.ofReal ‖v‖ := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameExponential, OAI.PositiveEinsteinFour.Geometry.metricEDistance

theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyBaseAugment_actual_inverse line 1129
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyBaseAugment_common_injectivity line 1151
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyFrameData line 1192
theorem OAI.PositiveEinsteinFour.Geometry.heatLinearForm_coordinate_expansion line 1267
theorem OAI.PositiveEinsteinFour.Geometry.heatFrame_matrixPartial line 1275
theorem OAI.PositiveEinsteinFour.Geometry.heatFrame_metricPartial line 1289
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalFrameChart line 1332
def OAI.PositiveEinsteinFour.Geometry.heatNormalScalarLift line 1389
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalScalarLift_on_target line 1394
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalScalarLift_source line 1399
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalScalarLift_support line 1404
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalScalarLift_compact line 1413
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalScalarLift_regular line 1423
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_common_injective_neighborhood line 1461
def OAI.PositiveEinsteinFour.Geometry.heatFamilySliceChart line 1549
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilySliceChart_source line 1594
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilySliceChart_inverse_regular line 1600
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilySliceChart_uniform line 1611
theorem OAI.PositiveEinsteinFour.Geometry.heat_frameTensor_weighted_sum line 1653
theorem OAI.PositiveEinsteinFour.Geometry.heat_covariantDirection_pullback line 1662
theorem OAI.PositiveEinsteinFour.Geometry.heatFrame_baseJacobian line 1693
def OAI.PositiveEinsteinFour.Geometry.heatNormalCoordinateTensor line 1724
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalFrame_matrix_nondegenerate line 1729
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCoordinateTensor_regular line 1737
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCoordinateTensor_support line 1756
def OAI.PositiveEinsteinFour.Geometry.heatNormalChartBump line 1786
def OAI.PositiveEinsteinFour.Geometry.heatNormalCutoff line 1794
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalChartBump_support line 1797
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoff_regular line 1803
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoff_compact line 1811
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoff_inner line 1817
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCutoff_bounds line 1827
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalFrameCommonData line 1857
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalFrameConnection_skew line 1961
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.connection_skew line 2006
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.connection_as_twoForm line 2015
def OAI.PositiveEinsteinFour.Geometry.heatNormalFrameTensorLift line 2042
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalFrameTensorLift_support line 2049
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalFrameTensorLift_continuous line 2065
def OAI.PositiveEinsteinFour.Geometry.heatNormalOneFrameLift line 2125
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneFrameLift_support line 2132
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneFrameLift_continuous line 2148
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalScalarLift_continuous line 2207
theorem OAI.PositiveEinsteinFour.Geometry.metricEDistance_continuous line 2248
theorem OAI.PositiveEinsteinFour.Geometry.metricEDistance_ne_top line 2256
theorem OAI.PositiveEinsteinFour.Geometry.metricEDistance_toReal_continuous line 2272
theorem OAI.PositiveEinsteinFour.Geometry.metricEDistance_uniform_bound line 2281
def OAI.PositiveEinsteinFour.Geometry.frameMinimizingTimes line 2312
theorem OAI.PositiveEinsteinFour.Geometry.frameMinimizingTimes_zero line 2315
theorem OAI.PositiveEinsteinFour.Geometry.frameMinimizingTimes_closed line 2322
theorem OAI.PositiveEinsteinFour.Geometry.frameMinimizingTimes_downward line 2328
theorem OAI.PositiveEinsteinFour.Geometry.frameMinimizingTimes_has_positive line 2353
theorem OAI.PositiveEinsteinFour.Geometry.frameMinimizingTimes_bddAbove line 2369
def OAI.PositiveEinsteinFour.Geometry.actualCutTime line 2375
theorem OAI.PositiveEinsteinFour.Geometry.actualCutTime_mem line 2378
theorem OAI.PositiveEinsteinFour.Geometry.actualCutTime_pos line 2383
theorem OAI.PositiveEinsteinFour.Geometry.frameMinimizingTimes_eq_Icc line 2389
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_joint_continuous line 2414
theorem OAI.PositiveEinsteinFour.Geometry.heat_connection_trace_expand line 2487
theorem OAI.PositiveEinsteinFour.Geometry.heat_framed_second_covariant line 2506
theorem OAI.PositiveEinsteinFour.Geometry.heat_framed_twoFormSecondTrace line 2526
theorem OAI.PositiveEinsteinFour.Geometry.heat_covariant_congr line 2567
theorem OAI.PositiveEinsteinFour.Geometry.heat_covariant_weighted_sum line 2580
theorem OAI.PositiveEinsteinFour.Geometry.heatFamily_manifold_chart line 2626
theorem OAI.PositiveEinsteinFour.Geometry.heatJacobian_entry_regular line 2706
theorem OAI.PositiveEinsteinFour.Geometry.heatJacobian_partial line 2713
theorem OAI.PositiveEinsteinFour.Geometry.heatJacobian_partials_commute line 2724
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCoordinateTensor_continuousOn line 2753
def OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeTensor line 2764
def OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeL2 line 2777
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeL2_pairing line 2784
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCoordinateTensor_joint_continuous line 2816
theorem OAI.PositiveEinsteinFour.Geometry.heatNormal_covariant_pullback line 2863
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalFrameTensorLift_joint_continuous line 2911
def OAI.PositiveEinsteinFour.Geometry.heatNormalOneCoordinates line 2987
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCoordinates_regular line 2992
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCoordinates_support line 3009
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneFrameLift_joint_continuous line 3042
theorem OAI.PositiveEinsteinFour.Geometry.heatTwoFormSkewAction_swap line 3114
def OAI.PositiveEinsteinFour.Geometry.heatConnectionActionLinear line 3119
theorem OAI.PositiveEinsteinFour.Geometry.heatConnectionActionLinear_apply line 3122
def OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnectionMatrix line 3126
theorem OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnectionMatrix_action line 3129
theorem OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnectionMatrix_skew line 3137
def OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnection line 3148
theorem OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnection_radial line 3153
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.twoForm_connection_radial line 3167
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.twoForm_connection_regular line 3173
theorem OAI.PositiveEinsteinFour.Geometry.metric_path_crosses_sphere line 3210
theorem OAI.PositiveEinsteinFour.Geometry.exists_metricDistance_split line 3229
theorem OAI.PositiveEinsteinFour.Geometry.actualCutTime_upperSemicontinuous line 3293
theorem OAI.PositiveEinsteinFour.Geometry.actualCutTime_measurable line 3325
def OAI.PositiveEinsteinFour.Geometry.actualMinimizingRadialDomain line 3328
theorem OAI.PositiveEinsteinFour.Geometry.actualMinimizingRadialDomain_measurable line 3331
theorem OAI.PositiveEinsteinFour.Geometry.mem_actualMinimizingRadialDomain_iff line 3336
theorem OAI.PositiveEinsteinFour.Geometry.exists_joint_exponential_log line 3358
theorem OAI.PositiveEinsteinFour.Geometry.heat_covariant_second_pullback line 3484
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCoordinateTensor_add line 3546
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalFrameTensorLift_add line 3556
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeL2_add line 3568
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeL2_continuous_family line 3615
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalCommonChart line 3658
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneCoordinates_joint_continuous line 3726
def OAI.PositiveEinsteinFour.Geometry.heatNormalFrameCurvature line 3770
def OAI.PositiveEinsteinFour.Geometry.heatNormalPotential line 3774
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalFrameCurvature_contDiffAt line 3778
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalPotential_contDiffAt line 3796
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.curvature_regular line 3809
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.potential_regular line 3816
theorem OAI.PositiveEinsteinFour.Geometry.heat_extract_twoFormTensor line 3841
def OAI.PositiveEinsteinFour.Geometry.heatNormalTwoFormValue line 3849
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalTwoFormValue_tensor line 3854
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalTwoFormValue_contDiffAt line 3868
def OAI.PositiveEinsteinFour.Geometry.heatWeightedConnection line 3908
theorem OAI.PositiveEinsteinFour.Geometry.heatWeightedConnection_partial line 3912
theorem OAI.PositiveEinsteinFour.Geometry.heatWeightedConnection_curvature line 3941
theorem OAI.PositiveEinsteinFour.Geometry.heatWeightedConnection_actual_curvature line 3961
def OAI.PositiveEinsteinFour.Geometry.metricDistance line 3997
theorem OAI.PositiveEinsteinFour.Geometry.metricDistance_nonneg line 4000
theorem OAI.PositiveEinsteinFour.Geometry.ofReal_metricDistance line 4003
theorem OAI.PositiveEinsteinFour.Geometry.metricDistance_eq_iff line 4007
theorem OAI.PositiveEinsteinFour.Geometry.metricDistance_triangle line 4016
theorem OAI.PositiveEinsteinFour.Geometry.metricDistance_continuous line 4025
theorem OAI.PositiveEinsteinFour.Geometry.metricDistance_eq_zero_iff line 4029
theorem OAI.PositiveEinsteinFour.Geometry.exists_metricDistance_real_split line 4041
def OAI.PositiveEinsteinFour.Geometry.oneFormSecondTrace line 4066
theorem OAI.PositiveEinsteinFour.Geometry.oneFormSecondTrace_frame line 4069
theorem OAI.PositiveEinsteinFour.Geometry.heat_framed_oneFormSecondTrace line 4105
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_image_closedBall line 4149
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_image_sphere line 4170
theorem OAI.PositiveEinsteinFour.Geometry.exists_frameExponential_normal_ball_images line 4196
def OAI.PositiveEinsteinFour.Geometry.heatFamilyCurvature line 4233
def OAI.PositiveEinsteinFour.Geometry.heatFamilyPotential line 4237
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyCurvature_contDiffAt line 4241
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyPotential_contDiffAt line 4259
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyPotential_slice line 4270
def OAI.PositiveEinsteinFour.Geometry.heatFamilyTwoFormConnection line 4275
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyTwoFormConnection_contDiffAt line 4280
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyTwoFormConnection_slice line 4298
theorem OAI.PositiveEinsteinFour.Geometry.heat_matrixPartial_comm_two line 4323
theorem OAI.PositiveEinsteinFour.Geometry.heat_connection_law_derivative line 4339
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.connection_law line 4368
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.connection_curvature_intertwining line 4385
theorem OAI.PositiveEinsteinFour.Geometry.frameChartCurvature_eq line 4448
def OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.frame line 4467
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.frame_base_of_mem_source line 4472
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.curvature_as_actual line 4481
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.potential_as_actual line 4498
theorem OAI.PositiveEinsteinFour.Geometry.heatNormal_covariant_second_pullback line 4525
def OAI.PositiveEinsteinFour.Geometry.heatNormalTwoFormNabla line 4602
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalTwoFormNabla_tensor line 4609
def OAI.PositiveEinsteinFour.Geometry.metricIntervalSpeed line 4661
def OAI.PositiveEinsteinFour.Geometry.metricCurveEnergy line 4664
theorem OAI.PositiveEinsteinFour.Geometry.metricIntervalSpeed_continuousOn line 4667
theorem OAI.PositiveEinsteinFour.Geometry.metricIntervalSpeed_nonneg line 4688
theorem OAI.PositiveEinsteinFour.Geometry.metric_pathELength_eq_ofReal_integral line 4693

theorem OAI.PositiveEinsteinFour.Geometry.integral_speed_le_energy_add line 4710

Source documentation

Pointwise completion of the square, integrated on a compact interval.

theorem integral_speed_le_energy_add (s : ℝ → ℝ) {a b : ℝ} (hab : a ≤ b)
    (hs : ContinuousOn s (Icc a b)) :
    (∫ t in a..b, s t) ≤ (∫ t in a..b, (1 / 2 : ℝ) * (s t) ^ 2) + (b - a) / 2 := by
…

theorem OAI.PositiveEinsteinFour.Geometry.metricDistance_le_curveEnergy_add line 4727
Source documentation
A curve segment joining two points costs at least their distance minus half its parameter duration, in the actual Riemannian kinetic energy.
```
theorem metricDistance_le_curveEnergy_add (g : SmoothMetric M) (γ : ℝ → M)
    {a b : ℝ} (hab : a < b) (hγ : ContMDiffOn 𝓘(ℝ, ℝ) I4 1 γ (Icc a b)) :
    metricDistance g (γ a) (γ b) ≤ metricCurveEnergy g γ a b + (b - a) / 2 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.metricDistance, OAI.PositiveEinsteinFour.Geometry.metricCurveEnergy
theorem OAI.PositiveEinsteinFour.Geometry.metricDistance_le_sum_chain line 4745
Source documentation
The triangle inequality along a finite chain of actual points.
```
theorem metricDistance_le_sum_chain (g : SmoothMetric M) (p : ℕ → M) (n : ℕ) :
    metricDistance g (p 0) (p n) ≤
      ∑ i ∈ Finset.range n, metricDistance g (p i) (p (i + 1)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.metricDistance

theorem OAI.PositiveEinsteinFour.Geometry.finite_piece_metric_energy_lower line 4759

Source documentation

A finite piecewise C1 competitor with matching endpoints satisfies the same energy bound. There is no regularity requirement at its corners.

theorem finite_piece_metric_energy_lower (g : SmoothMetric M) (n : ℕ)
    (p : ℕ → M) (t : ℕ → ℝ) (γ : ℕ → ℝ → M)
    (ht : ∀ i < n, t i < t (i + 1))
    (hγ : ∀ i < n, ContMDiffOn 𝓘(ℝ, ℝ) I4 1 (γ i) (Icc (t i) (t (i + 1))))
    (hleft : ∀ i < n, γ i (t i) = p i)
    (hright : ∀ i < n, γ i (t (i + 1)) = p (i + 1)) :
    metricDistance g (p 0) (p n) - (t n - t 0) / 2 ≤
      ∑ i ∈ Finset.range n, metricCurveEnergy g (γ i) (t i) (t (i + 1)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.metricDistance, OAI.PositiveEinsteinFour.Geometry.metricCurveEnergy

theorem OAI.PositiveEinsteinFour.Geometry.metricDistance_le_of_speed_bound line 4794
theorem OAI.PositiveEinsteinFour.Geometry.exists_sharp_linear_chart_neighborhood line 4833
theorem OAI.PositiveEinsteinFour.Geometry.chart_curve_contMDiffOn line 4907
theorem OAI.PositiveEinsteinFour.Geometry.chart_curve_derivativeWithin line 4913
theorem OAI.PositiveEinsteinFour.Geometry.chart_curve_energy_density line 4932
theorem OAI.PositiveEinsteinFour.Geometry.metricCurveEnergy_chart line 4950
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_metric_differential_zero line 4984
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_metric_differential_continuous line 5010
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_differential_norm_near line 5029
theorem OAI.PositiveEinsteinFour.Geometry.metricCurveEnergy_congr line 5106
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_intervalSpeed line 5120
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_energy line 5135

theorem OAI.PositiveEinsteinFour.Geometry.geodesic_piece_energy_isLocalMin line 5151

Source documentation

The path distance and unit speed of the reference curve imply energy minimality.

theorem geodesic_piece_energy_isLocalMin (g : SmoothMetric M) (k : Fin 4)
    (e : FrameBundle g) (n : ℕ) (t : ℕ → ℝ)
    (γ : ℕ → ℝ → ℝ → M) (p : ℝ → ℕ → M)
    (ht : ∀ i < n, t i < t (i + 1))
    (hγ : ∀ᶠ ε in 𝓝 (0 : ℝ), ∀ i < n,
      ContMDiffOn 𝓘(ℝ, ℝ) I4 1 (γ i ε) (Icc (t i) (t (i + 1))))
    (hleft : ∀ᶠ ε in 𝓝 (0 : ℝ), ∀ i < n, γ i ε (t i) = p ε i)
    (hright : ∀ᶠ ε in 𝓝 (0 : ℝ), ∀ i < n, γ i ε (t (i + 1)) = p ε (i + 1))
    (hends : ∀ᶠ ε in 𝓝 (0 : ℝ),
      p ε 0 = frameGeodesic g k e (t 0) ∧ p ε n = frameGeodesic g k e (t n))
    (href : ∀ i < n, EqOn (γ i 0) (frameGeodesic g k e) (Icc (t i) (t (i + 1))))
    (hmin : metricDistance g (frameGeodesic g k e (t 0))
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameGeodesic, OAI.PositiveEinsteinFour.Geometry.metricDistance

theorem OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnection_contDiffAt line 5203
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalTwoFormNabla_contDiffAt line 5220
theorem OAI.PositiveEinsteinFour.Geometry.heatNormal_oneForm_rough_pullback line 5266
theorem OAI.PositiveEinsteinFour.Geometry.heatNormal_rough_pullback line 5351
theorem OAI.PositiveEinsteinFour.Geometry.metricDistance_le_of_interior_speed_bound line 5431
theorem OAI.PositiveEinsteinFour.Geometry.metricCurveEnergy_nonneg line 5488
theorem OAI.PositiveEinsteinFour.Geometry.metricDistance_point_le_curveEnergy_add line 5492
theorem OAI.PositiveEinsteinFour.Geometry.finite_piece_metric_energy_point_bound line 5510

theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition_inside_on line 5558

Source documentation

Extend the two time fields only for the compactness argument. The resulting variation and its jets on the original segment are unchanged.

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

Mentions: OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition

theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition_contDiffOn line 5581
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrected_curve_contMDiffOn line 5600
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrected_actual_energy line 5613
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_distance_le_of_differential line 5651
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_locally_almost_isometric line 5698
theorem OAI.PositiveEinsteinFour.Geometry.metricDistance_le_of_speed_bound_off_finite line 5729
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_corner_shortening line 5792
structure OAI.PositiveEinsteinFour.Geometry.NormalEndpointJetData line 5853
def OAI.PositiveEinsteinFour.Geometry.normalEndpointJetData line 5873
def OAI.PositiveEinsteinFour.Geometry.normalSegmentPosition line 5883
def OAI.PositiveEinsteinFour.Geometry.normalSegmentCurve line 5888

theorem OAI.PositiveEinsteinFour.Geometry.normalSegment_common_radius line 5894

Source documentation

A single positive parameter radius keeps the entire corrected segment inside its chart and inside both endpoint-jet neighborhoods.

theorem normalSegment_common_radius (g : SmoothMetric M) (e : FrameBundle g) (c : M)
    (N : ℝ → Fin 3 → ℝ) {a b : ℝ} (hab : a < b)
    (hc : ∀ t ∈ Icc a b, frameGeodesic g 0 e t ∈ (chartAt FourSpace c).source)
    (hN : ContinuousOn N (Icc a b))
    (A : NormalEndpointJetData g (parallelFrameFlowMap g 0 a e) c (N a))
    (B : NormalEndpointJetData g (parallelFrameFlowMap g 0 b e) c (N b)) :
    ∃ δ > 0, δ ≤ A.radius ∧ δ ≤ B.radius ∧ ∀ ε ∈ Icc (-δ) δ, ∀ t ∈ Icc a b,
      normalSegmentPosition g e c N A.position B.position a b ε t ∈
        (chartAt FourSpace c).target := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.frameGeodesic, OAI.PositiveEinsteinFour.Geometry.NormalEndpointJetData, OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap, OAI.PositiveEinsteinFour.Geometry.normalSegmentPosition

theorem OAI.PositiveEinsteinFour.Geometry.normalSegmentCurve_zero line 5921
theorem OAI.PositiveEinsteinFour.Geometry.normalSegmentCurve_endpoints line 5931
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_ray_distance line 5965
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_no_minimizing_corner line 5973
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticSegment_common_radius line 6036
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticSegmentCurve_zero line 6063
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticSegmentCurve_endpoints line 6073
def OAI.PositiveEinsteinFour.Geometry.normalSegmentVelocity line 6107
def OAI.PositiveEinsteinFour.Geometry.normalSegmentEnergy line 6114
theorem OAI.PositiveEinsteinFour.Geometry.normalSegmentCurve_contMDiffOn line 6119
theorem OAI.PositiveEinsteinFour.Geometry.normalSegmentEnergy_eq_actual line 6139
theorem OAI.PositiveEinsteinFour.Geometry.normalSegmentEnergy_zero line 6155
def OAI.PositiveEinsteinFour.Geometry.reverseDirection line 6192
def OAI.PositiveEinsteinFour.Geometry.reverseFrameRotation line 6194
theorem OAI.PositiveEinsteinFour.Geometry.reverseFrameRotation_matrix line 6196
def OAI.PositiveEinsteinFour.Geometry.frameAntipode line 6205
theorem OAI.PositiveEinsteinFour.Geometry.frameAntipode_chart line 6208
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameCurveAt_antipode line 6212
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlowMap_antipode line 6235
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_first_ray_neg line 6250
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_first_ray_all line 6267
theorem OAI.PositiveEinsteinFour.Geometry.endpointCorrectedPosition_continuousAt line 6289
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticSegmentCurve_continuousAt line 6308
theorem OAI.PositiveEinsteinFour.Geometry.normalSegmentEnergy_secondDeriv line 6354
theorem OAI.PositiveEinsteinFour.Geometry.normalSegmentEnergy_first_differentiable line 6407
theorem OAI.PositiveEinsteinFour.Geometry.joint_exponential_log_radial_eventually line 6477
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_shift_first line 6525
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_minimizing_split_extends line 6532
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticSegmentEnergy_zero line 6606
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticSegmentEnergy_secondDeriv line 6626
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticSegmentEnergy_first_differentiable line 6679
theorem OAI.PositiveEinsteinFour.Geometry.normalSegmentSecond_integral line 6753
theorem OAI.PositiveEinsteinFour.Geometry.normalSegmentEnergy_index_secondDeriv line 6817
def OAI.PositiveEinsteinFour.Geometry.frameDistanceSplitTimes line 6856
theorem OAI.PositiveEinsteinFour.Geometry.frameDistanceSplitTimes_compact line 6860
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_reaches_of_positive_split line 6873
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_global_minimizing line 6896
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_surjective line 6944
theorem OAI.PositiveEinsteinFour.Geometry.normalEndpointCurve_zero line 6972
theorem OAI.PositiveEinsteinFour.Geometry.finite_geodesic_normal_index_nonneg line 6981
theorem OAI.PositiveEinsteinFour.Geometry.chartEnergyFirstDensity_covariant line 7107
theorem OAI.PositiveEinsteinFour.Geometry.frame_normal_first_density_zero line 7121
theorem OAI.PositiveEinsteinFour.Geometry.normalChartField_first_density_zero line 7141
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticSegmentSecond_integral line 7166
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticSegmentEnergy_index_secondDeriv line 7226
def OAI.PositiveEinsteinFour.Geometry.actualMinimizingTangentDomain line 7263
theorem OAI.PositiveEinsteinFour.Geometry.actualMinimizingTangentDomain_closed line 7267
theorem OAI.PositiveEinsteinFour.Geometry.actualMinimizingTangentDomain_compact line 7272
theorem OAI.PositiveEinsteinFour.Geometry.actualMinimizingTangentDomain_image line 7282
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_direction_ray line 7291
theorem OAI.PositiveEinsteinFour.Geometry.actualMinimizingTangentDomain_ray_iff line 7299
theorem OAI.PositiveEinsteinFour.Geometry.normalQuadraticSegmentEnergy_first_zero line 7329
theorem OAI.PositiveEinsteinFour.Geometry.scalar_tensor_square line 7427
def OAI.PositiveEinsteinFour.Geometry.scalarDirichletDensity line 7444
Source documentation
The squared norm of the scalar differential on the base.
```
def scalarDirichletDensity (g : SmoothMetric M) (a : M → ℝ) (c : M) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarDirichletDensity_eq_frame line 7448
theorem OAI.PositiveEinsteinFour.Geometry.scalarDirichletDensity_nonneg line 7456
theorem OAI.PositiveEinsteinFour.Geometry.scalarDirichletDensity_continuous line 7463
theorem OAI.PositiveEinsteinFour.Geometry.scalarGradient_eq_zero_of_laplacian_eq_zero line 7475
theorem OAI.PositiveEinsteinFour.Geometry.scalar_eq_along_parallelFlow_of_gradient_eq_zero line 7513
theorem OAI.PositiveEinsteinFour.Geometry.scalar_eq_on_exponential_of_gradient_eq_zero line 7528
theorem OAI.PositiveEinsteinFour.Geometry.scalar_constants_of_gradient_eq_zero line 7562
Source documentation
Vanishing actual scalar differential implies constancy on the connected compact manifold.
```
theorem scalar_constants_of_gradient_eq_zero (g : SmoothMetric M)
    (o : FrameOrientation g) (hRic : RicciThree g) {a : M → ℝ}
    (ha : ContMDiff I4 𝓘(ℝ, ℝ) ∞ a)
    (hgrad : ∀ e : FrameBundle g, ∀ i, scalarGradient g a e i = 0) :
    ∃ c : ℝ, ∀ x, a x = c := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.scalarGradient
theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacian_kernel_constants line 7577
Source documentation
A smooth harmonic scalar is constant for the actual normalized metric. The Ricci normalization supplies the invariant flow data.
```
theorem scalarLaplacian_kernel_constants (g : SmoothMetric M)
    (o : FrameOrientation g) (hRic : RicciThree g) {a : M → ℝ}
    (ha : ContMDiff I4 𝓘(ℝ, ℝ) ∞ a)
    (hLap : ∀ e : FrameBundle g, scalarLaplacian g a e = 0) :
    ∃ c : ℝ, ∀ x, a x = c := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.scalarLaplacian
theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacian_kernel_meanZero line 7588
theorem OAI.PositiveEinsteinFour.Geometry.two_piece_geodesic_index_nonneg line 7620
theorem OAI.PositiveEinsteinFour.Geometry.positive_frames_relative_rotation line 7712
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_minimizing_initial_unique line 7727
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_minimizing_before_cut_unique line 7777
def OAI.PositiveEinsteinFour.Geometry.actualMinimizingFramePairs line 7824
theorem OAI.PositiveEinsteinFour.Geometry.actualMinimizingFramePairs_compact line 7828
theorem OAI.PositiveEinsteinFour.Geometry.minimizing_vectors_common_neighborhood line 7844
theorem OAI.PositiveEinsteinFour.Geometry.actualCutTime_le_firstConjugateTime line 7892
theorem OAI.PositiveEinsteinFour.Geometry.frameMinimizingTime_le_firstConjugateTime line 7926
theorem OAI.PositiveEinsteinFour.Geometry.actualCutTime_le_pi line 7935
theorem OAI.PositiveEinsteinFour.Geometry.minimizing_vectors_near_unique line 7956
theorem OAI.PositiveEinsteinFour.Geometry.actualCutTime_second_minimizing_vector line 7976
theorem OAI.PositiveEinsteinFour.Geometry.orientedEuclidean_det line 8052
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_chart_det_rotate line 8062
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_metric_jacobian_direction line 8094
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_minimizing_of_cut_lower line 8136
theorem OAI.PositiveEinsteinFour.Geometry.direction_injective_of_cut_lower line 8156
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_injOn_ball_of_cut_lower line 8186
theorem OAI.PositiveEinsteinFour.Geometry.exists_uniform_exponential_injective_radius line 8233
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_minimizing_of_injOn line 8271
theorem OAI.PositiveEinsteinFour.Geometry.exists_uniform_positive_cut_time line 8289
theorem OAI.PositiveEinsteinFour.Geometry.exists_finite_parallel_normal_shortening line 8325
def OAI.PositiveEinsteinFour.Geometry.scalarFlowTranslation line 8477
Source documentation
The L² isometry obtained by translating an actual scalar field along one parallel flow.
```
def scalarFlowTranslation (d : ParallelMetricData g μ) (i : Fin 4) (t : ℝ) :
    ScalarL2 g μ →L[ℝ] ScalarL2 g μ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.ScalarL2
theorem OAI.PositiveEinsteinFour.Geometry.scalarFlowTranslation_norm line 8483
def OAI.PositiveEinsteinFour.Geometry.scalarTranslatedField line 8487
theorem OAI.PositiveEinsteinFour.Geometry.scalarFlowTranslation_toLp line 8491
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalar_flow_translation_bound line 8504
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_flow_translation_bound line 8542
Source documentation
The smooth translation estimate extends to the actual first-jet closure.
```
theorem scalarH1_flow_translation_bound (d : ParallelMetricData g μ)
    (i : Fin 4) (hzero : ∀ e, (d.flow i).map 0 e = e)
    (u : scalarH1 d) (t : ℝ) :
    ‖scalarFlowTranslation d i t (scalarH1Value d u) - scalarH1Value d u‖ ≤
      |t| * ‖scalarH1Gradient d i u‖ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.scalarFlowTranslation, OAI.PositiveEinsteinFour.Geometry.scalarH1Value, OAI.PositiveEinsteinFour.Geometry.scalarH1Gradient
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_flow_invariant_of_gradient_zero line 8563
theorem OAI.PositiveEinsteinFour.Geometry.actual_scalarH1_flow_translation_bound line 8582
theorem OAI.PositiveEinsteinFour.Geometry.actual_scalarH1_flow_invariant_of_gradient_zero line 8593
theorem OAI.PositiveEinsteinFour.Geometry.scalarGradient_zero_of_weighted_energy line 8627
abbrev OAI.PositiveEinsteinFour.Geometry.ZeroFormDeRhamCohomology line 8684
def OAI.PositiveEinsteinFour.Geometry.scalarConstantLinear line 8689
def OAI.PositiveEinsteinFour.Geometry.scalarConstantToDeRham line 8694
theorem OAI.PositiveEinsteinFour.Geometry.scalarConstantToDeRham_injective line 8701
theorem OAI.PositiveEinsteinFour.Geometry.scalarConstantToDeRham_surjective line 8708
def OAI.PositiveEinsteinFour.Geometry.scalarConstantDeRhamEquiv line 8722
theorem OAI.PositiveEinsteinFour.Geometry.zeroFormDeRhamCohomology_finite line 8727
theorem OAI.PositiveEinsteinFour.Geometry.zeroFormDeRhamCohomology_finrank line 8732
theorem OAI.PositiveEinsteinFour.Geometry.scalar_decreases_right line 8751
theorem OAI.PositiveEinsteinFour.Geometry.uniform_cut_initial_vector_unique line 8763
theorem OAI.PositiveEinsteinFour.Geometry.actualCutTime_common_lower_bound line 8797
theorem OAI.PositiveEinsteinFour.Geometry.actualCutTime_lowerSemicontinuousOn_positive line 8829
theorem OAI.PositiveEinsteinFour.Geometry.exists_minimal_actualCutTime line 8843
def OAI.PositiveEinsteinFour.Geometry.frameExponentialGram line 8878
def OAI.PositiveEinsteinFour.Geometry.frameExponentialJacobian line 8884
theorem OAI.PositiveEinsteinFour.Geometry.frameExponentialGram_continuous line 8887
theorem OAI.PositiveEinsteinFour.Geometry.frameExponentialJacobian_continuous line 8903
theorem OAI.PositiveEinsteinFour.Geometry.frameExponentialJacobian_nonneg line 8907
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_chart_backward line 8911
theorem OAI.PositiveEinsteinFour.Geometry.euclideanMatrix_column line 8930
theorem OAI.PositiveEinsteinFour.Geometry.frameExponentialJacobian_chart line 8939
theorem OAI.PositiveEinsteinFour.Geometry.exponential_log_norm_lt_along_curve line 8992
theorem OAI.PositiveEinsteinFour.Geometry.exists_moving_positive_frame line 9028
def OAI.PositiveEinsteinFour.Geometry.chartCoordinateExtension line 9080
theorem OAI.PositiveEinsteinFour.Geometry.chartCoordinateExtension_measurable line 9084
theorem OAI.PositiveEinsteinFour.Geometry.chartCoordinateExtension_eq line 9090
def OAI.PositiveEinsteinFour.Geometry.chartWeight line 9097
theorem OAI.PositiveEinsteinFour.Geometry.chartWeight_eq line 9103
theorem OAI.PositiveEinsteinFour.Geometry.chartWeight_measurable line 9110
def OAI.PositiveEinsteinFour.Geometry.exponentialAreaMeasure line 9119
theorem OAI.PositiveEinsteinFour.Geometry.exponentialAreaMeasure_apply line 9126
theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_le_exponentialAreaMeasure_on_chart line 9136
theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_le_exponentialAreaMeasure line 9194
theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_le_integral_exponentialJacobian line 9209
theorem OAI.PositiveEinsteinFour.Geometry.minimal_cut_terminal_opposite line 9235
theorem OAI.PositiveEinsteinFour.Geometry.moving_frame_chart_vector_continuousAt line 9379
theorem OAI.PositiveEinsteinFour.Geometry.short_inverse_branches_limit line 9395
theorem OAI.PositiveEinsteinFour.Geometry.short_variation_log_norm_lt line 9460
def OAI.PositiveEinsteinFour.Geometry.exponentialBallAreaMeasure line 9547
theorem OAI.PositiveEinsteinFour.Geometry.exponentialBallAreaMeasure_apply line 9553
theorem OAI.PositiveEinsteinFour.Geometry.exponentialBallAreaMeasure_le_on_chart line 9563
theorem OAI.PositiveEinsteinFour.Geometry.exponentialBallAreaMeasure_le line 9616
theorem OAI.PositiveEinsteinFour.Geometry.exponential_ball_integral_le_volume line 9631
theorem OAI.PositiveEinsteinFour.Geometry.frameExponentialJacobian_direction line 9659
theorem OAI.PositiveEinsteinFour.Geometry.minimizing_exponential_integral_polar line 9672
theorem OAI.PositiveEinsteinFour.Geometry.affinePartitionTime_strictMono line 9722
theorem OAI.PositiveEinsteinFour.Geometry.exists_parallel_short_branch line 9733