OAI/Geometry/EinsteinFour/ScalarRegularity06.lean

GitHub source file

237 declarations, 0 contain sorry, 0 declared as axioms

Averaging the actual polar bound over the canonical frame probability. Right invariance under each oriented rotation removes the angular average; Tonelli then puts the time and frame integrals in the manuscript's order.

  1. theorem OAI.PositiveEinsteinFour.Geometry.canonicalFrame_lintegral_sphere_rotations line 44
  2. theorem OAI.PositiveEinsteinFour.Geometry.measurable_actualJacobiDensity line 64
  3. def OAI.PositiveEinsteinFour.Geometry.actualRadialMass line 71
  4. theorem OAI.PositiveEinsteinFour.Geometry.measurable_actualRadialMass line 77
  5. theorem OAI.PositiveEinsteinFour.Geometry.canonical_actualRadialMass_integral line 82
  6. theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_le_canonicalRadialMass line 93
  7. theorem OAI.PositiveEinsteinFour.Geometry.exists_uniform_actualJacobi_det_bound line 128
  8. theorem OAI.PositiveEinsteinFour.Geometry.volume_lintegral_le_bounded_radial line 143
  9. theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_average_integrableOn line 215
  10. theorem OAI.PositiveEinsteinFour.Geometry.actualJacobi_average_nonneg line 224
  11. theorem OAI.PositiveEinsteinFour.Geometry.canonical_actualRadialMass_eq line 232
  12. theorem OAI.PositiveEinsteinFour.Geometry.totalVolume_le_actualJacobiIntegral line 255
  13. theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiPolarInput_proved line 275
  14. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalar_flow_oscillation_bound line 321
  15. def OAI.PositiveEinsteinFour.Geometry.scalarGeodesicOscillation line 358
  16. theorem OAI.PositiveEinsteinFour.Geometry.scalarGeodesicOscillation_joint_continuous line 363
  17. theorem OAI.PositiveEinsteinFour.Geometry.scalarGeodesicOscillation_measurable line 372
  18. theorem OAI.PositiveEinsteinFour.Geometry.scalarGeodesicOscillation_sphere_average line 380
  19. theorem OAI.PositiveEinsteinFour.Geometry.scalarGeodesicOscillation_integral_bound line 396
  20. def OAI.PositiveEinsteinFour.Geometry.scalarRadialOscillation line 429
  21. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialOscillation_measurable line 434
  22. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialOscillation_integral line 439
  23. theorem OAI.PositiveEinsteinFour.Geometry.scalar_pair_lintegral_le_radial line 449
  24. theorem OAI.PositiveEinsteinFour.Geometry.scalar_radial_lintegral_energy_bound line 520
  25. theorem OAI.PositiveEinsteinFour.Geometry.scalar_pair_lintegral_energy_bound line 545
  26. theorem OAI.PositiveEinsteinFour.Geometry.continuous_pairwise_square_lintegral line 581
  27. def OAI.PositiveEinsteinFour.Geometry.scalarPairConstant line 605
  28. theorem OAI.PositiveEinsteinFour.Geometry.scalarPairConstant_ne_top line 610
  29. theorem OAI.PositiveEinsteinFour.Geometry.normalized_scalar_pair_energy_bound line 621
  30. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalar_value_norm_sq line 682
  31. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalar_poincare_of_bound line 695
  32. theorem OAI.PositiveEinsteinFour.Geometry.exists_smoothScalar_poincare_constant line 734
  33. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalar_centered_orthogonal_one line 769
  34. theorem OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroWeakPoisson_all_tests line 780

    Source documentation

    A mean-zero source pairs identically with a test and its mean-zero projection. Consequently the variational solution tests against all H¹.

    theorem scalarMeanZeroWeakPoisson_all_tests (d : ParallelMetricData g μ)
    {K : ℝ} (hK : 0 < K) (hP : SmoothScalarPoincare d K)
    (f : ScalarL2 g μ) (hf : inner ℝ f (scalarL2One g μ) = 0)
    (v : scalarH1 d) :
    (∑ i : Fin 4, inner ℝ
      (scalarH1Gradient d i (scalarMeanZeroWeakPoisson d hK hP f).val)
      (scalarH1Gradient d i v)) = inner ℝ f (scalarH1Value d v) := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.SmoothScalarPoincare, OAI.PositiveEinsteinFour.Geometry.ScalarL2, OAI.PositiveEinsteinFour.Geometry.scalarL2One, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.scalarH1Gradient, OAI.PositiveEinsteinFour.Geometry.scalarMeanZeroWeakPoisson, OAI.PositiveEinsteinFour.Geometry.scalarH1Value

  35. theorem OAI.PositiveEinsteinFour.Geometry.actual_scalar_weak_poisson line 808

    Source documentation

    For every actual smooth source there is a mean-zero weak solution of Δu = a - average(a), with an actual base L² representative.

    theorem actual_scalar_weak_poisson (g : SmoothMetric M)
    (o : FrameOrientation g) (hRic : RicciThree g) (a : SmoothScalar (M := M)) :
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.SmoothScalar

  36. def OAI.PositiveEinsteinFour.Geometry.smoothScalarLaplacian line 855
  37. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarLaplacian_valueL2 line 859
  38. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarValueL2_injective line 879
  39. theorem OAI.PositiveEinsteinFour.Geometry.scalar_poisson_pointwise_of_smooth_representative line 892

    Source documentation

    A smooth representative of the constructed weak solution satisfies the actual pointwise geometric Poisson equation.

    theorem scalar_poisson_pointwise_of_smooth_representative (g : SmoothMetric M)
    (o : FrameOrientation g) (hRic : RicciThree g) (a φ : SmoothScalar (M := M))
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.SmoothScalar

  40. theorem OAI.PositiveEinsteinFour.Geometry.scalarGradient_zero_of_local_min line 959
  41. theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacian_nonneg_of_local_min line 975
  42. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalar_nonneg_of_negative_laplacian_on_negative line 999

    Source documentation

    A negative minimum contradicts a strictly negative Laplacian there. This is the comparison step used for a local positive barrier.

    theorem smoothScalar_nonneg_of_negative_laplacian_on_negative (d : ParallelMetricData g μ)
    (a : SmoothScalar (M := M))
…

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

  43. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalar_nonneg_of_shifted_supersolution line 1012
  44. theorem OAI.PositiveEinsteinFour.Geometry.actual_scalar_distributional_poisson line 1049
  45. theorem OAI.PositiveEinsteinFour.Geometry.normalizedVolume_integral_chart line 1102
  46. theorem OAI.PositiveEinsteinFour.Geometry.scalarChartLift_tsupport line 1132
  47. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarBaseL2_inner_right line 1151
  48. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarBaseL2_inner line 1163
  49. theorem OAI.PositiveEinsteinFour.Geometry.normalizedChartFactor_toReal_pos line 1174
  50. theorem OAI.PositiveEinsteinFour.Geometry.actual_scalar_chart_distribution line 1185
  51. def OAI.PositiveEinsteinFour.Geometry.smoothScalarExponentialBarrier line 1245
  52. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarExponentialBarrier_gradient line 1250
  53. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarExponentialBarrier_hessian line 1262
  54. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarExponentialBarrier_laplacian line 1286
  55. theorem OAI.PositiveEinsteinFour.Geometry.scalarHessian_sub_smul line 1321
  56. theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacian_sub_smul line 1345
  57. theorem OAI.PositiveEinsteinFour.Geometry.scalar_barrier_comparison line 1354
  58. theorem OAI.PositiveEinsteinFour.Geometry.scalar_barrier_parameter line 1391
  59. theorem OAI.PositiveEinsteinFour.Geometry.scalar_exponential_barrier_strict line 1414
  60. theorem OAI.PositiveEinsteinFour.Geometry.scalarChartL2_weighted line 1455
  61. theorem OAI.PositiveEinsteinFour.Geometry.scalarChart_density_lower_bound line 1472
  62. theorem OAI.PositiveEinsteinFour.Geometry.scalarChartL2_compact line 1479
  63. theorem OAI.PositiveEinsteinFour.Geometry.scalarChartL2_cutoff line 1519
  64. def OAI.PositiveEinsteinFour.Geometry.scalarChartOperator line 1560
  65. theorem OAI.PositiveEinsteinFour.Geometry.scalarChartOperator_congr_nhds line 1566
  66. theorem OAI.PositiveEinsteinFour.Geometry.scalarChartTest_laplacian line 1585
  67. theorem OAI.PositiveEinsteinFour.Geometry.actual_scalar_coordinate_distribution line 1599
  68. def OAI.PositiveEinsteinFour.Geometry.scalarAffineMap line 1637
  69. theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineMap_hasFDerivAt line 1640
  70. theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineMap_jacobian line 1645
  71. theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineMap_partial line 1653
  72. theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineMap_partial_second line 1660
  73. theorem OAI.PositiveEinsteinFour.Geometry.partialDeriv_chartVolumeDensity line 1712
  74. theorem OAI.PositiveEinsteinFour.Geometry.scalar_metric_trace_cancellation line 1729
  75. theorem OAI.PositiveEinsteinFour.Geometry.scalar_metric_divergence_algebra line 1742
  76. theorem OAI.PositiveEinsteinFour.Geometry.scalar_metric_coefficient_divergence line 1760
  77. theorem OAI.PositiveEinsteinFour.Geometry.scalar_divergence_expansion line 1790
  78. theorem OAI.PositiveEinsteinFour.Geometry.scalar_partial_mul line 1813
  79. theorem OAI.PositiveEinsteinFour.Geometry.scalarChartOperator_divergence line 1821
  80. theorem OAI.PositiveEinsteinFour.Geometry.actual_scalar_divergence_distribution line 1853
  81. theorem OAI.PositiveEinsteinFour.Geometry.scalarGradient_chart line 1895
  82. theorem OAI.PositiveEinsteinFour.Geometry.scalar_covector_bound line 1918
  83. theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinate_gradient_sq_le line 1946
  84. theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinate_gradient_sq_le_on_compact line 1967
  85. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_weak_base_distribution line 2015
  86. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_weak_coordinate_distribution line 2045
  87. theorem OAI.PositiveEinsteinFour.Geometry.scalar_inverse_chart_ae_predicate line 2113
  88. def OAI.PositiveEinsteinFour.Geometry.scalarRadialChartCorrection line 2162
  89. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialChartCorrection_smooth line 2165
  90. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialChartCorrection_compact line 2171
  91. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialChartCorrection_support line 2175
  92. def OAI.PositiveEinsteinFour.Geometry.scalarRadialChartFunction line 2181
  93. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialChartFunction_on_source line 2190
  94. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialChartFunction_off_source line 2199
  95. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialBlend_lower line 2206
  96. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialChartFunction_nonneg line 2212
  97. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialChartFunction_on_inner line 2221
  98. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialChartFunction_small line 2231
  99. theorem OAI.PositiveEinsteinFour.Geometry.scalar_no_zero_at_radial_contact line 2279
  100. def OAI.PositiveEinsteinFour.Geometry.scalarAffineJacobian line 2368
  101. theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineJacobian_pos line 2371
  102. theorem OAI.PositiveEinsteinFour.Geometry.scalarAffine_map_volume line 2375
  103. theorem OAI.PositiveEinsteinFour.Geometry.scalarAffine_integral line 2385
  104. theorem OAI.PositiveEinsteinFour.Geometry.scalarAffine_memLp line 2393
  105. def OAI.PositiveEinsteinFour.Geometry.scalarAffinePullbackL2 line 2401
  106. theorem OAI.PositiveEinsteinFour.Geometry.scalarAffinePullbackL2_coe line 2405
  107. def OAI.PositiveEinsteinFour.Geometry.scalarPartialVector line 2426
  108. def OAI.PositiveEinsteinFour.Geometry.scalarPartialMatrix line 2429
  109. def OAI.PositiveEinsteinFour.Geometry.scalarPrincipalContraction line 2432
  110. theorem OAI.PositiveEinsteinFour.Geometry.scalarPrincipalContraction_eq_trace line 2434
  111. theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineMap_partialVector line 2439
  112. theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineMap_partialMatrix line 2446
  113. theorem OAI.PositiveEinsteinFour.Geometry.scalarPrincipalContraction_affine line 2460
  114. def OAI.PositiveEinsteinFour.Geometry.scalarChartDrift line 2475
  115. theorem OAI.PositiveEinsteinFour.Geometry.scalarChartOperator_eq_contraction line 2478
  116. theorem OAI.PositiveEinsteinFour.Geometry.scalarChartOperator_affine line 2496
  117. theorem OAI.PositiveEinsteinFour.Geometry.scalarChart_eLpNorm_bound line 2528
  118. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_no_zero_inside_radial_barrier line 2617
  119. theorem OAI.PositiveEinsteinFour.Geometry.scalar_frame_gradient_sq_le_chart line 2692
  120. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_L2_weak_base_distribution line 2754
  121. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_L2_weak_coordinate_distribution line 2784
  122. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialChartFunction_eventually line 2851
  123. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialChartFunction_partial line 2859
  124. theorem OAI.PositiveEinsteinFour.Geometry.scalarRadialChartFunction_density_pos line 2879
  125. theorem OAI.PositiveEinsteinFour.Geometry.scalar_barrier_gradient_zero_at_first_order_contact line 2921
  126. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_no_zero_at_radial_contact line 2968
  127. def OAI.PositiveEinsteinFour.Geometry.scalarEnergyRoot line 3061
  128. def OAI.PositiveEinsteinFour.Geometry.scalarEnergyRootL2 line 3065
  129. theorem OAI.PositiveEinsteinFour.Geometry.scalarEnergyRootL2_norm_sq line 3069
  130. theorem OAI.PositiveEinsteinFour.Geometry.scalarEnergyRootL2_norm_le line 3094
  131. theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinate_gradient_abs_le line 3104
  132. theorem OAI.PositiveEinsteinFour.Geometry.scalarChart_norm_bound line 3119
  133. theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinate_gradient_memLp line 3132
  134. theorem OAI.PositiveEinsteinFour.Geometry.scalarChart_reverse_eLpNorm_bound line 3198
  135. theorem OAI.PositiveEinsteinFour.Geometry.scalar_euclidean_positive_contact_ball line 3285
  136. theorem OAI.PositiveEinsteinFour.Geometry.scalar_frame_gradient_abs_le_chart line 3342
  137. theorem OAI.PositiveEinsteinFour.Geometry.scalar_chart_gram_bounded line 3361
  138. theorem OAI.PositiveEinsteinFour.Geometry.scalar_radial_annulus_gradient_pos line 3403
  139. theorem OAI.PositiveEinsteinFour.Geometry.scalar_positive_annular_gradient_bound line 3420
  140. theorem OAI.PositiveEinsteinFour.Geometry.scalar_laplacian_uniform_upper line 3438
  141. theorem OAI.PositiveEinsteinFour.Geometry.frozenFrameLinearEquiv_symm_matrix line 3465
  142. def OAI.PositiveEinsteinFour.Geometry.scalarRescalingLinearEquiv line 3480
  143. theorem OAI.PositiveEinsteinFour.Geometry.scalarRescalingLinearEquiv_apply line 3488
  144. theorem OAI.PositiveEinsteinFour.Geometry.scalarRescalingLinearEquiv_symm_apply line 3495
  145. theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaling_inverse_affine line 3504
  146. def OAI.PositiveEinsteinFour.Geometry.smoothScalarH1Map line 3541
  147. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarH1Map_dense line 3548
  148. def OAI.PositiveEinsteinFour.Geometry.smoothScalarChartDerivative line 3557
  149. theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarChartDerivative_bound line 3597
  150. def OAI.PositiveEinsteinFour.Geometry.scalarH1ChartDerivative line 3641
  151. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1ChartDerivative_smooth line 3648
  152. theorem OAI.PositiveEinsteinFour.Geometry.scalarChart_ae_eq line 3685
  153. def OAI.PositiveEinsteinFour.Geometry.scalarChartValueLin line 3704
  154. theorem OAI.PositiveEinsteinFour.Geometry.scalarChartValueLin_bound line 3726
  155. def OAI.PositiveEinsteinFour.Geometry.scalarChartValue line 3736
  156. theorem OAI.PositiveEinsteinFour.Geometry.scalarChartValue_coe line 3743
  157. def OAI.PositiveEinsteinFour.Geometry.scalarH1ChartValue line 3750
  158. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1ChartValue_coe line 3757
  159. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1ChartValue_smooth line 3768
  160. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_continuous_no_zero_with_nearby_positive line 3804
  161. theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_product_integrable line 3914
  162. theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_integration_by_parts line 3926
  163. theorem OAI.PositiveEinsteinFour.Geometry.scalar_chart_integration_by_parts line 3955
  164. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_no_zero_with_nearby_positive line 3987
  165. def OAI.PositiveEinsteinFour.Geometry.scalarRescaledOperator line 4094
  166. theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledOperator_eq_zero_off_tsupport line 4100
  167. theorem OAI.PositiveEinsteinFour.Geometry.scalarContraction_smul line 4113
  168. theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaling_principal line 4118
  169. theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaling_drift line 4128
  170. theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledOperator_eq_chart line 4141
  171. def OAI.PositiveEinsteinFour.Geometry.scalarCompactTestL2 line 4185
  172. theorem OAI.PositiveEinsteinFour.Geometry.scalarCompactTestL2_coe line 4189
  173. def OAI.PositiveEinsteinFour.Geometry.scalarCompactDerivativeL2 line 4194
  174. theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_L2_pairing line 4202
  175. theorem OAI.PositiveEinsteinFour.Geometry.scalarChart_smooth_weak_derivative line 4215
  176. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Chart_weak_derivative line 4253
  177. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_continuous_strong_minimum line 4297
  178. def OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.constant line 4369
  179. theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.critical_estimate line 4371
  180. def OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.toL4 line 4379
  181. theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.toL4_coe line 4382
  182. def OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.toL4Linear line 4386
  183. theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.gradient_eLpNorm line 4404
  184. def OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.gradientL2 line 4412

    Source documentation

    The gradient in the existing Lebesgue measurable space of FourSpace.

    def gradientL2 (f : ↥(Euclidean.C1c (E := V))) : Lp V 2 (volume : Measure V) :=
…
  185. theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.toL4_bound line 4416
  186. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_strong_minimum line 4456
  187. theorem OAI.PositiveEinsteinFour.Geometry.scalarC1_differentiable_along_flow line 4527
  188. theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.fderiv_norm_le_sum_partial line 4572
  189. theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.continuous_partial line 4585
  190. def OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.partialL2 line 4589
  191. theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.partialL2_coe line 4594
  192. theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.gradientL2_norm_le_sum line 4597
  193. theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.toL4_bound_partials line 4629
  194. theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalL2_product_memLp line 4653
  195. def OAI.PositiveEinsteinFour.Geometry.scalarLocalL2Product line 4671
  196. theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalL2Product_coe line 4676
  197. theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalL2Product_integral line 4682
  198. theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalL2_mul_integrable line 4696
  199. def OAI.PositiveEinsteinFour.Geometry.h2Bump line 4723
  200. def OAI.PositiveEinsteinFour.Geometry.h2Cutoff line 4729
  201. theorem OAI.PositiveEinsteinFour.Geometry.h2Cutoff_smooth line 4732
  202. theorem OAI.PositiveEinsteinFour.Geometry.h2Cutoff_compact line 4737
  203. def OAI.PositiveEinsteinFour.Geometry.h2BumpDerivativeBound line 4740
  204. theorem OAI.PositiveEinsteinFour.Geometry.h2BumpDerivativeBound_nonneg line 4744
  205. theorem OAI.PositiveEinsteinFour.Geometry.h2Cutoff_derivative line 4747
  206. theorem OAI.PositiveEinsteinFour.Geometry.h2Cutoff_tendsto line 4779
  207. theorem OAI.PositiveEinsteinFour.Geometry.h2_operator_norm line 4787
  208. theorem OAI.PositiveEinsteinFour.Geometry.h2_cutoff_fderiv_bound line 4809
  209. theorem OAI.PositiveEinsteinFour.Geometry.h2_compact_critical line 4833
  210. theorem OAI.PositiveEinsteinFour.Geometry.h2_norm_sum_estimate line 4841
  211. theorem OAI.PositiveEinsteinFour.Geometry.h2_cutoff_L2_derivative line 4874
  212. theorem OAI.PositiveEinsteinFour.Geometry.h2_cutoff_L4_bound line 4887
  213. theorem OAI.PositiveEinsteinFour.Geometry.scalar_schwartz_L4_bound line 4898

    Source documentation

    A fixed inhomogeneous critical estimate for Schwartz functions.

    theorem scalar_schwartz_L4_bound (f : 𝓢(V, ℂ)) :
    eLpNorm f 4 volume ≤
      (ScalarEuclideanSobolev.constant : ℝ≥0∞) *
        (ENNReal.ofReal h2BumpDerivativeBound * eLpNorm f 2 volume +
          ∑ i : Fin 4, eLpNorm ((∂_{EuclideanSpace.basisFun (Fin 4) ℝ i} f : 𝓢(V, ℂ)) : V → ℂ) 2 volume) := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.constant, OAI.PositiveEinsteinFour.Geometry.h2BumpDerivativeBound

  214. theorem OAI.PositiveEinsteinFour.Geometry.h2_schwartz_eLpNorm line 4910
  215. theorem OAI.PositiveEinsteinFour.Geometry.h2_L2_injective line 4915
  216. def OAI.PositiveEinsteinFour.Geometry.h2SchwartzInverse line 4919
  217. theorem OAI.PositiveEinsteinFour.Geometry.h2SchwartzInverse_L2 line 4923
  218. theorem OAI.PositiveEinsteinFour.Geometry.h2SchwartzInverse_first line 4936
  219. theorem OAI.PositiveEinsteinFour.Geometry.h2SchwartzInverse_second line 4945
  220. theorem OAI.PositiveEinsteinFour.Geometry.scalar_H2_first_L4 line 4957

    Source documentation

    Every first derivative of an H2 distribution has an actual L4 representative.

    theorem scalar_H2_first_L4 (u : 𝓢'(V, ℂ)) (hu : MemSobolev 2 2 u) (i : Fin 4) :
    ∃ g : L2, (g : 𝓢'(V, ℂ)) = scalarCoordinateDerivative i u ∧
      MemLp (g : V → ℂ) 4 volume := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.scalarCoordinateDerivative

  221. theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselFirstL2_memLp_four line 5040
  222. def OAI.PositiveEinsteinFour.Geometry.besselFirstL4Linear line 5048
  223. theorem OAI.PositiveEinsteinFour.Geometry.besselFirstL4Linear_coe line 5070
  224. def OAI.PositiveEinsteinFour.Geometry.scalarBesselFirstL4 line 5076

    Source documentation

    The first derivative of the inverse Bessel operator is a continuous map from L2 to L4 in dimension four.

    def scalarBesselFirstL4 (i : Fin 4) : L2 →L[ℂ] L4 where
…
  225. theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselFirstL4_coe line 5091
  226. abbrev OAI.PositiveEinsteinFour.Geometry.scalarBorelLp line 5112
  227. def OAI.PositiveEinsteinFour.Geometry.scalarBorelLpEquivAux line 5118
  228. theorem OAI.PositiveEinsteinFour.Geometry.scalarBorelLpEquivAux_coe line 5128
  229. def OAI.PositiveEinsteinFour.Geometry.scalarBorelLpEquiv line 5139
  230. theorem OAI.PositiveEinsteinFour.Geometry.scalarBorelLpEquiv_coe line 5144
  231. theorem OAI.PositiveEinsteinFour.Geometry.scalarBorelLpEquivAux_ae line 5149
  232. theorem OAI.PositiveEinsteinFour.Geometry.scalarBorelLpEquiv_ae line 5168

    Source documentation

    Almost-everywhere representatives are unchanged by the transport.

    theorem scalarBorelLpEquiv_ae (F : Type*) [NormedAddCommGroup F] [NormedSpace ℝ F]
    (p : ℝ≥0∞) [Fact (1 ≤ p)] (u : Lp F p (volume : Measure FourSpace))
    (f : FourSpace → F) (hu : (u : FourSpace → F) =ᵐ[volume] f) :
    letI : MeasurableSpace FourSpace := borel FourSpace
…
  233. theorem OAI.PositiveEinsteinFour.Geometry.scalar_partial_product line 5194
  234. def OAI.PositiveEinsteinFour.Geometry.scalarLocalL2PartialProduct line 5202
  235. theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalL2PartialProduct_integral line 5212
  236. theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalL2_weak_product line 5220
  237. theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Chart_weak_derivative_integral line 5273