GeodesicGeometry12.lean`

GitHub source file

306 declarations, 0 contain sorry, 0 declared as axioms

Dominated convergence for the actual averaged lower Jacobi comparison.

def OAI.PositiveEinsteinFour.Geometry.actualFlatKernelDeterminant line 46
theorem OAI.PositiveEinsteinFour.Geometry.actualFlatKernelDeterminant_continuous line 51
theorem OAI.PositiveEinsteinFour.Geometry.actualFlatKernelDeterminant_tendsto line 61
theorem OAI.PositiveEinsteinFour.Geometry.actualFlatKernelDeterminant_integral_tendsto line 74
theorem OAI.PositiveEinsteinFour.Geometry.models_of_actual_normalized_model_input line 114
theorem OAI.PositiveEinsteinFour.Geometry.models_of_actual_model_inputs line 123
def OAI.PositiveEinsteinFour.ModelOrientedInputs line 156
Source documentation
The Derdzinski--Hitchin special case applies after establishing Weyl vanishing.
```
def ModelOrientedInputs (X : ClosedOrientedMetricFour.{u}) : Prop :=
…
```
structure OAI.PositiveEinsteinFour.ModelClassificationInputs line 162
theorem OAI.PositiveEinsteinFour.classificationOn_of_model_inputs line 169
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.eq_sine_of_curvature_one line 192
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvature_eq_one_of_weyl_zero line 234
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_eq_sine_of_weyl_zero line 254
theorem OAI.PositiveEinsteinFour.Geometry.actualFirstConjugateTime_eq_pi_of_weyl_zero line 263
theorem OAI.PositiveEinsteinFour.Geometry.matrixPairing_swap line 292
theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_pairing line 295
theorem OAI.PositiveEinsteinFour.Geometry.constant_matrix_norm_pairing line 302
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.unit_norm_first_pairing line 319
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.unit_norm_second_pairing line 335
theorem OAI.PositiveEinsteinFour.Geometry.actual_unit_weyl_parallel line 359
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_determinant_lower_cap line 417
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_determinant_pos_below_sqrt_three line 429
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_isUnit_below_sqrt_three line 442
theorem OAI.PositiveEinsteinFour.Geometry.actualFirstConjugateTime_lower_sqrt_three line 449
theorem OAI.PositiveEinsteinFour.Geometry.actual_jacobi_average_lower_normalized line 474
theorem OAI.PositiveEinsteinFour.Geometry.actual_jacobi_average_lower line 504
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_round_localChart line 533
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_round_isLocalHomeomorphOn line 558
theorem OAI.PositiveEinsteinFour.Geometry.round_jacobi_gram line 586
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_first_of_weyl_zero line 605
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_pi_normal_differential_zero line 646
theorem OAI.PositiveEinsteinFour.Geometry.round_normalized_volume_eq_one line 687
theorem OAI.PositiveEinsteinFour.Geometry.round_normalized_totalVolume line 702
def OAI.PositiveEinsteinFour.Geometry.roundBoundaryProjection line 726
theorem OAI.PositiveEinsteinFour.Geometry.roundBoundaryProjection_norm line 728
theorem OAI.PositiveEinsteinFour.Geometry.roundBoundaryProjection_differentiableAt line 734
theorem OAI.PositiveEinsteinFour.Geometry.roundBoundaryProjection_derivative_tangent line 740
def OAI.PositiveEinsteinFour.Geometry.roundRadialMass line 773
theorem OAI.PositiveEinsteinFour.Geometry.roundRadialMass_formula line 776
theorem OAI.PositiveEinsteinFour.Geometry.roundRadialMass_pi line 789
theorem OAI.PositiveEinsteinFour.Geometry.roundRadialMass_le_pi line 793
theorem OAI.PositiveEinsteinFour.Geometry.roundRadialMass_lt_pi line 797
def OAI.PositiveEinsteinFour.Geometry.roundNorth line 822
def OAI.PositiveEinsteinFour.Geometry.roundPolarVector line 824
theorem OAI.PositiveEinsteinFour.Geometry.roundPolarVector_norm line 827
def OAI.PositiveEinsteinFour.Geometry.roundPolarPoint line 838
theorem OAI.PositiveEinsteinFour.Geometry.roundPolarPoint_first line 841
theorem OAI.PositiveEinsteinFour.Geometry.roundPolarPoint_tail line 844
theorem OAI.PositiveEinsteinFour.Geometry.roundPolarPoint_zero line 847
theorem OAI.PositiveEinsteinFour.Geometry.roundPolarPoint_pi line 854
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_polar line 862
def OAI.PositiveEinsteinFour.Geometry.roundTail line 869
theorem OAI.PositiveEinsteinFour.Geometry.roundTail_norm_sq line 872
theorem OAI.PositiveEinsteinFour.Geometry.roundFirst_bounds line 880
theorem OAI.PositiveEinsteinFour.Geometry.roundTail_norm_arccos line 885
theorem OAI.PositiveEinsteinFour.Geometry.exists_roundPolarPoint line 889
theorem OAI.PositiveEinsteinFour.Geometry.roundTail_zero_cases line 917
theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.hessian_zero_of_gradient_zero line 960
theorem OAI.PositiveEinsteinFour.Geometry.actual_unit_weyl_polynomial line 980
theorem OAI.PositiveEinsteinFour.Jacobi.sine_exponential_lower_refined line 1015
theorem OAI.PositiveEinsteinFour.Geometry.actual_jacobi_average_lower_refined line 1039
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_truncated_eq_det_below_sqrt_three line 1074
theorem OAI.PositiveEinsteinFour.Geometry.canonical_actualBallRadialMass_eq line 1085
theorem OAI.PositiveEinsteinFour.Geometry.lower_polar_volume_of_injective_ball line 1117
theorem OAI.PositiveEinsteinFour.Geometry.frameAntipode_vector line 1148
theorem OAI.PositiveEinsteinFour.Geometry.frameAntipode_flow_cancel line 1157
theorem OAI.PositiveEinsteinFour.Geometry.minimal_cut_pair_initial_opposite line 1163
theorem OAI.PositiveEinsteinFour.Geometry.exists_closed_geodesic_at_minimal_cut line 1210
theorem OAI.PositiveEinsteinFour.Geometry.zero_chart_derivative_locally_constant line 1287
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_pi_first_tangent_zero line 1332
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_pi_angular_derivative_zero line 1352
theorem OAI.PositiveEinsteinFour.Geometry.round_actual_cut_mass line 1418
theorem OAI.PositiveEinsteinFour.Geometry.round_volume_le_cut_mass line 1449
theorem OAI.PositiveEinsteinFour.Geometry.round_volumeMeasure line 1466
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_eq_angle line 1496
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_nonneg line 1501
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_le_pi line 1504
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_comm line 1507
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_triangle line 1510
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_self line 1515
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_eq_zero_iff line 1518
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_continuous line 1527
theorem OAI.PositiveEinsteinFour.Geometry.round_inner_bounds line 1533
theorem OAI.PositiveEinsteinFour.Geometry.cos_roundDistance line 1538
theorem OAI.PositiveEinsteinFour.Geometry.round_chord_sq line 1542
theorem OAI.PositiveEinsteinFour.Geometry.round_tangent_pairing_bound line 1547
def OAI.PositiveEinsteinFour.Geometry.unitWeylProjection line 1578
theorem OAI.PositiveEinsteinFour.Geometry.unitWeylProjection_idempotent line 1580
theorem OAI.PositiveEinsteinFour.Geometry.unitWeylProjection_symmetric line 1590
theorem OAI.PositiveEinsteinFour.Geometry.unitWeylProjection_trace line 1598
theorem OAI.PositiveEinsteinFour.Geometry.unitWeylProjection_posSemidef line 1605
theorem OAI.PositiveEinsteinFour.Geometry.unitWeyl_upper_posSemidef line 1613
theorem OAI.PositiveEinsteinFour.Geometry.closed_geodesic_fixed_normal line 1646
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_curvature_matrix_positive line 1690
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_curvature_matrix_bound line 1711
theorem OAI.PositiveEinsteinFour.VolumeConstants.lowerVolumeKernel_rescale line 1743
theorem OAI.PositiveEinsteinFour.Geometry.actual_scaled_jacobi_lower line 1768
theorem OAI.PositiveEinsteinFour.Geometry.round_cut_time_all_directions line 1812
def OAI.PositiveEinsteinFour.Geometry.roundBoundaryEndpoint line 1884
theorem OAI.PositiveEinsteinFour.Geometry.roundBoundaryEndpoint_chart_derivative_zero line 1888
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_pi_independent_direction line 1915
theorem OAI.PositiveEinsteinFour.Geometry.round_block_pairing line 1964
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_round_first_pairing line 1980
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_round_pairing line 1995
theorem OAI.PositiveEinsteinFour.Geometry.round_inner_ne_endpoints line 2063
theorem OAI.PositiveEinsteinFour.Geometry.round_curve_tangent line 2077
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_derivative_bound line 2090
theorem OAI.PositiveEinsteinFour.Geometry.zero_chart_curve_constant line 2138
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_unit_curvature_bound line 2181
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_positive_harmonic_covariantEnergy_zero line 2207
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_covariantDerivative_zero_of_energy_zero line 2229
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_positive_harmonic_parallel line 2251
def OAI.PositiveEinsteinFour.Geometry.roundLog line 2272
theorem OAI.PositiveEinsteinFour.Geometry.roundTail_polar line 2276
theorem OAI.PositiveEinsteinFour.Geometry.roundLog_polar_interior line 2281
theorem OAI.PositiveEinsteinFour.Geometry.roundLog_polar_zero line 2291
theorem OAI.PositiveEinsteinFour.Geometry.roundLog_polar_pi line 2295
def OAI.PositiveEinsteinFour.Geometry.roundSphereMap line 2305
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_polar line 2308
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_surjective line 2326
theorem OAI.PositiveEinsteinFour.Geometry.parallelFrameFlow_vector_eq line 2369
theorem OAI.PositiveEinsteinFour.Geometry.frameAntipode_map line 2399
theorem OAI.PositiveEinsteinFour.Geometry.closed_geodesic_normal_midpoint line 2410
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_curve_continuous line 2435
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_curve_deriv_bound line 2445
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_curve_sub_le line 2455
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_curve_le line 2469
theorem OAI.PositiveEinsteinFour.Geometry.strict_lower_volume_of_injective_ball line 2496
theorem OAI.PositiveEinsteinFour.Geometry.normalCoordinates_neg line 2559
theorem OAI.PositiveEinsteinFour.Geometry.closed_geodesic_antipode_midpoint_base line 2566
theorem OAI.PositiveEinsteinFour.Geometry.closed_geodesic_impossible_below_uniform_cut line 2578
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_dimension_two_impossible_of_injective_ball line 2639
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_positive_harmonic_dimension_one_of_injective_ball line 2659
theorem OAI.PositiveEinsteinFour.Geometry.roundLog_norm line 2683
theorem OAI.PositiveEinsteinFour.Geometry.roundLog_north line 2692
theorem OAI.PositiveEinsteinFour.Geometry.roundLog_south line 2696
def OAI.PositiveEinsteinFour.Geometry.roundAntipodalPoint line 2700
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_north line 2711
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_south line 2716
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_distance_north line 2722
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_distance_south line 2727
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_allFrames_covariant_zero line 2762
theorem OAI.PositiveEinsteinFour.Geometry.parallel_twoForm_along_flow line 2783
theorem OAI.PositiveEinsteinFour.Geometry.parallel_twoForm_norm_along_flow line 2801
theorem OAI.PositiveEinsteinFour.Geometry.parallel_twoForm_norm_on_exponential line 2810
theorem OAI.PositiveEinsteinFour.Geometry.parallel_twoForm_norm_constant line 2839
theorem OAI.PositiveEinsteinFour.Geometry.actualCutTime_lower_sqrt_three line 2865
theorem OAI.PositiveEinsteinFour.Geometry.actual_frameExponential_injOn_sqrt_three line 2882
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_dimension_one_parallel_unit_form line 2912
theorem OAI.PositiveEinsteinFour.Geometry.roundTail_continuous line 2969
theorem OAI.PositiveEinsteinFour.Geometry.roundPolarAngle_continuous line 2973
theorem OAI.PositiveEinsteinFour.Geometry.roundLog_continuousAt line 2977
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_continuous line 2992
def OAI.PositiveEinsteinFour.Geometry.roundSphereExponential line 3043
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereExponential_zero line 3049
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereExponential_radial line 3052
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereExponential_vector line 3066
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereExponential_continuous line 3082
theorem OAI.PositiveEinsteinFour.Geometry.selfDual_twoFormMatrix_square line 3102
theorem OAI.PositiveEinsteinFour.Geometry.selfDual_twoFormMatrix_orthogonal line 3120
theorem OAI.PositiveEinsteinFour.Geometry.unit_selfDual_frame_complex line 3129
theorem OAI.PositiveEinsteinFour.Geometry.parallel_twoForm_secondDerivative_zero line 3161
theorem OAI.PositiveEinsteinFour.Geometry.parallel_twoForm_roughTrace_zero line 3182
theorem OAI.PositiveEinsteinFour.Geometry.parallel_twoForm_harmonic line 3191
theorem OAI.PositiveEinsteinFour.Geometry.parallel_twoForm_curvature_eigenvalue line 3209
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereExponential_log line 3250
theorem OAI.PositiveEinsteinFour.Geometry.roundLog_sphereExponential line 3266
theorem OAI.PositiveEinsteinFour.Geometry.roundLog_norm_lt_pi line 3280
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereExponential_ne_south line 3288
theorem OAI.PositiveEinsteinFour.Geometry.roundLog_continuousAt_north line 3297
theorem OAI.PositiveEinsteinFour.Geometry.roundLog_continuousOn line 3303
def OAI.PositiveEinsteinFour.Geometry.roundSpherePolarChart line 3312
theorem OAI.PositiveEinsteinFour.Geometry.round_norm_fderiv line 3346
def OAI.PositiveEinsteinFour.Geometry.roundSphereLinearInclusion line 3360
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereLinearInclusion_first line 3370
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereLinearInclusion_tail line 3373
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereExponential_differentiableAt line 3376
def OAI.PositiveEinsteinFour.Geometry.complexCircleMatrix line 3402
theorem OAI.PositiveEinsteinFour.Geometry.complexCircleMatrix_orthogonal line 3405
def OAI.PositiveEinsteinFour.Geometry.complexCircleVector line 3416
theorem OAI.PositiveEinsteinFour.Geometry.complexCircleVector_eq_matrix line 3419
theorem OAI.PositiveEinsteinFour.Geometry.complexCircleVector_norm line 3425
theorem OAI.PositiveEinsteinFour.Geometry.complexCircleVector_hasDerivAt line 3432
theorem OAI.PositiveEinsteinFour.Geometry.complexCircleVector_zero line 3449
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_localChart line 3470
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_isLocalHomeomorphOn line 3486
theorem OAI.PositiveEinsteinFour.Geometry.symmetric_projection_trace_one line 3510
theorem OAI.PositiveEinsteinFour.Geometry.unitWeylProjection_eq_vector line 3544
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereExponential_fderiv line 3577
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereLinearInclusion_inner line 3625
theorem OAI.PositiveEinsteinFour.Geometry.roundSphere_radial_pairing line 3634
theorem OAI.PositiveEinsteinFour.Geometry.roundSphere_compact line 3668
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_isCoveringMapOn line 3677
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_exponential line 3711
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_round_metric_eq_sphere line 3729
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_parallel_form_weyl line 3776
def OAI.PositiveEinsteinFour.Geometry.complexSpaceCurvature line 3857
theorem OAI.PositiveEinsteinFour.Geometry.complexSpaceCurvature_firstSkew line 3864
theorem OAI.PositiveEinsteinFour.Geometry.complexSpaceCurvature_lastSkew line 3872
theorem OAI.PositiveEinsteinFour.Geometry.complexSpace_matrix_row0 line 3880
theorem OAI.PositiveEinsteinFour.Geometry.complexSpace_matrix_row1 line 3893
theorem OAI.PositiveEinsteinFour.Geometry.complexSpace_matrix_row2 line 3906
theorem OAI.PositiveEinsteinFour.Geometry.complexSpace_matrix_row3 line 3919
theorem OAI.PositiveEinsteinFour.Geometry.complexSpace_matrix_row4 line 3932
theorem OAI.PositiveEinsteinFour.Geometry.complexSpace_matrix_row5 line 3945
theorem OAI.PositiveEinsteinFour.Geometry.selfDual_complexSpaceCurvature line 3958
theorem OAI.PositiveEinsteinFour.Geometry.metric_curve_speed_congr line 4015
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_round_curve_speed line 4028
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_round_minimizing line 4079
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_radial_distance line 4102
theorem OAI.PositiveEinsteinFour.Geometry.parallel_twoForm_frameValue_along_flow line 4131
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvature_parallel_form line 4139
def OAI.PositiveEinsteinFour.Jacobi.complexJacobiSlow line 4178
def OAI.PositiveEinsteinFour.Jacobi.complexJacobiFast line 4179
theorem OAI.PositiveEinsteinFour.Jacobi.sqrt_two_inverse line 4181
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiSlow_hasDerivAt line 4185
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiFast_hasDerivAt line 4192
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiSlow_velocity_hasDerivAt line 4199
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiFast_velocity_hasDerivAt line 4207
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_parallel_form_curvature line 4232
theorem OAI.PositiveEinsteinFour.Geometry.actual_dimension_one_complex_curvature line 4260
theorem OAI.PositiveEinsteinFour.Geometry.round_direction_injective line 4294
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_round_injOn_ball line 4326
def OAI.PositiveEinsteinFour.Jacobi.complexJacobiCurvature line 4373
def OAI.PositiveEinsteinFour.Jacobi.complexJacobiPosition line 4376
def OAI.PositiveEinsteinFour.Jacobi.complexJacobiVelocity line 4379
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiCurvature_mul_projection line 4382
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiCurvature_mul_complement line 4390
def OAI.PositiveEinsteinFour.Jacobi.complexModelJacobi line 4398
theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.eq_complex_projection line 4421
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiSlow_sq line 4447
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiFast_sq line 4451
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiFast_sq_sub_slow_sq line 4463
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_injective line 4489
def OAI.PositiveEinsteinFour.Geometry.actualRoundHomeomorph line 4522
theorem OAI.PositiveEinsteinFour.Geometry.actualRoundHomeomorph_apply line 4534
theorem OAI.PositiveEinsteinFour.Jacobi.rankOne_two_eigenvalue_determinant line 4554
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiPosition_det line 4569
def OAI.PositiveEinsteinFour.Jacobi.complexJacobiRadius line 4574
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiRadius_pos line 4576
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiFast_radius line 4579
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiFast_pos line 4584
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiSlow_pos line 4594
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiPosition_det_pos line 4604
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiPosition_det_radius line 4610
theorem OAI.PositiveEinsteinFour.Geometry.metricDistance_symm line 4636
theorem OAI.PositiveEinsteinFour.Geometry.round_antipodal_distance line 4642
theorem OAI.PositiveEinsteinFour.Geometry.round_antipodal_distance_sum line 4653
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_antipode_left line 4676
theorem OAI.PositiveEinsteinFour.Geometry.roundDistance_antipodal line 4683
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_distance_eq_of_le line 4687
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_round_mfderiv_isUnit line 4747
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_round_inverse_contMDiffAt line 4792
theorem OAI.PositiveEinsteinFour.Geometry.selfDual_firstThree_unit line 4818
theorem OAI.PositiveEinsteinFour.Geometry.unitSelfDual_frame_firstThree line 4838
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_parallel_form line 4850
theorem OAI.PositiveEinsteinFour.Geometry.actualFirstConjugateTime_parallel_form line 4869
theorem OAI.PositiveEinsteinFour.Geometry.round_inverse_curve_speed line 4919
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiPosition_radius_mulVec line 4992
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_normal_kernel line 5014
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_first_kernel line 5043
def OAI.PositiveEinsteinFour.Jacobi.complexJacobiGram line 5078
theorem OAI.PositiveEinsteinFour.Jacobi.complexJacobiPosition_transpose_mul line 5081
theorem OAI.PositiveEinsteinFour.Jacobi.jacobiBlockMatrix_transpose_mul line 5094
def OAI.PositiveEinsteinFour.Geometry.complexRadialDensity line 5120
theorem OAI.PositiveEinsteinFour.Geometry.complexRadialDensity_eq line 5122
theorem OAI.PositiveEinsteinFour.Geometry.complexRadialPrimitive_hasDerivAt line 5134
theorem OAI.PositiveEinsteinFour.Geometry.complexRadialDensity_continuous line 5145
theorem OAI.PositiveEinsteinFour.Geometry.complexRadial_integral line 5149
def OAI.PositiveEinsteinFour.Geometry.complexRadialMass line 5156
theorem OAI.PositiveEinsteinFour.Geometry.complexRadialDensity_nonneg line 5159
theorem OAI.PositiveEinsteinFour.Geometry.complexRadialMass_formula line 5168
theorem OAI.PositiveEinsteinFour.Geometry.complexRadialMass_radius line 5178
theorem OAI.PositiveEinsteinFour.Geometry.complexRadialMass_le_one line 5184
theorem OAI.PositiveEinsteinFour.Geometry.complexRadialMass_lt_one line 5189
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_localChart line 5223
theorem OAI.PositiveEinsteinFour.Geometry.round_frameGeodesic_radial_distance line 5270
theorem OAI.PositiveEinsteinFour.Geometry.round_frameGeodesic_injOn line 5283
theorem OAI.PositiveEinsteinFour.Geometry.round_frameGeodesic_real_speed line 5295
theorem OAI.PositiveEinsteinFour.Geometry.round_inverse_geodesic_distance_le line 5307
theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_det_parallel_form line 5375
theorem OAI.PositiveEinsteinFour.Geometry.parallel_form_cut_le_radius line 5386
theorem OAI.PositiveEinsteinFour.Geometry.complex_actual_cut_mass line 5391
theorem OAI.PositiveEinsteinFour.Geometry.complex_volume_le_cut_mass line 5420
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameValue_rotate line 5450
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_operator_rotate line 5459
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_first_parallel_form line 5499
theorem OAI.PositiveEinsteinFour.Geometry.frameGeodesic_metricDistance_le line 5568
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_mfderiv_isUnit line 5601
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_inverse_contMDiffAt line 5649
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_distance_ge line 5682
theorem OAI.PositiveEinsteinFour.Geometry.roundSphereMap_distance_eq line 5734
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_angular_kernel line 5761
theorem OAI.PositiveEinsteinFour.Geometry.complex_normalized_totalVolume line 5832
theorem OAI.PositiveEinsteinFour.Geometry.complex_volumeMeasure line 5846
theorem OAI.PositiveEinsteinFour.Geometry.actual_round_model line 5880
def OAI.PositiveEinsteinFour.Geometry.standardSelfDualForm line 5914
theorem OAI.PositiveEinsteinFour.Geometry.selfDual_matrix_eq_imaginary line 5916
theorem OAI.PositiveEinsteinFour.Geometry.standardSelfDualForm_matrix line 5929
theorem OAI.PositiveEinsteinFour.Geometry.unitSelfDual_exists_oriented_frame line 5935
theorem OAI.PositiveEinsteinFour.Geometry.frameExponential_complex_boundary_circle line 5997
def OAI.PositiveEinsteinFour.Geometry.complexCoordinatesLinear line 6047
theorem OAI.PositiveEinsteinFour.Geometry.complexCoordinatesLinear_norm line 6057
def OAI.PositiveEinsteinFour.Geometry.complexCoordinates line 6064
theorem OAI.PositiveEinsteinFour.Geometry.complexCoordinates_standard_complex line 6067
theorem OAI.PositiveEinsteinFour.Geometry.complex_cut_time_all_directions line 6096
theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_dimension_one_standard_frame line 6170