ScalarRegularity07.lean`

1280 declarations, 0 contain sorry, 0 declared as axioms

Real coordinate L² functions and their weak derivatives embed into the complex tempered distributions used by the elliptic inverse.

def OAI.PositiveEinsteinFour.Geometry.scalarComplexL2 line 97
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexL2_coe line 100
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexL2_pairing_re line 104
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexL2_pairing_im line 120
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartz_real_partial line 136
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexL2_weak_derivative line 146
def OAI.PositiveEinsteinFour.Geometry.scalarLocalL2Gradient line 178
theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalL2Gradient_pairing line 185
theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalL2_complex_derivative line 207
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Chart_cutoff_memSobolev_one line 231
theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoff_contDiff line 268
def OAI.PositiveEinsteinFour.Geometry.scalarCutoffSchwartz line 280
theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoffSchwartz_apply line 286
theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoffParameter_jets_uniform line 290
def OAI.PositiveEinsteinFour.Geometry.scalarCutoffPrincipal line 318
def OAI.PositiveEinsteinFour.Geometry.scalarCutoffDrift line 322
theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoffPrincipal_jets_uniform line 326
theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoffDrift_jets_uniform line 344
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzBesselInverse_first line 388
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzBesselInverse_second line 397
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzBesselInverse_first_four line 407

theorem OAI.PositiveEinsteinFour.Geometry.scalar_H2_schwartz_approximation line 419

Source documentation

Approximation of an H2 function controls values, first derivatives in both L2 and L4, and second derivatives in L2 along the same sequence.

theorem scalar_H2_schwartz_approximation (u : L2) (hu : MemSobolev 2 2 (u : T)) :
    ∃ (v : L2) (f : ℕ → S),
      u = scalarBesselInverseL2 v ∧
      Tendsto (fun n => (f n).toLp 2 volume) atTop (𝓝 u) ∧
      (∀ i, Tendsto (fun n => (D i (f n)).toLp 2 volume) atTop
        (𝓝 (scalarBesselFirstL2 i v))) ∧
      (∀ i, Tendsto (fun n => (D i (f n)).toLp 4 volume) atTop
        (𝓝 (scalarBesselFirstL4 i v))) ∧
      (∀ i j, Tendsto (fun n => (D i (D j (f n))).toLp 2 volume) atTop
        (𝓝 (scalarBesselSecondL2 i j v))) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarBesselInverseL2, OAI.PositiveEinsteinFour.Geometry.scalarBesselFirstL2, OAI.PositiveEinsteinFour.Geometry.scalarBesselFirstL4, OAI.PositiveEinsteinFour.Geometry.scalarBesselSecondL2

theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalL2Product_bound line 472
theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalL2Product_ae_congr line 499
def OAI.PositiveEinsteinFour.Geometry.scalarLocalL2ProductLinear line 513
def OAI.PositiveEinsteinFour.Geometry.scalarLocalL2ProductCLM line 538
theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalL2ProductCLM_coe line 546
def OAI.PositiveEinsteinFour.Geometry.scalarLinfL2Product line 572
theorem OAI.PositiveEinsteinFour.Geometry.scalarLinfL2Product_coe line 575
theorem OAI.PositiveEinsteinFour.Geometry.scalarLinfL2Product_tendsto line 579
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexL2_compact_weak_derivative line 604
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexL2_pairing_component line 643
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexSource_pairing_component line 657
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplex_partial line 690
theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoffSchwartz_first line 700
theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoffSchwartz_second line 710
theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoffSchwartz_jet_bounds line 728
def OAI.PositiveEinsteinFour.Geometry.densityCutoffL2 line 771
theorem OAI.PositiveEinsteinFour.Geometry.densityCutoffL2_distribution line 774
theorem OAI.PositiveEinsteinFour.Geometry.densityCutoffL2_coe line 780
theorem OAI.PositiveEinsteinFour.Geometry.densityCutoff_support line 787
theorem OAI.PositiveEinsteinFour.Geometry.scalar_H2_density_division line 794
def OAI.PositiveEinsteinFour.Geometry.halfSmoothBump line 849
def OAI.PositiveEinsteinFour.Geometry.halfSmoothCutoff line 855
theorem OAI.PositiveEinsteinFour.Geometry.halfSmoothCutoff_apply line 860
theorem OAI.PositiveEinsteinFour.Geometry.halfSmoothCutoff_support line 862
theorem OAI.PositiveEinsteinFour.Geometry.halfSmoothCutoff_one line 873
theorem OAI.PositiveEinsteinFour.Geometry.scalar_half_smooth_real_representative line 878
def OAI.PositiveEinsteinFour.Geometry.integerBesselSymbol line 918
theorem OAI.PositiveEinsteinFour.Geometry.integerBesselSymbol_temperate line 921
theorem OAI.PositiveEinsteinFour.Geometry.integerBesselSymbol_bound line 926
theorem OAI.PositiveEinsteinFour.Geometry.integerBesselSymbol_memLp line 933
def OAI.PositiveEinsteinFour.Geometry.scalarIntegerBesselInverse line 938
theorem OAI.PositiveEinsteinFour.Geometry.scalarIntegerBesselInverse_distribution line 941
theorem OAI.PositiveEinsteinFour.Geometry.scalarIntegerBesselInverse_memSobolev line 951
def OAI.PositiveEinsteinFour.Geometry.scalarSchwartzIntegerBesselInverse line 956
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzIntegerBesselInverse_distribution line 959
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzIntegerBesselInverse_toLp line 970
theorem OAI.PositiveEinsteinFour.Geometry.scalar_integer_Hn_schwartz_approximation line 979
def OAI.PositiveEinsteinFour.Geometry.localC1Bump line 1024
def OAI.PositiveEinsteinFour.Geometry.localC1Cutoff line 1030
theorem OAI.PositiveEinsteinFour.Geometry.localC1Cutoff_apply line 1035
theorem OAI.PositiveEinsteinFour.Geometry.localC1Cutoff_support line 1037
theorem OAI.PositiveEinsteinFour.Geometry.localC1Cutoff_one line 1048
theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_H4_C1_real_representative line 1053
def OAI.PositiveEinsteinFour.Geometry.localContinuousBump line 1102
def OAI.PositiveEinsteinFour.Geometry.localContinuousCutoff line 1108
theorem OAI.PositiveEinsteinFour.Geometry.localContinuousCutoff_apply line 1113
theorem OAI.PositiveEinsteinFour.Geometry.localContinuousCutoff_support line 1115
theorem OAI.PositiveEinsteinFour.Geometry.localContinuousCutoff_one line 1126
theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_H3_continuous_real_representative line 1131
theorem OAI.PositiveEinsteinFour.Geometry.scalar_localized_distribution_eq line 1175
def OAI.PositiveEinsteinFour.Geometry.scalarCutoffChartC1 line 1222
theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoffChart_partial line 1241
def OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffDerivative line 1265
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffDerivative_smooth line 1280
def OAI.PositiveEinsteinFour.Geometry.scalarCutoffChartL4 line 1316
theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoffChartL4_bound line 1322
def OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffL4 line 1345
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffL4_smooth line 1352
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffine_complex_integral line 1385
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffine_complex_memLp line 1394
def OAI.PositiveEinsteinFour.Geometry.scalarComplexAffinePullbackL2 line 1403
Source documentation
Pullback of the complex L2 representative by an invertible affine map.
```
def scalarComplexAffinePullbackL2 (A : V ≃L[ℝ] V) (q : V) (u : L2) : L2 :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexAffinePullbackL2_coe line 1406
def OAI.PositiveEinsteinFour.Geometry.scalarAffineTestCLM line 1411
Source documentation
Inverse affine coordinates on test functions.
```
def scalarAffineTestCLM (A : V ≃L[ℝ] V) (q : V) : S →L[ℂ] S :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineTestCLM_apply line 1415
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineTestCLM_derivative line 1418
def OAI.PositiveEinsteinFour.Geometry.scalarAffineDistribution line 1431
Source documentation
Distributional affine pullback, with its change-of-variables Jacobian.
```
def scalarAffineDistribution (A : V ≃L[ℝ] V) (q : V) : T →L[ℂ] T :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineDistribution_apply line 1435
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineDistribution_L2 line 1439
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineDistribution_derivative line 1456
Source documentation
The weak derivative is transformed by the actual linear part A.
```
theorem scalarAffineDistribution_derivative (A : V ≃L[ℝ] V) (q v : V) (u : T) :
    ∂_{v} (scalarAffineDistribution A q u) =
      scalarAffineDistribution A q (∂_{A v} u) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarAffineDistribution
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineDistribution_memSobolev_zero line 1463
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineDistribution_memSobolev_one line 1472
Source documentation
First-order Sobolev regularity is stable under an invertible affine change of coordinates, with no smoothness assumption on the L2 function.
```
theorem scalarAffineDistribution_memSobolev_one (A : V ≃L[ℝ] V) (q : V)
    (u : T) (hu : MemSobolev 1 2 u) :
    MemSobolev 1 2 (scalarAffineDistribution A q u) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarAffineDistribution
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexAffinePullbackL2_memSobolev_one line 1486
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexAffinePullbackL2_ofReal line 1492
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffinePullbackL2_memSobolev_one line 1511
Source documentation
The real L2 affine pullback has the same H1 regularity after the canonical complexification used by the distributional elliptic theory.
```
theorem scalarAffinePullbackL2_memSobolev_one (A : V ≃L[ℝ] V) (q : V)
    (u : Lp ℝ 2 (volume : Measure V))
    (hu : MemSobolev 1 2 (scalarComplexL2 u : T)) :
    MemSobolev 1 2 (scalarComplexL2 (scalarAffinePullbackL2 A q u) : T) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarComplexL2, OAI.PositiveEinsteinFour.Geometry.scalarAffinePullbackL2
theorem OAI.PositiveEinsteinFour.Geometry.scalar_direct_finite_algebra line 1539

theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzDirectOperator_coordinate line 1561

Source documentation

The normalization and identity-matrix correction recombine to the actual principal matrix and drift at the point x.

theorem scalarSchwartzDirectOperator_coordinate (P : Mat4) (B : Fin 4 → ℝ)
    (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S) (φ : S) (x : V)
    (ha : ∀ i j, a i j x =
      ((-((2 * Real.pi) ^ 2)⁻¹ * (P i j - (1 : Mat4) i j) : ℝ) : ℂ))
    (hb : ∀ i, b i x = ((-((2 * Real.pi) ^ 2)⁻¹ * B i : ℝ) : ℂ)) :
    scalarSchwartzDirectOperator a b φ x - φ x =
      (-Complex.ofReal (((2 * Real.pi) ^ 2)⁻¹)) *
        ((∑ i, ∑ j, (P i j : ℂ) * D i (D j φ) x) + ∑ i, (B i : ℂ) * D i φ x) := by
…

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

theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzDirectOperator_zero_off_tsupport line 1585
Source documentation
Every term of the test operator is supported in the original test support, regardless of the coefficient values outside it.
```
theorem scalarSchwartzDirectOperator_zero_off_tsupport
    (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S) (φ : S) (x : V)
    (hx : x ∉ tsupport (φ : V → ℂ)) :
    scalarSchwartzDirectOperator a b φ x - φ x = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarSchwartzDirectOperator
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartz_real_second_partial line 1612
theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_map_mul line 1622

theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzDirectOperator_real_coordinate line 1629

Source documentation

Any real-linear component, in particular real or imaginary part, recovers the ordinary real scalar principal/drift expression.

theorem scalarSchwartzDirectOperator_real_coordinate (L : ℂ →L[ℝ] ℝ)
    (P : Mat4) (B : Fin 4 → ℝ) (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S)
    (φ : S) (x : V)
    (ha : ∀ i j, a i j x =
      ((-((2 * Real.pi) ^ 2)⁻¹ * (P i j - (1 : Mat4) i j) : ℝ) : ℂ))
    (hb : ∀ i, b i x = ((-((2 * Real.pi) ^ 2)⁻¹ * B i : ℝ) : ℂ)) :
    L (scalarSchwartzDirectOperator a b φ x - φ x) =
      -((2 * Real.pi) ^ 2)⁻¹ *
        (scalarPrincipalContraction P (scalarPartialMatrix (L ∘ φ) x) +
          dotProduct B (scalarPartialVector (L ∘ φ) x)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.scalarSchwartzDirectOperator, OAI.PositiveEinsteinFour.Geometry.scalarPrincipalContraction, OAI.PositiveEinsteinFour.Geometry.scalarPartialMatrix, OAI.PositiveEinsteinFour.Geometry.scalarPartialVector

def OAI.PositiveEinsteinFour.Geometry.quarterC1Bump line 1678
def OAI.PositiveEinsteinFour.Geometry.quarterC1Cutoff line 1684
theorem OAI.PositiveEinsteinFour.Geometry.quarterC1Cutoff_apply line 1689
theorem OAI.PositiveEinsteinFour.Geometry.quarterC1Cutoff_support line 1691
theorem OAI.PositiveEinsteinFour.Geometry.quarterC1Cutoff_one line 1702
theorem OAI.PositiveEinsteinFour.Geometry.scalar_quarter_H4_C1_real_representative line 1707
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartz_re_derivative line 1761
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartz_re_toLp line 1770

theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_H2_approximation line 1780

Source documentation

A real H2 function has one smooth approximating sequence controlling all derivatives needed by the second-order nonlinear chain rule.

theorem scalar_real_H2_approximation (u : L2) (hu : MemSobolev 2 2 (scalarComplexL2 u : T)) :
    ∃ (f : ℕ → S) (G : Fin 4 → L2) (G4 : Fin 4 → L4) (H : Fin 4 → Fin 4 → L2),
      (∀ i, (G i : V → ℝ) =ᵐ[volume] G4 i) ∧
      Tendsto (fun n => (f n).toLp 2 volume) atTop (𝓝 u) ∧
      (∀ i, Tendsto (fun n => (D i (f n)).toLp 2 volume) atTop (𝓝 (G i))) ∧
      (∀ i, Tendsto (fun n => (D i (f n)).toLp 4 volume) atTop (𝓝 (G4 i))) ∧
      (∀ i j, Tendsto (fun n => (D i (D j (f n))).toLp 2 volume) atTop (𝓝 (H i j))) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarComplexL2

theorem OAI.PositiveEinsteinFour.Geometry.scalarDensityCutoff_smooth line 1845
def OAI.PositiveEinsteinFour.Geometry.scalarWeightedChartL2 line 1852
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedChartL2_memSobolev_one line 1863
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedChartL2_coe line 1875
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedChartL2_integral line 1900
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineDistribution_memSobolev_two line 1930
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexAffinePullbackL2_memSobolev_two line 1946
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineDistribution_memSobolev_integer line 1972
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexAffinePullbackL2_memSobolev_integer line 1991
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffinePullbackL2_memSobolev_integer line 1998
def OAI.PositiveEinsteinFour.Geometry.scalarChartSupport line 2025
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartSupport_compact line 2029
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartSupport_subset line 2035
def OAI.PositiveEinsteinFour.Geometry.scalarChartCutoff line 2041
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartCutoff_support line 2045
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartCutoff_smooth line 2060
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartCutoff_compact line 2076
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartCutoff_apply line 2083
structure OAI.PositiveEinsteinFour.Geometry.ScalarPartition line 2090
Source documentation
A finite set of chart centers with subordinate smooth weights.
```
structure ScalarPartition (M : Type*) [TopologicalSpace M] [ChartedSpace FourSpace M] where
…
```
abbrev OAI.PositiveEinsteinFour.Geometry.ScalarPartition.ι line 2097
instance OAI.PositiveEinsteinFour.Geometry.ScalarPartition.(instance at line 2099) line 2099
abbrev OAI.PositiveEinsteinFour.Geometry.ScalarPartition.center line 2101
abbrev OAI.PositiveEinsteinFour.Geometry.ScalarPartition.ρ line 2103
theorem OAI.PositiveEinsteinFour.Geometry.scalarPartition_exists line 2107
def OAI.PositiveEinsteinFour.Geometry.scalarPartitionFunction line 2123
theorem OAI.PositiveEinsteinFour.Geometry.scalarPartitionFunction_support line 2127
def OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.valueL2 line 2152
theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.valueL2_coe line 2156
def OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.coordinateL2 line 2160
Source documentation
Insert one scalar L² function in a Euclidean coordinate direction.
```
def coordinateL2 (i : Fin 4) :
    Lp ℝ 2 (volume : Measure FourSpace) →L[ℝ] Lp FourSpace 2 (volume : Measure FourSpace) :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.coordinateL2_coe line 2164
theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.grad_eq_sum_partial line 2169
theorem OAI.PositiveEinsteinFour.Geometry.ScalarEuclideanSobolev.gradientL2_eq_sum_partialL2 line 2186
def OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffValueL2 line 2214
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffValueL2_smooth line 2223

def OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffGradientL2 line 2242

Source documentation

Assemble the four bounded weak coordinate derivative maps into the ordinary Euclidean vector gradient.

def scalarH1CutoffGradientL2 (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) (c : M)
    {K : Set FourSpace} (hK : IsCompact K) (hKt : K ⊆ (chartAt FourSpace c).target)
    (χ : FourSpace → ℝ) (hχ : ContDiff ℝ ∞ χ) (hc : HasCompactSupport χ)
    (hs : tsupport χ ⊆ K) :
    scalarH1 d →L[ℝ] Lp FourSpace 2 (volume : Measure FourSpace) :=
…

theorem OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffGradientL2_smooth line 2251

def OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffJet line 2263

Source documentation

The compact chart localization of an intrinsic scalar H¹ first jet.

def scalarH1CutoffJet (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) (c : M)
    {K : Set FourSpace} (hK : IsCompact K) (hKt : K ⊆ (chartAt FourSpace c).target)
    (χ : FourSpace → ℝ) (hχ : ContDiff ℝ ∞ χ) (hc : HasCompactSupport χ)
    (hs : tsupport χ ⊆ K) :
    scalarH1 d →L[ℝ]
      (Lp ℝ 2 (volume : Measure FourSpace) × Lp FourSpace 2 (volume : Measure FourSpace)) :=
…

theorem OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffJet_smooth line 2273
theorem OAI.PositiveEinsteinFour.Geometry.scalarIntegerBesselInverse_three_memLp_top line 2307
def OAI.PositiveEinsteinFour.Geometry.besselThreeUniformLinear line 2313
theorem OAI.PositiveEinsteinFour.Geometry.besselThreeUniformLinear_coe line 2335
def OAI.PositiveEinsteinFour.Geometry.scalarBesselThreeUniform line 2340
Source documentation
Three inverse Bessel derivatives give a continuous map from L2 to L∞.
```
def scalarBesselThreeUniform : L2 →L[ℂ] Linf where
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselThreeUniform_coe line 2355
theorem OAI.PositiveEinsteinFour.Geometry.scalar_partial_scalar_comp line 2377
theorem OAI.PositiveEinsteinFour.Geometry.scalar_partial_smooth line 2384
theorem OAI.PositiveEinsteinFour.Geometry.scalar_partial_scalar_comp_second line 2388
theorem OAI.PositiveEinsteinFour.Geometry.scalar_partial_local_composition line 2404
theorem OAI.PositiveEinsteinFour.Geometry.scalar_partial_local_composition_second line 2415
theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_H2_approximation_ae line 2480
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartz_ofReal_derivative line 2520
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartz_ofReal_toLp line 2529
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartz_ofReal_weak_derivative line 2537

theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_H2_of_strong_jets line 2548

Source documentation

Actual first and second derivative limits of one smooth real sequence place its value limit in the real H2 Sobolev space.

theorem scalar_real_H2_of_strong_jets (f : ℕ → S) (u : L2)
    (g : Fin 4 → L2) (h : Fin 4 → Fin 4 → L2)
    (hf : Tendsto (fun n => (f n).toLp 2 volume) atTop (𝓝 u))
    (hg : ∀ i, Tendsto (fun n => (D i (f n)).toLp 2 volume) atTop (𝓝 (g i)))
    (hh : ∀ i j, Tendsto (fun n => (D i (D j (f n))).toLp 2 volume) atTop (𝓝 (h i j))) :
    MemSobolev 2 2 (scalarComplexL2 u : T) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarComplexL2

theorem OAI.PositiveEinsteinFour.Geometry.scalar_rescaled_ae_predicate line 2589
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledDrift_contDiffAt line 2625
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledPoint_compact_eventually line 2637
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledPoint_compact_target line 2658
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledSchwartz_small_compact line 2665
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledSchwartz_small line 2733
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartOperator_eq_zero_off_tsupport line 2769
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedChartL2_test_equation line 2780
def OAI.PositiveEinsteinFour.Geometry.twoFormCutoffC1 line 2848
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCutoffC1_partial line 2871
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCutoffC1_support line 2894
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_smooth line 2917
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_amplitude_partial line 2921
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_amplitude_second line 2930
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_amplitude_flat line 2944
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_amplitude_time line 2956
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_amplitude_residual line 2963

def OAI.PositiveEinsteinFour.Geometry.scalarCoordinateJet line 2998

Source documentation

A finite ordered coordinate derivative on tempered distributions.

def scalarCoordinateJet : List (Fin 4) → T →L[ℂ] T
  | [] => ContinuousLinearMap.id ℂ T
  | i :: is => (lineDerivOpCLM ℂ T (EuclideanSpace.basisFun (Fin 4) ℝ i)).comp
      (scalarCoordinateJet is)

theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinateJet_nil line 3003
theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinateJet_cons line 3005
theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinateJet_memSobolev line 3008
theorem OAI.PositiveEinsteinFour.Geometry.besselJet_exists line 3018
def OAI.PositiveEinsteinFour.Geometry.besselJetLinear line 3025
theorem OAI.PositiveEinsteinFour.Geometry.besselJetLinear_distribution line 3042
def OAI.PositiveEinsteinFour.Geometry.scalarBesselJetL2 line 3050
Source documentation
Every derivative of order at most n of the inverse n-th Bessel operator is continuous from L2 to L2.
```
def scalarBesselJetL2 (n : ℕ) (is : List (Fin 4)) (hle : is.length ≤ n) : L2 →L[ℂ] L2 where
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselJetL2_distribution line 3070
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselJetL2_memSobolev line 3076
def OAI.PositiveEinsteinFour.Geometry.scalarSchwartzCoordinateJet line 3082
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzCoordinateJet_distribution line 3087
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzBesselJet_toLp line 3098
theorem OAI.PositiveEinsteinFour.Geometry.scalarC1_weak_derivative line 3126
theorem OAI.PositiveEinsteinFour.Geometry.scalarC1_complex_derivative line 3139
def OAI.PositiveEinsteinFour.Geometry.scalarGradientCoordinateL2 line 3158
theorem OAI.PositiveEinsteinFour.Geometry.scalarGradientCoordinateL2_smooth line 3162
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffDerivative_distribution line 3198
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffDerivative_memLp_four line 3214
theorem OAI.PositiveEinsteinFour.Geometry.scalar_elliptic_cutoff_neighborhood line 3256
def OAI.PositiveEinsteinFour.Geometry.smoothScalarContinuous line 3313
def OAI.PositiveEinsteinFour.Geometry.smoothScalarBaseL4 line 3318
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarBaseL4_coe line 3322
def OAI.PositiveEinsteinFour.Geometry.smoothScalarProduct line 3327
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarPieceL4_bound line 3330
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalar_partition line 3387
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarBaseL4_bound line 3396
def OAI.PositiveEinsteinFour.Geometry.scalarH1BaseL4 line 3413
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BaseL4_smooth line 3418
def OAI.PositiveEinsteinFour.Geometry.scalarEllipticEstimateConstant line 3445
def OAI.PositiveEinsteinFour.Geometry.scalarEllipticSmallSize line 3448
theorem OAI.PositiveEinsteinFour.Geometry.scalarEllipticEstimateConstant_pos line 3450
theorem OAI.PositiveEinsteinFour.Geometry.scalarEllipticSmallSize_pos line 3454
theorem OAI.PositiveEinsteinFour.Geometry.scalarEllipticSmallSize_small line 3458
theorem OAI.PositiveEinsteinFour.Geometry.scalarScaledSchwartz_derivative line 3466
theorem OAI.PositiveEinsteinFour.Geometry.scalarScaledSchwartz_bound line 3470
theorem OAI.PositiveEinsteinFour.Geometry.scalar_rescaling_budget line 3476

theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledAdjointSchwartz_small line 3491

Source documentation

At every sufficiently small scale, the actual normalized principal coefficients and their actual adjoint drift obey one fixed inverse budget. The unexpanded drift b is retained for the exact adjoint test identity.

theorem scalarRescaledAdjointSchwartz_small (g : SmoothMetric M) (c : M)
    (z₀ : ChartTarget c) (χ : V → ℝ) (hχ : ContDiff ℝ ∞ χ)
    (hc : HasCompactSupport χ) :
    ∃ η : ℝ, 0 < η ∧ ∀ r : ℝ, |r| < η →
      ∃ (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S),
        (∀ i j y, a i j y =
          (-(((2 * Real.pi) ^ 2)⁻¹) : ℝ) •
            (scalarCutoffPrincipal g c z₀ χ r i j y : ℂ)) ∧
        (∀ i y, b i y =
          (-(((2 * Real.pi) ^ 2)⁻¹) : ℝ) •
            (scalarCutoffDrift g c z₀ χ r i y : ℂ)) ∧
        (∀ i j y, ‖a i j y‖ ≤ scalarEllipticSmallSize) ∧
…

Mentions: OAI.PositiveEinsteinFour.Geometry.ChartTarget, OAI.PositiveEinsteinFour.Geometry.scalarCutoffPrincipal, OAI.PositiveEinsteinFour.Geometry.scalarCutoffDrift, OAI.PositiveEinsteinFour.Geometry.scalarEllipticSmallSize

theorem OAI.PositiveEinsteinFour.Geometry.scalar_realPart_memSobolev_two line 3578
theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_H2_realization line 3594
def OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzMultiply line 3624
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzMultiply_coe line 3629
def OAI.PositiveEinsteinFour.Geometry.scalarLocalizedCompose line 3633
theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalizedCompose_apply line 3637
theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalizedCompose_valueLp line 3641
theorem OAI.PositiveEinsteinFour.Geometry.scalarPartition_subordinate_neighborhoods line 3673
theorem OAI.PositiveEinsteinFour.Geometry.scalarBorel_valueL2 line 3715
theorem OAI.PositiveEinsteinFour.Geometry.scalarBorel_gradientL2 line 3722
def OAI.PositiveEinsteinFour.Geometry.scalarH1BorelCutoffJet line 3742
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BorelCutoffJet_smooth line 3749
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BorelCutoffJet_mem line 3763
def OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffEuclideanH1 line 3776
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffEuclideanH1_supported line 3781
def OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffSupportedH1 line 3804
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffValueL2_compact line 3810
Source documentation
Compactness of a fixed chart cutoff, in the original Lebesgue L² space.
```
theorem scalarH1CutoffValueL2_compact :
    IsCompactOperator (scalarH1CutoffValueL2 g o d c hK hKt χ hχ hc hs) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffValueL2
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffineL2_integral line 3840
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaled_test_equation line 3856
theorem OAI.PositiveEinsteinFour.Geometry.scalar_partial_second_product_at line 3953
theorem OAI.PositiveEinsteinFour.Geometry.scalar_H2_unscale line 4000
theorem OAI.PositiveEinsteinFour.Geometry.scalar_integer_unscale line 4044
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedChartL2_L2_test_equation line 4092
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCutoffC1_control line 4158
def OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator line 4228
def OAI.PositiveEinsteinFour.Geometry.fourHeatConjugatedOperator line 4233
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_gaussian line 4241
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_residual line 4271
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_slice_partial line 4300
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_slice_partial_contDiffAt line 4311
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_slice_partial_continuousAt line 4320
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_slice_second_continuousAt line 4329
def OAI.PositiveEinsteinFour.Geometry.fourHeatRadialPrimitive line 4353
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialPrimitive_hasDerivAt line 4356
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialPrimitive_transport line 4375
def OAI.PositiveEinsteinFour.Geometry.jetL2 line 4408
theorem OAI.PositiveEinsteinFour.Geometry.jetL2_memLp_top line 4410
def OAI.PositiveEinsteinFour.Geometry.jetUniformLinear line 4419
theorem OAI.PositiveEinsteinFour.Geometry.jetUniformLinear_coe line 4441
def OAI.PositiveEinsteinFour.Geometry.scalarBesselJetUniform line 4446
Source documentation
Jets leaving at least three Sobolev derivatives are continuous in L∞.
```
def scalarBesselJetUniform : L2 →L[ℂ] Linf where
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselJetUniform_coe line 4461
def OAI.PositiveEinsteinFour.Geometry.scalarChartReconstructionFun line 4491
theorem OAI.PositiveEinsteinFour.Geometry.reconstruction_set_measurable line 4495
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartReconstructionFun_chart line 4502
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartReconstructionFun_add line 4512
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartReconstructionFun_smul line 4523
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartReconstructionFun_stronglyMeasurable line 4533
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartReconstruction_eLpNorm_bound line 4556
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartReconstructionFun_ae line 4579
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartReconstruction_memLp line 4599
def OAI.PositiveEinsteinFour.Geometry.scalarChartReconstructionLp line 4607
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartReconstructionLp_coe line 4612
def OAI.PositiveEinsteinFour.Geometry.scalarChartReconstructionLinear line 4618
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartReconstructionLinear_bound line 4643

def OAI.PositiveEinsteinFour.Geometry.scalarChartReconstruction line 4656

Source documentation

Reconstruction through a compact coordinate set, in actual base volume.

def scalarChartReconstruction (g : SmoothMetric M) (c : M)
    {K : Set FourSpace} (hK : IsCompact K) (hKt : K ⊆ (chartAt FourSpace c).target) :
    Lp ℝ 2 (volume : Measure FourSpace) →L[ℝ] Lp ℝ 2 (normalizedVolume g) :=
…

Mentions: OAI.PositiveEinsteinFour.Geometry.normalizedVolume

theorem OAI.PositiveEinsteinFour.Geometry.scalarChartReconstruction_coe line 4662
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartReconstruction_chartCutoff line 4668
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1CutoffValue_H2_of_rep line 4733
theorem OAI.PositiveEinsteinFour.Geometry.scalarEuclidean_rescaled_equation line 4779
theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinateJet_append line 4855
theorem OAI.PositiveEinsteinFour.Geometry.scalar_memSobolev_of_coordinate_jets line 4863
Source documentation
Only the finitely many coordinate derivatives through order n are needed.
```
theorem scalar_memSobolev_of_coordinate_jets (n : ℕ) (u : T)
    (hj : ∀ is : List (Fin 4), is.length ≤ n → ∃ v : L2, scalarCoordinateJet is u = (v : T)) :
    MemSobolev (n : ℝ) 2 u := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarCoordinateJet

theorem OAI.PositiveEinsteinFour.Geometry.scalar_integer_jets_closed line 4881

Source documentation

Strong L2 limits of every finite jet remain the actual derivatives of the value limit and yield integer Sobolev regularity.

theorem scalar_integer_jets_closed (n : ℕ) (u : L2) (fs : ℕ → L2)
    (G : List (Fin 4) → L2) (Gs : List (Fin 4) → ℕ → L2)
    (hvalue : Tendsto fs atTop (𝓝 u))
    (hG : ∀ is, is.length ≤ n → Tendsto (Gs is) atTop (𝓝 (G is)))
    (hjets : ∀ is, is.length ≤ n → ∀ k,
      scalarCoordinateJet is (fs k : T) = (Gs is k : T)) :
    MemSobolev (n : ℝ) 2 (u : T) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarCoordinateJet

def OAI.PositiveEinsteinFour.Geometry.scalarCoefficientBump line 4917
theorem OAI.PositiveEinsteinFour.Geometry.scalarCoefficientBump_one line 4923
theorem OAI.PositiveEinsteinFour.Geometry.exists_scalar_chart_cutoff line 4929
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzDerivative_apply line 4979
def OAI.PositiveEinsteinFour.Geometry.scalarDerivativeMultiplier line 4984
theorem OAI.PositiveEinsteinFour.Geometry.scalarDerivativeMultiplier_coe line 4990
theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalizedCompose_first_L2 line 4996
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaled_L2_test_equation line 5046
def OAI.PositiveEinsteinFour.Geometry.scalarRescaledSource line 5147
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledPoint_contDiff line 5152
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledSource_contDiffAt line 5159
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledSource_complex_contDiffAt line 5171
def OAI.PositiveEinsteinFour.Geometry.scalarL4ToL2Linear line 5197
theorem OAI.PositiveEinsteinFour.Geometry.scalarL4ToL2Linear_bound line 5220
def OAI.PositiveEinsteinFour.Geometry.scalarL4ToL2 line 5229
theorem OAI.PositiveEinsteinFour.Geometry.scalarL4ToL2_coe line 5234
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BaseL4_toL2 line 5249
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BaseL4_coe line 5268
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCutoff_jet_bound line 5296
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFrameValue_mul line 5347
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartValue_mul line 5351
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.mul line 5361
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormProduct line 5370
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormProduct_add line 5373
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormProduct_smul line 5379
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_partition line 5389
def OAI.PositiveEinsteinFour.Geometry.fourHeatEikonalDefect line 5415
def OAI.PositiveEinsteinFour.Geometry.fourHeatRadialTransport line 5418
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatConjugatedOperator_decomposition line 5424
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_transport_residual line 5435
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatEikonalDefect_zero line 5446
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_rescaled line 5482
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatScalarChart_residual line 5494
theorem OAI.PositiveEinsteinFour.Geometry.schwartz_L4_coefficient line 5535
theorem OAI.PositiveEinsteinFour.Geometry.schwartz_eLpNorm_two line 5545
def OAI.PositiveEinsteinFour.Geometry.l4JetL2 line 5552
def OAI.PositiveEinsteinFour.Geometry.l4NextJetL2 line 5554
def OAI.PositiveEinsteinFour.Geometry.l4JetBound line 5557
theorem OAI.PositiveEinsteinFour.Geometry.l4JetBound_lt_top line 5562
theorem OAI.PositiveEinsteinFour.Geometry.schwartz_jet_L4_bound line 5569
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselJetL2_memLp_four line 5595
Source documentation
The critical four-dimensional estimate applies to each actual derivative with at least one derivative remaining.
```
theorem scalarBesselJetL2_memLp_four (f : L2) :
    MemLp (scalarBesselJetL2 n is (by omega) f : V → ℂ) 4 volume := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarBesselJetL2
def OAI.PositiveEinsteinFour.Geometry.jetL4Linear line 5624
theorem OAI.PositiveEinsteinFour.Geometry.jetL4Linear_coe line 5646
def OAI.PositiveEinsteinFour.Geometry.scalarBesselJetL4 line 5650
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselJetL4_coe line 5665
theorem OAI.PositiveEinsteinFour.Geometry.scalar_chart_C1_unweight line 5690
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartValue_memLp_four line 5765
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1ChartValue_memLp_four line 5792
theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalL2Product_memLp_four line 5800
theorem OAI.PositiveEinsteinFour.Geometry.scalar_chart_continuous_unweight line 5842
theorem OAI.PositiveEinsteinFour.Geometry.scalarDerivativeMultiplier_tendsto line 5915
theorem OAI.PositiveEinsteinFour.Geometry.scalar_euclidean_continuous_unweight line 5953
def OAI.PositiveEinsteinFour.Geometry.scalarH1LocalizedCoordinate line 6032
Source documentation
The localized weak coordinate derivative, reconstructed in the base volume.
```
def scalarH1LocalizedCoordinate (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) (c : M)
    (ρ : SmoothScalar (M := M)) (hs : tsupport ρ.val ⊆ (chartAt FourSpace c).source)
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.SmoothScalar
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1LocalizedCoordinate_smooth line 6044
def OAI.PositiveEinsteinFour.Geometry.scalarH1LocalizedFrame line 6091
Source documentation
Actual frame gradient multiplied by a smooth base cutoff.
```
def scalarH1LocalizedFrame (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o))
    (ρ : SmoothScalar (M := M)) {B : ℝ} (hB : ∀ x, |ρ.val x| ≤ B) (i : Fin 4) :
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.SmoothScalar
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1LocalizedFrame_smooth line 6099
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzSecond_apply line 6137
theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalizedCompose_second_L2 line 6144
theorem OAI.PositiveEinsteinFour.Geometry.scalar_normalized_adjoint_test_equation line 6219
theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_L2_test_integrable line 6299
theorem OAI.PositiveEinsteinFour.Geometry.scalar_normalized_adjoint_test_equation_of_integrable line 6304
def OAI.PositiveEinsteinFour.Geometry.scalarH1ReconstructedPiece line 6394
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1ReconstructedPiece_smooth line 6405
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1ReconstructedPiece_compact line 6414
def OAI.PositiveEinsteinFour.Geometry.smoothScalarBaseL2Linear line 6425
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue_partition line 6429
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue_compact line 6447
Source documentation
The actual inclusion of scalar H¹ into base L² is compact.
```
theorem scalarH1BaseValue_compact (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) :
    IsCompactOperator (scalarH1BaseValue g o d) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue
def OAI.PositiveEinsteinFour.Geometry.scalarChartSourceL2 line 6478
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartSourceL2_coe line 6487
def OAI.PositiveEinsteinFour.Geometry.scalarRescaledSourceL2 line 6495
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledSourceL2_coe line 6504
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledSourceL2_pairing line 6530
theorem OAI.PositiveEinsteinFour.Geometry.scalar_chart_smooth_unweight line 6569
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_moment_le line 6641
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_moment_tendsto_zero line 6662
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCutoffJet line 6716
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCutoffJet_bound line 6722
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCutoffJetCLM line 6736
def OAI.PositiveEinsteinFour.Geometry.twoFormCutoffJet line 6741
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCutoffJet_smooth line 6745
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCutoffJet_mem line 6751
def OAI.PositiveEinsteinFour.Geometry.twoFormCutoffEuclideanH1 line 6762
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCutoffEuclideanH1_supported line 6767
def OAI.PositiveEinsteinFour.Geometry.twoFormCutoffSupportedH1 line 6785
def OAI.PositiveEinsteinFour.Geometry.twoFormCutoffValueL2 line 6790
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCutoffValueL2_compact line 6794
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCutoffValueL2_smooth line 6799
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_product_inner line 6828
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoForm_partition_weights line 6846
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2_eq_of_smooth_pairings line 6854
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_amplitude_partial_at line 6880
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_amplitude_second_at line 6889
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_gaussian_at line 6902
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_transport_residual_at line 6932
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_radial_derivative line 6965
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialTransport_of_radial line 6976
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_radial_divergence line 6993
abbrev OAI.PositiveEinsteinFour.Geometry.heatNormalMetric line 7046
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_symm line 7050
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_row line 7055
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_gauss_vector line 7073
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_radial line 7099
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_inverse_radial line 7112
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_eikonal line 7124
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarContinuous_dense line 7154
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarBaseL2_dense line 7169
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue_dense line 7180
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_local_frame_control line 7210
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexL2_real_smul line 7292
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexL2_real_smul_distribution line 7300
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartSourceL2_memSobolev_one line 7312
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledSourceL2_memSobolev_one line 7326
theorem OAI.PositiveEinsteinFour.Geometry.scalar_localized_H2_composition line 7366
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzBesselJet_toLp_four line 7442
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzBesselJet_toLp_top line 7453

theorem OAI.PositiveEinsteinFour.Geometry.scalar_integer_smooth_approximation line 7469

Source documentation

Density holds simultaneously for every required derivative of the same smooth sequence, including almost-everywhere convergence of its values.

theorem scalar_integer_smooth_approximation (n : ℕ) (u : L2)
    (hu : MemSobolev (n : ℝ) 2 (u : T)) :
    ∃ (v : L2) (fs : ℕ → S), u = scalarIntegerBesselInverse n v ∧
      (∀ᵐ x ∂(volume : Measure V), Tendsto (fun k => fs k x) atTop (𝓝 (u x))) ∧
      Tendsto (fun k => (fs k).toLp 2 volume) atTop (𝓝 u) ∧
      (∀ is hle, Tendsto (fun k => (scalarSchwartzCoordinateJet is (fs k)).toLp 2 volume)
        atTop (𝓝 (scalarBesselJetL2 n is hle v))) ∧
      (∀ is h1, Tendsto (fun k => (scalarSchwartzCoordinateJet is (fs k)).toLp 4 volume)
        atTop (𝓝 (scalarBesselJetL4 n is h1 v))) ∧
      (∀ is h3, Tendsto (fun k => (scalarSchwartzCoordinateJet is (fs k)).toLp ∞ volume)
        atTop (𝓝 (scalarBesselJetUniform n is h3 v))) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarIntegerBesselInverse, OAI.PositiveEinsteinFour.Geometry.scalarSchwartzCoordinateJet, OAI.PositiveEinsteinFour.Geometry.scalarBesselJetL2, OAI.PositiveEinsteinFour.Geometry.scalarBesselJetL4, OAI.PositiveEinsteinFour.Geometry.scalarBesselJetUniform

theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_weighted_H2 line 7529
theorem OAI.PositiveEinsteinFour.Geometry.scalar_rescaled_solution_smooth line 7648
def OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzProduct line 7718
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzProduct_apply line 7720
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzProduct_first line 7724
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzProduct_second line 7735
theorem OAI.PositiveEinsteinFour.Geometry.realSchwartz_toLp_add line 7756
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzProduct_L2_top line 7760
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzProduct_L2_four line 7769
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzProduct_first_L2 line 7778
theorem OAI.PositiveEinsteinFour.Geometry.realSchwartz_toLp_four_add line 7791
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzProduct_second_L2 line 7796
def OAI.PositiveEinsteinFour.Geometry.scalarL4ToLpLinear line 7841
theorem OAI.PositiveEinsteinFour.Geometry.scalarL4ToLpLinear_coe line 7848
theorem OAI.PositiveEinsteinFour.Geometry.scalarL4ToLpLinear_bound line 7852
def OAI.PositiveEinsteinFour.Geometry.scalarL4ToLp line 7858
theorem OAI.PositiveEinsteinFour.Geometry.scalarL4ToLp_coe line 7864
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_moment_filter_tendsto_zero line 7868
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_eLpNorm_tendsto_zero line 7892
def OAI.PositiveEinsteinFour.Geometry.scalarH1BaseLp line 7934
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BaseLp_coe line 7940
def OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffWeight line 7967
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffWeight_smooth line 7971
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffWeight_support line 7979
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffWeight_compact line 7984
def OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffC1 line 7988
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffC1_apply line 7999
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffC1_value line 8010
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffC1_support line 8022
def OAI.PositiveEinsteinFour.Geometry.twoFormLocalValueL2 line 8054
theorem OAI.PositiveEinsteinFour.Geometry.twoFormLocalValueL2_compact line 8062
theorem OAI.PositiveEinsteinFour.Geometry.twoFormLocalValueL2_smooth line 8070
def OAI.PositiveEinsteinFour.Geometry.twoFormReconstructedValue line 8081
theorem OAI.PositiveEinsteinFour.Geometry.twoFormReconstructedValue_compact line 8091
theorem OAI.PositiveEinsteinFour.Geometry.twoFormReconstructedValue_smooth_coe line 8101
abbrev OAI.PositiveEinsteinFour.Geometry.HeatMat6 line 8157
def OAI.PositiveEinsteinFour.Geometry.fourHeatBundleFirst line 8159
def OAI.PositiveEinsteinFour.Geometry.fourHeatBundleZero line 8163
def OAI.PositiveEinsteinFour.Geometry.fourHeatBundleOperator line 8166
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleFirst_gaussian line 8172
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleZero_gaussian line 8193
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleOperator_transport_residual_at line 8203
def OAI.PositiveEinsteinFour.Geometry.fourHeatDensityDrift line 8238
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatDensityDrift_radial line 8243
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_normalized_amplitude_radial line 8265
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatDensity_leading_transport line 8288
def OAI.PositiveEinsteinFour.Geometry.fourHeatOneFirst line 8318
def OAI.PositiveEinsteinFour.Geometry.fourHeatOneZero line 8322
def OAI.PositiveEinsteinFour.Geometry.fourHeatOneOperator line 8325
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneFirst_gaussian line 8331
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneZero_gaussian line 8352
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneOperator_transport_residual_at line 8362
def OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverage line 8398
def OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverageDerivative line 8401
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverage_integrand_derivative line 8405
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverageDerivative_continuous line 8420
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverageDerivative_bound line 8427
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverage_hasFDerivAt line 8453
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_pairing line 8501
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_posDef line 8517
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_det_of_chart_unit line 8536
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_eventually_nondegenerate line 8566
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_eikonal_neighborhood line 8592
def OAI.PositiveEinsteinFour.Geometry.scalarBaseShiftedSolution line 8626
def OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent line 8629
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseShiftedSolution_weak line 8632
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_compact line 8636
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_symmetric line 8639
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_energy line 8646
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseShiftedSolution_injective line 8653
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_injective line 8663
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_pos line 8670
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffinePullbackL2_smul line 8693
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartSourceL2_baseValue line 8718
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedChartL2_smul line 8725
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledEigenSource line 8736
theorem OAI.PositiveEinsteinFour.Geometry.scalarEuclidean_local_H3 line 8771
theorem OAI.PositiveEinsteinFour.Geometry.scalarEuclidean_local_integer line 8878
theorem OAI.PositiveEinsteinFour.Geometry.scalarEuclidean_local_H2 line 8985
theorem OAI.PositiveEinsteinFour.Geometry.scalar_localized_H2_positive_power line 9073
theorem OAI.PositiveEinsteinFour.Geometry.scalarL2_memLp_four_of_domination line 9114
theorem OAI.PositiveEinsteinFour.Geometry.scalarChartReconstruction_memLp_four line 9139
theorem OAI.PositiveEinsteinFour.Geometry.scalarBasePullback_memLp_four line 9161
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1LocalizedFrame_memLp_four line 9170
theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_weighted_H3 line 9212
theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_weighted_smooth line 9347
def OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzJet line 9450
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzJet_re line 9455

theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_integer_approximation line 9468

Source documentation

One real sequence controls all finite jets, with L4 and uniform control at the Sobolev orders used in products.

theorem scalar_real_integer_approximation (n : ℕ) (u : L2)
    (hu : MemSobolev (n : ℝ) 2 (scalarComplexL2 u : T)) :
    ∃ (fs : ℕ → S) (G : List (Fin 4) → L2)
      (G4 : List (Fin 4) → L4) (Gtop : List (Fin 4) → Linf),
      (∀ᵐ x ∂(volume : Measure V), Tendsto (fun k => fs k x) atTop (𝓝 (u x))) ∧
      Tendsto (fun k => (fs k).toLp 2 volume) atTop (𝓝 u) ∧
      (∀ is, is.length ≤ n → Tendsto (fun k => (scalarRealSchwartzJet is (fs k)).toLp 2 volume)
        atTop (𝓝 (G is))) ∧
      (∀ is, is.length + 1 ≤ n → Tendsto (fun k => (scalarRealSchwartzJet is (fs k)).toLp 4 volume)
        atTop (𝓝 (G4 is))) ∧
      (∀ is, is.length + 3 ≤ n → Tendsto (fun k => (scalarRealSchwartzJet is (fs k)).toLp ∞ volume)
        atTop (𝓝 (Gtop is))) ∧
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarComplexL2, OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzJet

theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_cauchy_of_L2 line 9555

theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_subcritical_subsequence line 9601

Source documentation

Every bounded intrinsic H¹ sequence has a strongly convergent actual base Lp subsequence for 2 < p < 4.

theorem scalarH1_subcritical_subsequence (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) {p : ℝ}
    [Fact (1 ≤ ENNReal.ofReal p)] (hp : 2 < p) (hp4 : p < 4)
    (u : ℕ → scalarH1 d) {R : ℝ} (hu : ∀ n, ‖u n‖ ≤ R) :
    ∃ v : Lp ℝ (ENNReal.ofReal p) (normalizedVolume g),
      ∃ φ : ℕ → ℕ, StrictMono φ ∧
        Tendsto (fun n => scalarH1BaseLp g o d (ENNReal.ofReal p)
          (by exact_mod_cast hp4.le) (u (φ n))) atTop (𝓝 v) := by
…

theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.gramTensor_contDiffAt line 9650
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.chartValue_contDiffAt line 9661
theorem OAI.PositiveEinsteinFour.Geometry.TwoFormSmooth.gramCovariantDirection line 9672
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffC1_partial line 9700
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoff_covariant line 9728
def OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffJet line 9774
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffJet_smooth line 9785
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffJet_mem line 9795
def OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffH1 line 9808
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCutoffH1_supported line 9816
def OAI.PositiveEinsteinFour.Geometry.fourHeatConnectionFirst line 9853
def OAI.PositiveEinsteinFour.Geometry.fourHeatConnectionZero line 9856
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatConnectionFirst_radial line 9862
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatConnectionFirst_contDiffAt line 9882
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatConnectionZero_contDiffAt line 9891
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_cutoff line 9932
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleOperator_joint_continuousAt line 9991
def OAI.PositiveEinsteinFour.Geometry.fourHeatOneConnectionFirst line 10046
def OAI.PositiveEinsteinFour.Geometry.fourHeatOneConnectionZero line 10049
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneConnectionFirst_radial line 10055
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneConnectionFirst_contDiffAt line 10075
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneConnectionZero_contDiffAt line 10084
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneOperator_joint_continuousAt line 10125
theorem OAI.PositiveEinsteinFour.Geometry.fourLinearForm_expansion line 10185
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverage_partial line 10200
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverage_fderiv line 10212
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverage_contDiff line 10223
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverage_smooth line 10252
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverage_zero line 10273
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverage_transport line 10281
theorem OAI.PositiveEinsteinFour.Geometry.heatCompatibleDrift_algebra line 10340
theorem OAI.PositiveEinsteinFour.Geometry.heatCompatibleMetric_drift line 10365
def OAI.PositiveEinsteinFour.Geometry.heatFamilyScaleLinear line 10415
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScaleLinear_apply line 10419
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScaleLinear_continuous line 10422
def OAI.PositiveEinsteinFour.Geometry.heatFamilyRadialAverage line 10427
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyRadialAverage_slice line 10431
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyRadialAverage_continuous line 10435
def OAI.PositiveEinsteinFour.Geometry.heatFamilyRadialDerivative line 10443
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyRadialDerivative_continuous line 10447
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyRadialAverage_hasFDerivAt line 10455
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyRadialAverage_fderiv_apply line 10484
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_zero line 10536
theorem OAI.PositiveEinsteinFour.Geometry.frameExponentialJacobian_zero line 10562
theorem OAI.PositiveEinsteinFour.Geometry.frameExponentialJacobian_eventually_pos line 10567
def OAI.PositiveEinsteinFour.Geometry.heatNormalLeadingAmplitude line 10575
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalLeadingAmplitude_zero line 10579
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalLeadingAmplitude_continuousAt line 10583
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalLeadingAmplitude_normalization line 10590
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalLeadingAmplitude_neighborhood line 10597
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_inner_base line 10635
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_norm_le line 10644
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_eigenvalue line 10657
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_eigenvector_weak line 10671
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_cutoff_coordinate_memLp_four line 10726
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1LocalizedCoordinate_memLp_four_of_H2 line 10755
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexL2_scaled_pairing line 10795
def OAI.PositiveEinsteinFour.Geometry.scalarEigenCutoff line 10803
theorem OAI.PositiveEinsteinFour.Geometry.scalarEigenCutoff_on_ball line 10807
theorem OAI.PositiveEinsteinFour.Geometry.scalar_eigen_source_pairing line 10812
theorem OAI.PositiveEinsteinFour.Geometry.scalarPartitionFunction_abs_le_one line 10841
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1Gradient_memLp_four_of_partition line 10853

theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_H2_H3_product line 10911

Source documentation

No pointwise differentiability of either factor is assumed.

theorem scalar_real_H2_H3_product (u v : L2)
    (hu : MemSobolev 2 2 (scalarComplexL2 u : T))
    (hv : MemSobolev 3 2 (scalarComplexL2 v : T)) :
    ∃ w : L2, MemSobolev 2 2 (scalarComplexL2 w : T) ∧
      (w : V → ℝ) =ᵐ[volume] fun x => u x * v x := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarComplexL2

theorem OAI.PositiveEinsteinFour.Geometry.scalar_localized_H2_subcritical_source line 10974
theorem OAI.PositiveEinsteinFour.Geometry.scalar_half_ball_cutoff_of_compact line 11014
theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_H2_power_source line 11046
theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_chart_smooth line 11103
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzJet_ofReal line 11179
theorem OAI.PositiveEinsteinFour.Geometry.scalarRealSchwartzJet_weak line 11190
theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_jet_limit line 11197
theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_derivative_sobolev line 11220
theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_integer_jets_closed line 11234
def OAI.PositiveEinsteinFour.Geometry.scalarWeightedBaseLp line 11279
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedBaseLp_coe line 11285
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeighted_subcritical_subsequence line 11292
def OAI.PositiveEinsteinFour.Geometry.twoFormGramValueL2 line 11333
def OAI.PositiveEinsteinFour.Geometry.twoFormGramGradientL2 line 11338
def OAI.PositiveEinsteinFour.Geometry.twoFormGramPartialL2 line 11343
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramValueL2_smooth line 11347
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramGradientL2_smooth line 11358
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramPartialL2_smooth line 11369
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGram_complex_derivative line 11376
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGram_memSobolev_one line 11403
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_supported_gramTest line 11436
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleOperator_cutoff line 11511
def OAI.PositiveEinsteinFour.Geometry.fourHeatWeightedRadialAverage line 11560
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatWeightedRadialAverage_contDiff line 11563
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialTransport_product line 11569
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatWeightedRadialAverage_transport line 11582
abbrev OAI.PositiveEinsteinFour.Geometry.heatFamilyBasis line 11629
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyLinearForm_expansion line 11631
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyRadialAverage_preserves_contDiff line 11645
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_chart_pairing line 11702
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalMetric_smoothAt_zero line 11731
theorem OAI.PositiveEinsteinFour.Geometry.frameExponentialJacobian_smoothAt_zero line 11772
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalLeadingAmplitude_smoothAt_zero line 11783
def OAI.PositiveEinsteinFour.Geometry.heatPullbackMetric line 11812
def OAI.PositiveEinsteinFour.Geometry.heatPullbackConnection line 11816
theorem OAI.PositiveEinsteinFour.Geometry.heatPullbackConnection_torsion line 11821
theorem OAI.PositiveEinsteinFour.Geometry.heatPullbackMetric_regular line 11834
theorem OAI.PositiveEinsteinFour.Geometry.heatPullbackConnection_compatible line 11849
abbrev OAI.PositiveEinsteinFour.Geometry.ScalarBaseSpectralValue line 11905
abbrev OAI.PositiveEinsteinFour.Geometry.ScalarBaseSpectralSpace line 11907
instance OAI.PositiveEinsteinFour.Geometry.scalarBaseSpectralSpaceFinite line 11910
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseSpectral_total line 11916
abbrev OAI.PositiveEinsteinFour.Geometry.ScalarBaseEigenIndex line 11926
def OAI.PositiveEinsteinFour.Geometry.scalarBaseEigenvector line 11929
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseEigenvector_orthonormal line 11932
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseEigenvector_span line 11936
def OAI.PositiveEinsteinFour.Geometry.scalarBaseEigenbasis line 11958
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseEigenvector_hasEigenvector line 11963
theorem OAI.PositiveEinsteinFour.Geometry.scalarAffinePullbackL2_sub line 11989
theorem OAI.PositiveEinsteinFour.Geometry.scalarComplexL2_sub_distribution line 12005
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedChartL2_sub line 12025
theorem OAI.PositiveEinsteinFour.Geometry.scalarRescaledDifferenceSource line 12037
theorem OAI.PositiveEinsteinFour.Geometry.scalar_eigen_local_all_orders line 12075
theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_H2_nonlinear_source line 12211
theorem OAI.PositiveEinsteinFour.Geometry.scalar_weak_poisson_smooth_representative line 12313
theorem OAI.PositiveEinsteinFour.Geometry.actual_petersen_poisson line 12350
theorem OAI.PositiveEinsteinFour.Geometry.scalar_realPart_memSobolev_integer line 12383
theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_integer_realization line 12396
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedBaseLp_smooth line 12434
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedBaseLp_ne_zero line 12444

theorem OAI.PositiveEinsteinFour.Geometry.scalarWeighted_subcritical_extremal line 12456

Source documentation

The actual subcritical Sobolev operator attains its norm.

theorem scalarWeighted_subcritical_extremal (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) {p : ℝ}
    [Fact (1 ≤ ENNReal.ofReal p)] (hp : 2 < p) (hp4 : p < 4) :
    ∃ u : scalarWeightedH1 d, ‖u‖ = 1 ∧
      ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) u‖ =
        ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le)‖ := by
…

theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_L2_distribution_injective line 12519

theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_weak_product line 12532

Source documentation

The product of H2 factors has an L2 weak derivative with the actual Leibniz formula. The result identifies the derivative of any L2 realization of the pointwise product.

theorem scalar_real_weak_product (u v w du dv : L2)
    (hu : MemSobolev 2 2 (scalarComplexL2 u : T))
    (hv : MemSobolev 2 2 (scalarComplexL2 v : T))
    (hw : (w : V → ℝ) =ᵐ[volume] fun x => u x * v x)
    (i : Fin 4)
    (hdu : scalarCoordinateDerivative i (scalarComplexL2 u : T) = (scalarComplexL2 du : T))
    (hdv : scalarCoordinateDerivative i (scalarComplexL2 v : T) = (scalarComplexL2 dv : T)) :
    ∃ z : L2, scalarCoordinateDerivative i (scalarComplexL2 w : T) = (scalarComplexL2 z : T) ∧
      (z : V → ℝ) =ᵐ[volume] fun x => du x * v x + u x * dv x := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarComplexL2, OAI.PositiveEinsteinFour.Geometry.scalarCoordinateDerivative

theorem OAI.PositiveEinsteinFour.Geometry.twoFormCutoffPartial_smooth line 12599
def OAI.PositiveEinsteinFour.Geometry.twoFormConnectionCutoff line 12603
theorem OAI.PositiveEinsteinFour.Geometry.twoFormConnectionCutoff_smooth line 12607
def OAI.PositiveEinsteinFour.Geometry.twoFormGramConnectionL2 line 12621
def OAI.PositiveEinsteinFour.Geometry.twoFormGramCovariantL2 line 12627
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramValueL2_coe line 12634
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramConnectionL2_coe line 12642
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCovariantL2_coe line 12678
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyBasePartial_slice line 12730
def OAI.PositiveEinsteinFour.Geometry.heatFamilyMetric line 12743
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyMetric_contDiffAt line 12748
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyMetric_exponential_germ line 12773
theorem OAI.PositiveEinsteinFour.Geometry.heatMatrixDeterminant_smoothAt line 12819
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalInverse_smoothAt_zero line 12830
theorem OAI.PositiveEinsteinFour.Geometry.heat_matrix_congruence_pairing line 12871
theorem OAI.PositiveEinsteinFour.Geometry.heat_matrix_inverse_congruence line 12882
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.metric_pullback line 12893
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.inverseMetric_transport line 12912
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.inverseMetric_transport_near line 12929
theorem OAI.PositiveEinsteinFour.Geometry.heatWeighted_integrable line 12956
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatWeightedRadialAverage_sum line 12963
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatWeightedRadialAverage_add line 12973
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatWeightedRadialAverage_const_mul line 12984
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatWeightedRadialAverage_zero_germ line 12995
def OAI.PositiveEinsteinFour.Geometry.scalarBaseSpectralEquiv line 13043
def OAI.PositiveEinsteinFour.Geometry.scalarBaseSpectralMultiplier line 13046
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseSpectralMultiplier_coordinate line 13062
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseSpectralMultiplier_norm line 13072
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseSpectralMultiplier_inner line 13091
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseSpectralMultiplier_selfAdjoint line 13102
theorem OAI.PositiveEinsteinFour.Geometry.scalar_eigen_local_chart_smooth line 13143
theorem OAI.PositiveEinsteinFour.Geometry.scalar_localized_H2_composition_derivative line 13228
theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_sobolev_add line 13294

theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_H3_product line 13307

Source documentation

Two H3 functions have an actual H3 pointwise product.

theorem scalar_real_H3_product (u v : L2)
    (hu : MemSobolev 3 2 (scalarComplexL2 u : T))
    (hv : MemSobolev 3 2 (scalarComplexL2 v : T)) :
    ∃ w : L2, MemSobolev 3 2 (scalarComplexL2 w : T) ∧
      (w : V → ℝ) =ᵐ[volume] fun x => u x * v x := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarComplexL2

def OAI.PositiveEinsteinFour.Geometry.integerDensityCutoffL2 line 13353
theorem OAI.PositiveEinsteinFour.Geometry.integerDensityCutoffL2_distribution line 13356
theorem OAI.PositiveEinsteinFour.Geometry.integerDensityCutoffL2_coe line 13362
theorem OAI.PositiveEinsteinFour.Geometry.integerDensityCutoff_support line 13369
theorem OAI.PositiveEinsteinFour.Geometry.scalar_integer_density_division line 13376
theorem OAI.PositiveEinsteinFour.Geometry.scalar_inverse_cube_gradient line 13432
theorem OAI.PositiveEinsteinFour.Geometry.scalar_reciprocal_equation_derivative line 13449
theorem OAI.PositiveEinsteinFour.Geometry.scalar_inverse_hessian_algebra line 13493
theorem OAI.PositiveEinsteinFour.Geometry.scalar_normalize_extremal line 13525
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedBaseLp_one line 13557
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarToWeightedH1_one_norm_sq line 13566

theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_normalized_minimum line 13579

Source documentation

The normalized actual subcritical minimum is positive, at most one, and bounds the homogeneous energy of every completed scalar first jet.

theorem scalar_subcritical_normalized_minimum (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) {p : ℝ}
    [Fact (1 ≤ ENNReal.ofReal p)] (hp : 2 < p) (hp4 : p < 4) :
    ∃ w : scalarWeightedH1 d,
      ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) w‖ = 1 ∧
      0 < ‖w‖ ^ 2 ∧ ‖w‖ ^ 2 ≤ 1 ∧
      ∀ v : scalarWeightedH1 d, ‖w‖ ^ 2 *
        ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) v‖ ^ 2
          ≤ ‖v‖ ^ 2 := by
…

theorem OAI.PositiveEinsteinFour.Geometry.scalar_positive_Euler_local_H4 line 13639
theorem OAI.PositiveEinsteinFour.Geometry.scalar_resolvent_chain_local line 13832
theorem OAI.PositiveEinsteinFour.Geometry.scalarReal_memSobolev_sum line 13980
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramConnection_memSobolev_one line 14007
def OAI.PositiveEinsteinFour.Geometry.twoFormGramDerivativeCorrection line 14021
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCovariant_add_correction line 14027
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramDerivativeCorrection_memSobolev_one line 14039
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramDerivativeCorrection_derivative line 14050
def OAI.PositiveEinsteinFour.Geometry.twoFormComponentIndex line 14077
theorem OAI.PositiveEinsteinFour.Geometry.twoFormTensor_component line 14080
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_sum_components line 14084
def OAI.PositiveEinsteinFour.Geometry.twoFormComponentL2 line 14089
theorem OAI.PositiveEinsteinFour.Geometry.twoFormComponentL2_coe line 14093
def OAI.PositiveEinsteinFour.Geometry.twoFormAssembleL2 line 14102
theorem OAI.PositiveEinsteinFour.Geometry.twoFormAssembleL2_coe line 14106
def OAI.PositiveEinsteinFour.Geometry.twoFormGramVectorL2 line 14130
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramVectorL2_coe line 14134
def OAI.PositiveEinsteinFour.Geometry.twoFormGramNablaL2 line 14145
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramNablaL2_coe line 14150
def OAI.PositiveEinsteinFour.Geometry.heatFamilyDensity line 14191
def OAI.PositiveEinsteinFour.Geometry.heatFamilyLeading line 14195
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyDensity_contDiffAt line 14199
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyLeading_contDiffAt line 14208
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyInverse_contDiffAt line 14218
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyDensity_exponential_germ line 14229
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyLeading_exponential_germ line 14240
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyMetric_exponential_eq line 14271
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.metric_slice_eq line 14290
abbrev OAI.PositiveEinsteinFour.Geometry.heatNormalDrift line 14322
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalInverse_symm line 14327
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalLeadingAmplitude_transport_neighborhood line 14332
theorem OAI.PositiveEinsteinFour.Geometry.heat_jacobianMatrix_det line 14404
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.volume_jacobian line 14418
theorem OAI.PositiveEinsteinFour.Geometry.heatPullbackMetric_jacobian_unit line 14453
theorem OAI.PositiveEinsteinFour.Geometry.heatPullback_drift line 14462
theorem OAI.PositiveEinsteinFour.Geometry.heatPullback_drift_transport line 14475
def OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatRate line 14518
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatRate_nonneg line 14521
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatRate_eq_zero line 14527
def OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatWeight line 14532
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatWeight_bound line 14536
def OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat line 14542
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_coordinate line 14546
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_zero line 14552
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_add line 14560
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_contraction line 14572
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_selfAdjoint line 14577
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_nonneg line 14581
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseSpectralMultiplier_sub_norm_sq line 14609
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseSpectralMultiplier_tendsto line 14628
def OAI.PositiveEinsteinFour.Geometry.scalarCriticalExponent line 14688
theorem OAI.PositiveEinsteinFour.Geometry.scalarCriticalExponent_bounds line 14690
theorem OAI.PositiveEinsteinFour.Geometry.scalarCriticalExponent_tendsto line 14698
theorem OAI.PositiveEinsteinFour.Geometry.scalar_moment_critical_limit line 14705
theorem OAI.PositiveEinsteinFour.Geometry.sharpScalarSobolev_of_subcritical_moments line 14753
Source documentation
Subcritical inequalities with the sharp constant pass to the exact critical inequality used in the two Weyl-block gaps.
```
theorem sharpScalarSobolev_of_subcritical_moments (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o))
    (hsub : ∀ (p : ℝ), 2 < p → p < 4 → ∀ a : SmoothScalar (M := M),
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.SmoothScalar
theorem OAI.PositiveEinsteinFour.Geometry.scalar_weak_eigen_smooth_representative line 14792
theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_integer_product line 14849
def OAI.PositiveEinsteinFour.Geometry.scalarLpAbs line 14907
theorem OAI.PositiveEinsteinFour.Geometry.scalarLpAbs_coe line 14910
theorem OAI.PositiveEinsteinFour.Geometry.scalarLpAbs_nonneg line 14914
theorem OAI.PositiveEinsteinFour.Geometry.scalarLpAbs_norm line 14919
theorem OAI.PositiveEinsteinFour.Geometry.scalarLpAbs_continuous line 14923
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedBaseLp_absRegularized_error line 14938
def OAI.PositiveEinsteinFour.Geometry.scalarSubcriticalWeight line 14987
theorem OAI.PositiveEinsteinFour.Geometry.scalar_inverse_hessian_divergence line 14990
theorem OAI.PositiveEinsteinFour.Geometry.scalar_reciprocal_subcritical_constants line 15023
Source documentation
The Hessian sign identity forces any positive smooth reciprocal solution with exponent below four to be constant.
```
theorem scalar_reciprocal_subcritical_constants (g : SmoothMetric M)
    (o : FrameOrientation g) (hRic : RicciThree g) {a : M → ℝ}
    (ha : ContMDiff I4 𝓘(ℝ, ℝ) ∞ a) (hpos : ∀ x, 0 < a x)
    (p : ℝ) (hp : p < 4)
    (hEq : ∀ e : FrameBundle g,
      a e.base * scalarLaplacian g a e -
        2 * (∑ i, scalarGradient g a e i ^ 2) + 2 * a e.base ^ 2 =
          2 * (a e.base) ^ (4 - p)) :
    ∃ c : ℝ, ∀ x, a x = c := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.RicciThree, OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.scalarLaplacian, OAI.PositiveEinsteinFour.Geometry.scalarGradient
theorem OAI.PositiveEinsteinFour.Geometry.scalar_positive_Euler_C1 line 15102
theorem OAI.PositiveEinsteinFour.Geometry.scalar_localized_positive_power_weak_derivative line 15172
theorem OAI.PositiveEinsteinFour.Geometry.scalar_reciprocal_gradient line 15244
theorem OAI.PositiveEinsteinFour.Geometry.scalar_reciprocal_hessian line 15255
theorem OAI.PositiveEinsteinFour.Geometry.scalar_reciprocal_laplacian line 15278
theorem OAI.PositiveEinsteinFour.Geometry.scalar_reciprocal_gradient_energy line 15292
theorem OAI.PositiveEinsteinFour.Geometry.scalar_reciprocal_euler_equation line 15303
theorem OAI.PositiveEinsteinFour.Geometry.scalar_energy_line_hasDerivAt line 15345
Source documentation
The quadratic energy has its usual derivative along an affine line in the completed energy space; no smooth representative is required.
```
theorem scalar_energy_line_hasDerivAt
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (w b : H) :
    HasDerivAt (fun t : ℝ => ‖w + t • b‖ ^ 2) (2 * inner ℝ w b) 0 := by
…
```

theorem OAI.PositiveEinsteinFour.Geometry.scalar_energy_minimum_euler line 15355

Source documentation

Fermat's rule applied to the homogeneous Sobolev quotient. The only analytic ingredient here is the directional derivative of its norm term.

theorem scalar_energy_minimum_euler
    {H E : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    [NormedAddCommGroup E] [NormedSpace ℝ E] (T : H →L[ℝ] E)
    (w b : H) (hunit : ‖T w‖ = 1)
    (hmin : ∀ v : H, ‖w‖ ^ 2 * ‖T v‖ ^ 2 ≤ ‖v‖ ^ 2)
    (I : ℝ) (hvar : HasDerivAt (fun t : ℝ => ‖T (w + t • b)‖ ^ 2) (2 * I) 0) :
    inner ℝ w b = ‖w‖ ^ 2 * I := by
…

theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_minimum_weak_euler line 15390

Source documentation

The actual weak Euler equation for a normalized subcritical minimum, against every smooth scalar test function.

theorem scalar_subcritical_minimum_weak_euler (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) {p : ℝ}
    [Fact (1 ≤ ENNReal.ofReal p)] (hp : 2 < p) (hp4 : p < 4)
    (w : scalarWeightedH1 d)
    (hw : ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) w‖ = 1)
    (hmin : ∀ v : scalarWeightedH1 d, ‖w‖ ^ 2 *
      ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) v‖ ^ 2 ≤ ‖v‖ ^ 2)
    (a : SmoothScalar (M := M)) :
…

theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_weak_euler_exists line 15410
Source documentation
Existence of an actual normalized subcritical weak Euler solution.
```
theorem scalar_subcritical_weak_euler_exists (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) {p : ℝ}
    [Fact (1 ≤ ENNReal.ofReal p)] (hp : 2 < p) (hp4 : p < 4) :
    ∃ w : scalarWeightedH1 d,
      ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) w‖ = 1 ∧
      0 < ‖w‖ ^ 2 ∧ ‖w‖ ^ 2 ≤ 1 ∧
      ∀ a : SmoothScalar (M := M),
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1, OAI.PositiveEinsteinFour.Geometry.scalarWeightedBaseLp, OAI.PositiveEinsteinFour.Geometry.SmoothScalar
def OAI.PositiveEinsteinFour.Geometry.smoothL2AsH1 line 15445
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormGramL2Linear line 15455
theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormGramL2Linear_bound line 15460
def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormGramL2 line 15508
def OAI.PositiveEinsteinFour.Geometry.twoFormL2GramValue line 15513
theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2GramValue_smooth line 15517
theorem OAI.PositiveEinsteinFour.Geometry.twoFormLocalNabla_contDiffAt line 15542
def OAI.PositiveEinsteinFour.Geometry.twoFormMassTest line 15566
def OAI.PositiveEinsteinFour.Geometry.twoFormEnergyTest line 15569
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMassTest_support line 15574
theorem OAI.PositiveEinsteinFour.Geometry.twoFormEnergyTest_support line 15578
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMassTest_smooth line 15587
theorem OAI.PositiveEinsteinFour.Geometry.twoFormEnergyTest_smooth line 15599
def OAI.PositiveEinsteinFour.Geometry.twoFormMassTestL2 line 15616
def OAI.PositiveEinsteinFour.Geometry.twoFormEnergyTestL2 line 15624
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMassTestL2_coe line 15632
theorem OAI.PositiveEinsteinFour.Geometry.twoFormEnergyTestL2_coe line 15638
def OAI.PositiveEinsteinFour.Geometry.twoFormVectorComponentL2 line 15661
theorem OAI.PositiveEinsteinFour.Geometry.twoFormVectorComponentL2_coe line 15665
theorem OAI.PositiveEinsteinFour.Geometry.twoFormVectorComponentL2_assemble line 15675
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramVectorComponent line 15686
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramVectorComponent_memSobolev_one line 15694
def OAI.PositiveEinsteinFour.Geometry.heatFamilyDrift line 15724
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyDrift_contDiffAt line 15731
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyDrift_slice line 15747
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatDensityDrift_congr line 15780
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.metric_pullback_near line 15796
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.drift_transport_near line 15808
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalGaussian_leading_residual line 15855
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalScalarLift_integral line 15903
theorem OAI.PositiveEinsteinFour.Geometry.heatScalarCutoff_contDiff line 15960
def OAI.PositiveEinsteinFour.Geometry.heatScalarBump line 15972
theorem OAI.PositiveEinsteinFour.Geometry.heatScalar_extension line 15978
theorem OAI.PositiveEinsteinFour.Geometry.heatScalar_positive_extension line 15993
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatWeight_continuous line 16044
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_continuous line 16050
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_tendsto_zero_time line 16059
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_joint_continuous line 16066
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_coordinate line 16120
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatPowerWeight_bound line 16139
def OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatPowerSource line 16171
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_power_coordinate line 16177
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatPowerSource_resolvent line 16189
theorem OAI.PositiveEinsteinFour.Geometry.scalar_weak_eigen_smooth line 16232
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseEigenvector_smooth line 16274
theorem OAI.PositiveEinsteinFour.Geometry.scalar_positive_subcritical_euler line 16308
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_base_composition line 16389
Source documentation
The actual base representative has the same composition law as its frame pullback. Membership in L² is the only integrability requirement.
```
theorem scalarH1_base_composition (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o))
    (u v : scalarH1 d) (φ : ℝ → ℝ)
    (hv : scalarH1Value d v =ᵐ[canonicalFrameMeasure g o]
      fun e => φ (scalarH1Value d u e))
    (hmem : MemLp (fun x => φ (scalarH1BaseValue g o d u x)) 2 (normalizedVolume g)) :
    scalarH1BaseValue g o d v =ᵐ[normalizedVolume g]
      fun x => φ (scalarH1BaseValue g o d u x) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.scalarH1Value, OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue, OAI.PositiveEinsteinFour.Geometry.normalizedVolume
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_katoTest_base_exists line 16419
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_katoSquare_base_exists line 16437
theorem OAI.PositiveEinsteinFour.Geometry.scalar_minimum_kato_test line 16460
Source documentation
Admissibility and the exact nonlinear Euler identity for a rational test of an actual homogeneous minimum.
```
theorem scalar_minimum_kato_test (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) {p : ℝ}
    [Fact (1 ≤ ENNReal.ofReal p)] (hp : 2 < p) (hp4 : p < 4)
    (w : scalarWeightedH1 d)
    (hw : ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) w‖ = 1)
    (hmin : ∀ z : scalarWeightedH1 d, ‖w‖ ^ 2 *
      ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) z‖ ^ 2 ≤ ‖z‖ ^ 2)
    {lam : ℝ} (hlam : 0 < lam) :
    ∃ v : scalarH1 d,
      scalarH1BaseValue g o d v =ᵐ[normalizedVolume g]
        (fun x => scalarKatoTest lam
          (scalarH1BaseValue g o d (scalarWeightedH1ToH1 d w) x)) ∧
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1, OAI.PositiveEinsteinFour.Geometry.scalarWeightedBaseLp, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue, OAI.PositiveEinsteinFour.Geometry.normalizedVolume, OAI.PositiveEinsteinFour.Geometry.scalarKatoTest, OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1ToH1
theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_sobolev_smul line 16530
theorem OAI.PositiveEinsteinFour.Geometry.scalar_real_integer_product_extra line 16536
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_minimum_absolute line 16574

theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_nonnegative_minimum line 16620

Source documentation

There is a nonnegative normalized weak Euler minimizer in the actual completed scalar Sobolev space, with positive energy at most one.

theorem scalar_subcritical_nonnegative_minimum (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) {p : ℝ}
    [Fact (1 ≤ ENNReal.ofReal p)] (hp : 2 < p) (hp4 : p < 4) :
    ∃ w : scalarWeightedH1 d,
      ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) w‖ = 1 ∧
      0 < ‖w‖ ^ 2 ∧ ‖w‖ ^ 2 ≤ 1 ∧
      (∀ᵐ x ∂normalizedVolume g,
        0 ≤ scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) w x) ∧
      (∀ v : scalarWeightedH1 d, ‖w‖ ^ 2 *
        ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) v‖ ^ 2 ≤ ‖v‖ ^ 2) := by
…

theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedBaseLp_injective line 16667
theorem OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1_eq_smooth_of_Lp_representative line 16682
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarToWeightedH1_inner line 16691
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficient_bound line 16728
def OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientBound line 16732
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientBound_nonneg line 16734
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientBound_le line 16737
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientPair_memLp line 16740
def OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientPair line 16748
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientPair_coe line 16752
def OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientPairLinear line 16756
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientPair_norm line 16775
def OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientPairL2 line 16784
theorem OAI.PositiveEinsteinFour.Geometry.twoFormTensor_coordinate_expansion line 16806
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramValue_tensor_coe line 16821
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramValue_component_expansion line 16829
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_product_coordinate_bound line 16895
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_product_local_norm line 16913
theorem OAI.PositiveEinsteinFour.Geometry.twoFormLocalNabla_smul_const line 16975
def OAI.PositiveEinsteinFour.Geometry.twoFormWeightedConnection line 16988
theorem OAI.PositiveEinsteinFour.Geometry.twoFormEnergyTest_smul_const line 16993
theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeightedConnection_contDiffAt line 17009
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCutoffWeightedConnection_smooth line 17016
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_partial_contDiff line 17046
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_contDiff line 17052
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_partial_germ line 17070
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialTransport_germ line 17074
def OAI.PositiveEinsteinFour.Geometry.heatFamilyFirst line 17100
def OAI.PositiveEinsteinFour.Geometry.heatFamilyZero line 17106
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyFirst_contDiffAt line 17115
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyZero_contDiffAt line 17128
def OAI.PositiveEinsteinFour.Geometry.heatFamilyOneFirst line 17182
def OAI.PositiveEinsteinFour.Geometry.heatFamilyOneZero line 17188
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOneFirst_contDiffAt line 17197
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOneZero_contDiffAt line 17210
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.metric_pullback_germ line 17264
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.drift_transport_at line 17274
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.rough_pullback_near line 17315
def OAI.PositiveEinsteinFour.Geometry.scalarBaseEigenfunction line 17368
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseEigenfunction_L2 line 17371
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseEigenfunction_laplacian line 17375
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_eigenvector line 17380
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseEigenfunction_norm line 17400
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_fixed_smooth line 17432
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_fixed_one line 17452
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_fixed_constant line 17471
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarHessian_const_smul line 17509
theorem OAI.PositiveEinsteinFour.Geometry.smoothScalarLaplacian_const_smul line 17530
theorem OAI.PositiveEinsteinFour.Geometry.scalar_positive_normalized_euler_minimum_one line 17544
Source documentation
Once positive smooth regularity is known, the normalized minimum has energy one and its representative is the constant one.
```
theorem scalar_positive_normalized_euler_minimum_one (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
theorem OAI.PositiveEinsteinFour.Geometry.kato_square_bound line 17606
theorem OAI.PositiveEinsteinFour.Geometry.kato_real_inner line 17614
theorem OAI.PositiveEinsteinFour.Geometry.kato_gradient_le line 17620

theorem OAI.PositiveEinsteinFour.Geometry.scalarKato_potential_memLp line 17638

Source documentation

The subcritical nonlinear potential is in L² because the actual H¹ value is already in L⁴.

theorem scalarKato_potential_memLp {X : Type*} [MeasurableSpace X]
    {μ : Measure X} [IsFiniteMeasure μ] {f : X → ℝ} (hf : MemLp f 4 μ)
    {p : ℝ} (hp : 2 < p) (hp4 : p < 4) :
    MemLp (fun x => |f x| ^ (p - 2)) 2 μ := by
…

theorem OAI.PositiveEinsteinFour.Geometry.scalar_minimum_kato_energy line 17671

Source documentation

The rational square has controlled actual first-jet energy.

theorem scalar_minimum_kato_energy (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) {p : ℝ}
    [Fact (1 ≤ ENNReal.ofReal p)] (hp : 2 < p) (hp4 : p < 4)
    (w : scalarWeightedH1 d)
    (hw : ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) w‖ = 1)
    (hm : ‖w‖ ^ 2 ≤ 1)
    (hmin : ∀ z : scalarWeightedH1 d, ‖w‖ ^ 2 *
      ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) z‖ ^ 2 ≤ ‖z‖ ^ 2)
    {lam : ℝ} (hlam : 0 < lam) :
    ∃ z : scalarH1 d,
      scalarH1BaseValue g o d z =ᵐ[normalizedVolume g]
        (fun x => scalarKatoSquare lam
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1, OAI.PositiveEinsteinFour.Geometry.scalarWeightedBaseLp, OAI.PositiveEinsteinFour.Geometry.scalarH1, OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue, OAI.PositiveEinsteinFour.Geometry.normalizedVolume, OAI.PositiveEinsteinFour.Geometry.scalarKatoSquare

theorem OAI.PositiveEinsteinFour.Geometry.scalar_minimum_memLp_eight line 17750

Source documentation

The actual normalized homogeneous minimum has an L⁸ base value.

theorem scalar_minimum_memLp_eight (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) {p : ℝ}
    [Fact (1 ≤ ENNReal.ofReal p)] (hp : 2 < p) (hp4 : p < 4)
    (w : scalarWeightedH1 d)
    (hw : ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) w‖ = 1)
    (hm : ‖w‖ ^ 2 ≤ 1)
    (hmin : ∀ z : scalarWeightedH1 d, ‖w‖ ^ 2 *
      ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) z‖ ^ 2 ≤ ‖z‖ ^ 2) :
    MemLp (scalarH1BaseValue g o d (scalarWeightedH1ToH1 d w)) 8 (normalizedVolume g) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.ParallelMetricData, OAI.PositiveEinsteinFour.Geometry.canonicalFrameMeasure, OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1, OAI.PositiveEinsteinFour.Geometry.scalarWeightedBaseLp, OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue, OAI.PositiveEinsteinFour.Geometry.scalarWeightedH1ToH1, OAI.PositiveEinsteinFour.Geometry.normalizedVolume

theorem OAI.PositiveEinsteinFour.Geometry.scalar_localized_integer_positive_power line 17810

Source documentation

A positive bounded local power loses at most one of the available integer Sobolev derivatives. Combined with the two-derivative elliptic gain, this is the required ascending bootstrap.

theorem scalar_localized_integer_positive_power (n : ℕ) (hn : 2 ≤ n) :
    ∀ (u : L2) (χ : S), HasCompactSupport (χ : V → ℝ) →
      ∀ (a B q : ℝ), 0 < a → 0 ≤ B →
      MemSobolev ((n : ℝ) + 1) 2 (scalarComplexL2 u : T) →
      (∀ᵐ x ∂(volume : Measure V), x ∈ tsupport (χ : V → ℝ) → u x ∈ Icc a B) →
      ∃ v : L2, MemSobolev (n : ℝ) 2 (scalarComplexL2 v : T) ∧
        (v : V → ℝ) =ᵐ[volume] fun x => χ x * (u x) ^ q := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarComplexL2

def OAI.PositiveEinsteinFour.Geometry.scalarBaseResolventJet line 17892
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolventJet_value line 17895
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolventJet_weak line 17901
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseResolvent_local_orders line 17913
theorem OAI.PositiveEinsteinFour.Geometry.scalar_minimum_euler_all_H1_of_L2_source line 17963
theorem OAI.PositiveEinsteinFour.Geometry.scalar_weighted_euler_to_weak_poisson line 17994
def OAI.PositiveEinsteinFour.Geometry.twoFormChartPotential line 18032
theorem OAI.PositiveEinsteinFour.Geometry.twoFormChartPotential_contDiffAt line 18036
def OAI.PositiveEinsteinFour.Geometry.twoFormPotentialCoefficient line 18042
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotentialCoefficient_smooth line 18047
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotentialCoefficient_compact line 18058
theorem OAI.PositiveEinsteinFour.Geometry.twoForm_linear_coordinate line 18062
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotentialCoefficient_pair line 18069
def OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientSchwartz line 18096
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientSchwartz_apply line 18100
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientPair_complex line 18103
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientPair_distribution line 18142
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientPair_memSobolev_one line 18156
def OAI.PositiveEinsteinFour.Geometry.twoFormWeightedTestL2 line 18194
theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeightedTestL2_coe line 18199
theorem OAI.PositiveEinsteinFour.Geometry.twoFormCoefficientPair_test line 18204
def OAI.PositiveEinsteinFour.Geometry.twoFormMassCoefficient line 18240
def OAI.PositiveEinsteinFour.Geometry.twoFormFluxCoefficient line 18243
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMassCoefficient_smooth line 18253
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFluxCoefficient_smooth line 18257
def OAI.PositiveEinsteinFour.Geometry.twoFormMassPair line 18263
def OAI.PositiveEinsteinFour.Geometry.twoFormFluxPair line 18268
def OAI.PositiveEinsteinFour.Geometry.twoFormConnectionPair line 18273
def OAI.PositiveEinsteinFour.Geometry.twoFormDivergenceFlux line 18278
def OAI.PositiveEinsteinFour.Geometry.twoFormDivergenceSource line 18282
theorem OAI.PositiveEinsteinFour.Geometry.twoFormValueNormL2_partition line 18309
theorem OAI.PositiveEinsteinFour.Geometry.twoFormValueNormL2_eq_H1value_norm line 18336
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1_partition_bound line 18347
def OAI.PositiveEinsteinFour.Geometry.fourHeatCoefficient line 18384
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCoefficient_contDiff line 18390
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCoefficient_transport line 18414
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCoefficient_center line 18430
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_second_germ line 18456
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_germ line 18464
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleOperator_germ line 18470
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleOperator_zero_of_locally_zero line 18479
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_partial_const_mul line 18508
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_partial_add line 18514
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_second_const_mul line 18519
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_second_add line 18524
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_const_mul line 18538
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatLocalOperator_add line 18547
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialTransport_const_mul line 18558
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialTransport_add line 18566
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarJet_bound line 18593
abbrev OAI.PositiveEinsteinFour.Geometry.HeatFamilyCoefficientIndex line 18615
def OAI.PositiveEinsteinFour.Geometry.heatFamilyCoefficient line 18621
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyCoefficient_contDiffAt line 18630
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyCoefficient_local_bound line 18642
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalDrift_smoothAt_zero line 18686
structure OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension line 18702
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalExtension line 18715
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.transport_neighborhood line 18747
theorem OAI.PositiveEinsteinFour.Geometry.heat_orthonormal_inverse line 18801
theorem OAI.PositiveEinsteinFour.Geometry.heat_framedSecond_chart line 18815
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.roughTrace_as_actual line 18835
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.actual_tensor_rough_near line 18856
theorem OAI.PositiveEinsteinFour.Geometry.heat_scalar_second_comp line 18892
theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_chart_laplacian line 18934
def OAI.PositiveEinsteinFour.Geometry.scalarBaseHarmonicWeight line 18975
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHarmonicWeight_bound line 18980
def OAI.PositiveEinsteinFour.Geometry.scalarBaseHarmonicProjection line 18985
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHarmonicProjection_coordinate line 18989
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHarmonicProjection_fixed line 18995
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHarmonicProjection_of_fixed line 19006
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHarmonicProjection_mean line 19024
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeatWeight_tendsto line 19054
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_tendsto_harmonic line 19074
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_local_all_orders line 19105
def OAI.PositiveEinsteinFour.Geometry.scalarFiniteValueL2 line 19168
def OAI.PositiveEinsteinFour.Geometry.scalarFiniteLaplacianL2 line 19172
theorem OAI.PositiveEinsteinFour.Geometry.scalarFiniteValueL2_coe line 19178
theorem OAI.PositiveEinsteinFour.Geometry.scalarFiniteLaplacianL2_coe line 19183
theorem OAI.PositiveEinsteinFour.Geometry.scalarFiniteLaplacian_eigen line 19187
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1BaseValue_injective line 19243
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseShiftedSolution_dense line 19250
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseShiftedSolution_eigen_smooth line 19253
theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_eigenfunctions_total line 19261
def OAI.PositiveEinsteinFour.Geometry.scalarHeatConvolution line 19304
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatConvolution_integrable line 19307
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatConvolution_norm_le line 19315
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatConvolution_eigen line 19329
theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_integer_power_source line 19371
theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_sobolev_transfer line 19421
theorem OAI.PositiveEinsteinFour.Geometry.scalarReal_memSobolev_finset line 19457
theorem OAI.PositiveEinsteinFour.Geometry.scalar_nonlinear_memLp_two_of_eight line 19490
def OAI.PositiveEinsteinFour.Geometry.smoothScalarPositivePower line 19540
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_pointwise_euler_of_positive_representative line 19556
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_minimum_one_of_positive_representative line 19626
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCoefficient_memSobolev_one line 19669
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCoefficient_derivative line 19675
def OAI.PositiveEinsteinFour.Geometry.twoFormGramPartialVectorL2 line 19712
def OAI.PositiveEinsteinFour.Geometry.twoFormGramCorrectionVectorL2 line 19716
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCorrectionVector_component line 19721
theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramCorrectionVector_component_H1 line 19733
def OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalFlux line 19740
def OAI.PositiveEinsteinFour.Geometry.twoFormFluxCorrection line 19745
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPrincipalFlux_eq line 19750
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFluxCorrection_memSobolev_one line 19765
theorem OAI.PositiveEinsteinFour.Geometry.twoFormFluxCorrection_derivatives line 19775
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1ToL2_compact line 19813
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMassTest_separated line 19866
theorem OAI.PositiveEinsteinFour.Geometry.twoFormEnergyTest_separated line 19880
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_local_product_integrable line 19923
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_local_integration_by_parts line 19934
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_local_second_integration line 19959
def OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomial line 19994
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomial_contDiff line 19997
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomial_hasDerivAt line 20002
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomial_operator line 20012
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomial_transport line 20028
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomial_gaussian_residual line 20044
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverage_preserves_contDiff line 20100
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatWeightedRadialAverage_preserves_contDiff line 20129
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCoefficient_contDiff_two_derivatives line 20134
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatActualFamilyBound line 20176
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatDensityDrift_germ line 20230
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatConnectionZero_germ line 20240
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyFirst_slice line 20253
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyZero_slice line 20262
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyCutoff_contDiff line 20316
def OAI.PositiveEinsteinFour.Geometry.heatFamilyBump line 20328
theorem OAI.PositiveEinsteinFour.Geometry.heatFamily_scalar_extension line 20335
theorem OAI.PositiveEinsteinFour.Geometry.heatFamily_positive_extension line 20351
def OAI.PositiveEinsteinFour.Geometry.heatNormalBundleFirst line 20397
def OAI.PositiveEinsteinFour.Geometry.heatNormalBundleZero line 20403
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.bundleFirst_regular line 20409
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.bundleZero_regular line 20418
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.bundleFirst_radial line 20430
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.bundleFirst_radial_near line 20444
def OAI.PositiveEinsteinFour.Geometry.heatNormalExtension line 20476
def OAI.PositiveEinsteinFour.Geometry.heatNormalCoefficient line 20480
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCoefficient_contDiff line 20485
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCoefficient_leading line 20496
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCoefficient_zero_center line 20501
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalCoefficient_transport line 20506
theorem OAI.PositiveEinsteinFour.Geometry.heat_normal_frame_pairing line 20554
def OAI.PositiveEinsteinFour.Geometry.heatNormalOneFirst line 20601
def OAI.PositiveEinsteinFour.Geometry.heatNormalOneZero line 20607
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneFirst_regular line 20613
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneZero_regular line 20622
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneFirst_radial line 20634
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneFirst_radial_near line 20648
theorem OAI.PositiveEinsteinFour.Geometry.heat_normal_one_pairing line 20677
theorem OAI.PositiveEinsteinFour.Geometry.heat_framedValue_chart line 20723
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.value_as_actual line 20743
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.potential_action_as_actual line 20759
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.scalar_operator_pullback line 20794
theorem OAI.PositiveEinsteinFour.Geometry.scalar_distribution_memSobolev_finset line 20865
theorem OAI.PositiveEinsteinFour.Geometry.scalar_compact_sobolev_assembly line 20875
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_local_chart_smooth line 20949
theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_integer_nonlinear_source line 21030
theorem OAI.PositiveEinsteinFour.Geometry.scalar_minimum_L2_source_of_memLp_eight line 21131

theorem OAI.PositiveEinsteinFour.Geometry.scalar_minimum_L2_source line 21163

Source documentation

The actual normalized minimum has an L2 nonlinear source, with no regularity premise on its representative.

theorem scalar_minimum_L2_source
    (g : SmoothMetric M) (o : FrameOrientation g)
    (d : ParallelMetricData g (canonicalFrameMeasure g o)) {p : ℝ}
    [Fact (1 ≤ ENNReal.ofReal p)] (hp : 2 < p) (hp4 : p < 4)
    (w : scalarWeightedH1 d)
    (hw : ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) w‖ = 1)
    (hm : ‖w‖ ^ 2 ≤ 1)
    (hmin : ∀ v : scalarWeightedH1 d, ‖w‖ ^ 2 *
      ‖scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) v‖ ^ 2 ≤ ‖v‖ ^ 2) :
    ∃ F : Lp ℝ 2 (normalizedVolume g),
      F =ᵐ[normalizedVolume g] (fun x =>
        |scalarWeightedBaseLp g o d (ENNReal.ofReal p) (by exact_mod_cast hp4.le) w x| ^ (p - 2) *
…

theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_derivative_memLp_four line 21203
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_nonlinear_gradient_memLp_two line 21229
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_bound_of_positive_representative line 21271
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1ToL2_dense line 21322
def OAI.PositiveEinsteinFour.Geometry.twoFormRoughSolution line 21328
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRoughSolution_weak line 21331
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRoughSolution_unique line 21335
def OAI.PositiveEinsteinFour.Geometry.twoFormRoughResolvent line 21342
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRoughResolvent_compact line 21345
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRoughResolvent_inner line 21348
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRoughResolvent_selfAdjoint line 21353
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRoughResolvent_nonneg line 21361
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRoughSolution_injective line 21366
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRoughResolvent_injective line 21381
theorem OAI.PositiveEinsteinFour.Geometry.twoFormMassTestL2_separated line 21418
theorem OAI.PositiveEinsteinFour.Geometry.twoFormEnergyTestL2_separated line 21434
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleOperator_contDiff line 21481
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneOperator_contDiff line 21517
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_amplitude_integrable line 21553
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_amplitude_limit line 21563
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomial_gaussian_integral line 21571
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomial_approximate_identity line 21601
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomial_joint_continuous line 21633
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomial_partial line 21643
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomial_partial_joint_continuous line 21657
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverage_partial_zero line 21681
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatRadialAverage_second_zero line 21688
def OAI.PositiveEinsteinFour.Geometry.heatChartTensor line 21721
theorem OAI.PositiveEinsteinFour.Geometry.heatChartTensor_smooth line 21730
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyNormal_on_ball line 21782
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneConnectionZero_germ line 21865
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOneFirst_slice line 21878
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOneZero_slice line 21887
structure OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients line 21940
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatFamilySmoothCoefficients line 21956
structure OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension line 22028
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalBundleExtension line 22038
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.radial_near line 22065
theorem OAI.PositiveEinsteinFour.Geometry.heat_euclideanTensor_inner line 22090
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalLift_pairing line 22100
structure OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension line 22151
theorem OAI.PositiveEinsteinFour.Geometry.exists_heatNormalOneExtension line 22161
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.radial_near line 22188
theorem OAI.PositiveEinsteinFour.Geometry.heat_radial_axis_zero line 22213
theorem OAI.PositiveEinsteinFour.Geometry.heat_radial_connection_axis line 22236
theorem OAI.PositiveEinsteinFour.Geometry.heat_radial_connection_center line 22255
theorem OAI.PositiveEinsteinFour.Geometry.heat_radial_connection_diagonal line 22263
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.twoForm_connection_zero line 22285
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.twoForm_connection_diagonal_zero line 22294
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCoefficient_contDiff_two line 22318
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_minimum_positive_of_C1 line 22353
theorem OAI.PositiveEinsteinFour.Geometry.exists_scalar_compact_cutoff line 22438
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_minimum_positive_of_continuous line 22484
theorem OAI.PositiveEinsteinFour.Geometry.scalarBaseHeat_smooth_representative line 22579
theorem OAI.PositiveEinsteinFour.Geometry.scalar_local_positive_Euler_all_orders line 22632
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_minimum_local_H2 line 22731
def OAI.PositiveEinsteinFour.Geometry.nonlinearEpsilon line 22781
theorem OAI.PositiveEinsteinFour.Geometry.nonlinearEpsilon_pos line 22783
theorem OAI.PositiveEinsteinFour.Geometry.nonlinearEpsilon_le_one line 22787
theorem OAI.PositiveEinsteinFour.Geometry.nonlinearEpsilon_tendsto line 22792
theorem OAI.PositiveEinsteinFour.Geometry.nonlinear_square_rpow line 22797
theorem OAI.PositiveEinsteinFour.Geometry.nonlinear_power_tendsto line 22803
theorem OAI.PositiveEinsteinFour.Geometry.nonlinear_value_tendsto line 22812
theorem OAI.PositiveEinsteinFour.Geometry.nonlinear_derivative_tendsto line 22820
theorem OAI.PositiveEinsteinFour.Geometry.nonlinear_value_bound line 22849
theorem OAI.PositiveEinsteinFour.Geometry.nonlinear_L2_tendsto line 22866
theorem OAI.PositiveEinsteinFour.Geometry.nonlinear_value_dominator line 22900
theorem OAI.PositiveEinsteinFour.Geometry.nonlinear_gradient_dominator line 22915

theorem OAI.PositiveEinsteinFour.Geometry.scalarH1_subcritical_compose line 22941

Source documentation

The subcritical power has an actual H1 first jet once its value is L8 and its four weak derivatives are L4.

theorem scalarH1_subcritical_compose (d : ParallelMetricData g μ) (u : scalarH1 d)
    {p : ℝ} (hp : 2 < p) (hp4 : p < 4)
    (hu : MemLp (scalarH1Value d u : FrameBundle g → ℝ) 8 μ)
    (hDu : ∀ i, MemLp (scalarH1Gradient d i u : FrameBundle g → ℝ) 4 μ) :
    ∃ v : scalarH1 d,
      (scalarH1Value d v : FrameBundle g → ℝ) =ᵐ[μ]
        (fun x => |scalarH1Value d u x| ^ (p - 2) * scalarH1Value d u x) ∧
      ∀ i, (scalarH1Gradient d i v : FrameBundle g → ℝ) =ᵐ[μ]
        (fun x => (p - 1) * |scalarH1Value d u x| ^ (p - 2) * scalarH1Gradient d i u x) := by
…

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

def OAI.PositiveEinsteinFour.Geometry.twoFormPotentialResolvent line 23043
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotentialResolvent_compact line 23046
def OAI.PositiveEinsteinFour.Geometry.twoFormWeakPotentialKernel line 23050
theorem OAI.PositiveEinsteinFour.Geometry.mem_twoFormWeakPotentialKernel line 23055
theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeakPotentialKernel_weak line 23061
def OAI.PositiveEinsteinFour.Geometry.twoFormPotentialKernelValue line 23071
theorem OAI.PositiveEinsteinFour.Geometry.twoFormPotentialKernelValue_injective line 23082
theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeakPotentialKernel_finite line 23090
def OAI.PositiveEinsteinFour.Geometry.twoFormH1HodgeIsometry line 23117
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1Hodge_inner line 23121
theorem OAI.PositiveEinsteinFour.Geometry.twoFormH1Hodge_selfAdjoint line 23125
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRoughSolution_hodge line 23131
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRoughResolvent_hodge line 23140
def OAI.PositiveEinsteinFour.Geometry.fourHeatBundleCoefficient line 23164
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleCoefficient_contDiff line 23172
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleCoefficient_transport line 23200
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleCoefficient_center line 23222
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleOperator_const_mul line 23250
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleOperator_add line 23275
def OAI.PositiveEinsteinFour.Geometry.fourHeatBundlePolynomial line 23291
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundlePolynomial_operator line 23295
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_family_limit line 23335
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_square_half line 23379
def OAI.PositiveEinsteinFour.Geometry.fourHeatOneCoefficient line 23406
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCoefficient_contDiff line 23414
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCoefficient_transport line 23442
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCoefficient_center line 23464
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneOperator_const_mul line 23492
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneOperator_add line 23517
def OAI.PositiveEinsteinFour.Geometry.fourHeatOnePolynomial line 23533
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOnePolynomial_operator line 23537
def OAI.PositiveEinsteinFour.Geometry.fourHeatPolynomialTime line 23577
def OAI.PositiveEinsteinFour.Geometry.fourHeatGaussianPolynomialTime line 23580
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussianPolynomial_hasDerivAt line 23584
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussianPolynomialTime_continuousOn line 23590
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_compact_polynomial_pairing_deriv line 23602
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatWeightedRadialAverage_partial_zero line 23640
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatWeightedRadialAverage_second_zero line 23653
theorem OAI.PositiveEinsteinFour.Geometry.twoTensorEuclidean_norm_le_sum line 23687
theorem OAI.PositiveEinsteinFour.Geometry.heatChartTensor_bound line 23701
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyNormal_germs line 23769
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOneNormal_on_ball line 23879
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeL2_pairing_base line 23950
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.bundleFirst_zero line 24009
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.bundleZero_center line 24014
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.frame_zero line 24021
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.curvature_center line 24028
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.bundleZero_intrinsic_center line 24034
theorem OAI.PositiveEinsteinFour.Geometry.heat_partial_sum_four line 24057
theorem OAI.PositiveEinsteinFour.Geometry.heat_partial_second_sum_four line 24063
theorem OAI.PositiveEinsteinFour.Geometry.heat_partial_coordinate line 24082
theorem OAI.PositiveEinsteinFour.Geometry.heat_partial_second_coordinate line 24088
theorem OAI.PositiveEinsteinFour.Geometry.heat_radial_first_jet_alternating line 24095
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.twoForm_connection_first_jet line 24129
def OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.scalarAmplitude line 24162
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.scalarAmplitude_regular line 24166
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.scalarAmplitude_zero line 24175
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.scalarAmplitude_transport line 24179
def OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.scalarParametrix line 24199
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.scalarParametrix_regular line 24203
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalExtension.scalarParametrix_residual line 24210
def OAI.PositiveEinsteinFour.Geometry.scalarHeatContinuousValue line 24254
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatContinuousValue_L2 line 24258
def OAI.PositiveEinsteinFour.Geometry.scalarHeatContinuousLinear line 24263
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatContinuous_graph_closed line 24276
def OAI.PositiveEinsteinFour.Geometry.scalarHeatToContinuous line 24297
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatToContinuous_L2 line 24300
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatToContinuous_bound line 24304
theorem OAI.PositiveEinsteinFour.Geometry.scalar_weighted_H2_unweight line 24333
theorem OAI.PositiveEinsteinFour.Geometry.scalar_positive_Euler_local_all_orders line 24392
def OAI.PositiveEinsteinFour.Geometry.twoFormWeitzenbockKernel line 24574
instance OAI.PositiveEinsteinFour.Geometry.twoFormWeitzenbockKernel_finite line 24577
theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeitzenbockKernel_hodge line 24580
def OAI.PositiveEinsteinFour.Geometry.twoFormKernelHodge line 24591
theorem OAI.PositiveEinsteinFour.Geometry.twoFormKernelHodge_involutive line 24597
def OAI.PositiveEinsteinFour.Geometry.twoFormPositiveWeakKernel line 24603
def OAI.PositiveEinsteinFour.Geometry.twoFormNegativeWeakKernel line 24607
instance OAI.PositiveEinsteinFour.Geometry.twoFormPositiveWeakKernel_finite line 24611
instance OAI.PositiveEinsteinFour.Geometry.twoFormNegativeWeakKernel_finite line 24614
def OAI.PositiveEinsteinFour.Geometry.twoFormKernelPlus line 24617
def OAI.PositiveEinsteinFour.Geometry.twoFormKernelMinus line 24624
theorem OAI.PositiveEinsteinFour.Geometry.twoFormKernel_decomposition line 24631
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundlePolynomial_gaussian_residual line 24654
def OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative line 24720
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_partial_sum_six line 24724
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_partial line 24731
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_second line 24755
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_quadratic_majorant_integrable line 24799
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_coordinate_integrable line 24807
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_coordinate_pair_integrable line 24818
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_coordinate_covariance line 24831
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_hessian_integral line 24861
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_square_weighted line 24901
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_square_family_limit line 24911
def OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative line 24959
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_partial_sum_oneForm line 24963
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_partial line 24970
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantDerivative_second line 24994
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneOperator_cutoff line 25034
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOnePolynomial_gaussian_residual line 25081
def OAI.PositiveEinsteinFour.Geometry.fourHeatScaledCommutator line 25147
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatScaledCommutator_identity line 25156
theorem OAI.PositiveEinsteinFour.Geometry.heatChartTensor_sub line 25222
theorem OAI.PositiveEinsteinFour.Geometry.heatChartTensor_smooth_approx line 25246
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOneNormal_germs line 25292
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyScalarPartial_contDiff line 25365
def OAI.PositiveEinsteinFour.Geometry.heatFamilyBundleOperator line 25371
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyBundleOperator_contDiff line 25381
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalAmplitudeL2_pairing_normal line 25428
def OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.amplitude line 25467
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.amplitude_regular line 25472
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.amplitude_zero line 25485
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.amplitude_transport line 25493
def OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.amplitude line 25543
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.amplitude_regular line 25548
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.amplitude_zero line 25561
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.amplitude_transport line 25569
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.frame_connection_zero line 25620
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.frame_connection_first_jet line 25639
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.frame_connection_curvature_center line 25651
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.base_jacobian_center line 25670
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.frame_connection_curvature_intrinsic line 25686
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.frame_connection_half_curvature line 25702
theorem OAI.PositiveEinsteinFour.Geometry.scalar_chart_H2_realization line 25735
def OAI.PositiveEinsteinFour.Geometry.scalarHeatEvaluation line 25806
def OAI.PositiveEinsteinFour.Geometry.scalarHeatColumn line 25809
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatColumn_pairing line 25813
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatColumn_norm line 25817
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatContinuous_eigen line 25825
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeatColumn_eigen line 25836
theorem OAI.PositiveEinsteinFour.Geometry.scalar_positive_Euler_smooth line 25867
def OAI.PositiveEinsteinFour.Geometry.twoFormHodgeForm line 25936
theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeitzenbockPotential_symmetric line 25939
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeForm_comm line 25948
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeForm_add_left line 25953
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeForm_smul_left line 25958
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeForm_add_right line 25963
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeForm_smul_right line 25968
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeForm_smooth line 25972
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeForm_nonneg line 25990
theorem OAI.PositiveEinsteinFour.Geometry.linear_term_zero line 26002
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeForm_zero_left line 26018
theorem OAI.PositiveEinsteinFour.Geometry.mem_twoFormWeitzenbockKernel_iff_energy_zero line 26028
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatScaledCommutator_continuous line 26054
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatScaledCommutator_zero_of_locally_const line 26088
def OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantOperator line 26121
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantOperator_eq line 26129
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_skew_pairing line 26226
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_pairing line 26241
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatCovariantDerivative_scalar line 26278
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatDensityDrift_weighted line 26298
def OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantOperator line 26334
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneCovariantOperator_eq line 26342
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_quadratic_hasFDerivAt line 26439
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_second_order_remainder line 26451
theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_second_order_remainder_at line 26474
theorem OAI.PositiveEinsteinFour.Geometry.heatChartTensor_L2_realization line 26509
theorem OAI.PositiveEinsteinFour.Geometry.heatChartTensor_L2_norm line 26534
def OAI.PositiveEinsteinFour.Geometry.heatFamilyWeightedAverage line 26570
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyWeightedAverage_contDiff line 26574
def OAI.PositiveEinsteinFour.Geometry.heatFamilyCoefficientSequence line 26579
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyCoefficientSequence_contDiff line 26588
def OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.amplitude line 26617
theorem OAI.PositiveEinsteinFour.Geometry.HeatFamilySmoothCoefficients.amplitude_regular line 26621
def OAI.PositiveEinsteinFour.Geometry.heatFamilyOneOperator line 26648
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyOneOperator_contDiff line 26658
theorem OAI.PositiveEinsteinFour.Geometry.heatFamilyBundleOperator_slice line 26701
def OAI.PositiveEinsteinFour.Geometry.heatNormalBundleParametrix line 26750
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalBundleParametrix_residual line 26756
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatBundleOperator_initial line 26822
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.first_amplitude_center line 26839
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalBundleExtension.first_amplitude_intrinsic_center line 26865
theorem OAI.PositiveEinsteinFour.Geometry.heat_twoForm_partial_component line 26889
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalTwoFormNabla_component line 26899
theorem OAI.PositiveEinsteinFour.Geometry.fourHeatOneOperator_initial line 26933
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneFirst_zero line 26950
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneConnection_diagonal_zero line 26955
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.oneZero_center line 26962
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalOneExtension.first_amplitude_center line 26969
def OAI.PositiveEinsteinFour.Geometry.heatNormalOneParametrix line 27014
theorem OAI.PositiveEinsteinFour.Geometry.heatNormalOneParametrix_residual line 27020
def OAI.PositiveEinsteinFour.Geometry.heatConnectionMatrixLinear line 27086
theorem OAI.PositiveEinsteinFour.Geometry.heat_matrixPartial_eq_fderiv line 27100
theorem OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnectionMatrix_partial line 27112
theorem OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnectionMatrix_infinitesimal line 27124
theorem OAI.PositiveEinsteinFour.Geometry.heatTwoFormConnectionMatrix_curvature line 27131
theorem OAI.PositiveEinsteinFour.Geometry.HeatNormalFrameData.twoForm_connection_half_curvature line 27151
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeat_eigen_integral line 27207
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeat_diagonal_bound line 27222
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeat_weight_square_summable line 27240
theorem OAI.PositiveEinsteinFour.Geometry.scalarHeat_weight_summable line 27259
instance OAI.PositiveEinsteinFour.Geometry.scalarBaseEigenIndex_countable line 27268
theorem OAI.PositiveEinsteinFour.Geometry.scalar_subcritical_minimum_gradient_memLp_four line 27299
def OAI.PositiveEinsteinFour.Geometry.twoFormHodgeCompact line 27372
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeCompact_compact line 27375
def OAI.PositiveEinsteinFour.Geometry.twoFormHodgeOperator line 27378
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeOperator_inner line 27381
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeOperator_ker line 27387
def OAI.PositiveEinsteinFour.Geometry.twoFormHarmonicProjection line 27390
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonicProjection_compact line 27393
theorem OAI.PositiveEinsteinFour.Geometry.twoFormHarmonicProjection_inner line 27399
def OAI.PositiveEinsteinFour.Geometry.twoFormRegularizedHodge line 27411
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRegularizedHodge_eq_zero line 27414
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRegularizedHodge_injective line 27430
theorem OAI.PositiveEinsteinFour.Geometry.twoFormRegularizedHodge_surjective line 27437